Simple license key checker that can be cracked via Angr or z3 with some light reversing.
Challenge Overview
This is the 1st part of the challenge which involves reversing the license key before we can proceed to the .
Solution 1: via Angr
In the first stage, our user input undergoes a series of algorithmic operations defined in the checker function to verify a match with the hardcoded bytes.
Since the operations are not too complex and do not lead to path explosion, we can solve this using Angr's find_condition. (find_address will not work due to PIE enabled in the binary.)
Running Angr gives us the license key in just under 15 seconds!
License Key: HWKLERGNEUPMQGDA-ERIGADPQWJVIGNEG
Final Script
#!/usr/bin/env python3
import angr
import sys
import claripy
import logging
def is_successful(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return b"The license key is acceptable" in stdout_output
def should_abort(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return b"Unacceptable license key.." in stdout_output
logging.getLogger('angr').setLevel('INFO')
project = angr.Project("./licrackense", auto_load_libs=True)
initial_state = project.factory.entry_state(
add_options={
angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS
}
)
print(initial_state)
sm = project.factory.simgr(initial_state)
sm.explore(find=is_successful, avoid=should_abort)
if sm.found:
solution_state = sm.found[0]
solution = solution_state.posix.dumps(sys.stdin.fileno()).decode()
print(solution)
else:
raise Exception("Could not find the solution")
Solution 2: via z3
At first glance, the encryption subroutine seems to be undergoing a multi-step process:
Translating this to z3 gives:
The default right shift >> in Z3 is arithmetical, so Z3's LShR() function (logical shift right) is used instead.
# Stage 1
for i in range(0x21):
input[i] = LShR(input[i], 6) | LShL(input[i], 2)
# Stage 2
for i in range(0x21):
input[i] = LShL(input[i] & 0xf, 4) + LShR(input[i], 4)
# Stage 3
for i in range(0x21 - 1):
input[i] ^= input[i+1]
# Stage 4
for i in range(0x21):
input[i] = LShL(input[i] & 0xf, 4) + LShR(input[i], 4)
# Stage 5
for i in range(0x21):
input[i] ^= xor_key[i]
However, cross-referencing the decompiled pseudocode through pattern matching with ChatGPT shows that it is more likely to be Bit Rotation.
Making corrections to the z3 expression gives:
Due to compiler optimization, + addition and & with a bitmask of 0xf is sometimes used to achieve the same result as | bitwise OR. This can be observed through Stage 1, 2, and 4.
# Stage 1
for i in range(0x21):
input[i] = RotateLeft(input[i], 2)
# Stage 2
for i in range(0x21):
input[i] = RotateRight(input[i], 4)
# Stage 3
for i in range(0x21 - 1):
input[i] ^= input[i+1]
# Stage 4
for i in range(0x21):
input[i] = RotateRight(input[i], 4)
# Stage 5
for i in range(0x21):
input[i] ^= xor_key[i]
Running the solver gives us the flag pretty much immediately.
License Key: HWKLERGNEUPMQGDA-ERIGADPQWJVIGNEG
Final Script
#!/usr/bin/python3
from z3 import *
s = Solver()
xor_key = [0x35, 0x78, 0xDA, 0x89, 0xAD, 0x90, 0x34, 0x75, 0x4F, 0x67, 0xFD, 0x89, 0x79, 0xF3, 0x43, 0x28, 0x9D, 0x67, 0xDF, 0x54, 0xF7, 0x82, 0x11, 0x20, 0xDF, 0x89, 0x34, 0x38, 0x9D, 0x67, 0x47, 0x89, 0xD8]
enc = [0x49, 0x8, 0xC6, 0xAD, 0xF1, 0xC4, 0x10, 0x59, 0x0F, 0x73, 0x89, 0xF9, 0x21, 0xFF, 0x57, 0x99, 0x3C, 0x3B, 0xB3, 0x6C, 0xEF, 0x96, 0x41, 0x24, 0xC7, 0xFD, 0x44, 0x44, 0xA5, 0x43, 0x6B, 0x81, 0xC5]
# License key length = 33
input = [BitVec(str(i), 8) for i in range(0x21)]
# Stage 1
for i in range(0x21):
input[i] = RotateLeft(input[i], 2)
# Stage 2
for i in range(0x21):
input[i] = RotateRight(input[i], 4)
# Stage 3
for i in range(0x21 - 1):
input[i] ^= input[i+1]
# Stage 4
for i in range(0x21):
input[i] = RotateRight(input[i], 4)
# Stage 5
for i in range(0x21):
input[i] ^= xor_key[i]
# Check byte-by-byte
for i in range(0x21):
s.add(input[i] == enc[i])
if s.check() == sat:
model = s.model()
indices = [BitVec(f"{i}", 8) for i in range(33)]
# Index value for s.model() expects type BitVecRef and not Int
license = ""
for i in indices:
license += chr(model[i].as_long())
print("License:", license)
