ACS 2023: Licrackense Pt I

I forgot my license key.. can you crack it and read the secret document for me?

TL;DR

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 2nd stage.

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)