JavaCrackMe.jar이라는 .jar 확장자를 가진 자바 패키지 파일을 내려받게 된다.
Decompiled-src
jadx-gui로 디컴파일해서 소스코드를 확인해봤다.
package defpackage;
/* renamed from: JavaCrackMe reason: default package */
/* loaded from: JavaCrackMe.jar:JavaCrackMe.class */
public class JavaCrackMe {
public static final synchronized /* bridge */ /* synthetic */ void main(String... strArr) {
try {
System.out.println("Reversing.Kr CrackMe!!");
System.out.println("-----------------------------");
System.out.println("The idea came out of the warsaw's crackme");
System.out.println("-----------------------------\n");
if (Long.decode(strArr[0]).longValue() * 26729 == -1536092243306511225L) {
System.out.println("Correct!");
} else {
System.out.println("Wrong");
}
} catch (Exception e) {
System.out.println("Please enter a 64bit signed int");
}
}
}
long 타입인 값을 입력받아 26729를 곱했을때, -1536092243306511225라는 값이 나와야된다.
>>> -1536092243306511225 / 26729 -57469125044203.34
나누어 떨어지지 않기 때문에,
integer overflow해서 저 값으로 맞추어야 된다.
from z3 import *
import numpy as np
def twos_complement(n, bits=64):
return n - 2 ** 64
code1 = BitVec('code1', 64)
equations = [
(code1 * 26729) & 0x7fffffffffffffff == (-1536092243306511225 & 0x7fffffffffffffff)
]
solver = Solver()
for equation in equations:
solver.add(equation)
solutions = []
while solver.check() == sat:
model = solver.model()
solution = {
'code1': model[code1].as_long()
}
solutions.append(solution)
solver.add(code1 != model[code1])
for i, solution in enumerate(solutions):
print(f"Solution {i + 1}:")
for var_name, value in solution.items():
print(f"{var_name}: {(value)}")
print(twos_complement(value))
print()
PS C:\Users\Seo Hyun-gyu\Downloads\JavaCrackMe> python3 solve.py Solution 1: code1: 245287194656008047 -18201456879053543569 Solution 2: code1: 9468659231510783855 -8978084842198767761
그럼 2개의 결과가 나오는데, 이중 9468659231510783855 값의 보수인 -8978084842198767761 값이 정답이다.