# ACS 2023: Licrackense Pt I
## 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](https://jesuscries.gitbook.io/home/ctf-writeups/binary-exploitation/acs-2023-licrackense-pt-ii).
## 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
```python
#!/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:
{% hint style="info" %}
The default right shift >> in Z3 is arithmetical, so Z3's LShR() function (logical shift right) is used instead.
{% endhint %}
```python
# 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:
{% hint style="info" %}
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.
{% endhint %}
```python
# 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
```python
#!/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)
```
---
# Agent Instructions: Querying This Documentation
If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.
Perform an HTTP GET request on the current page URL with the `ask` query parameter:
```
GET https://jesuscries.gitbook.io/home/ctf-writeups/reverse-engineering/acs-2023-licrackense-pt-i.md?ask=
```
The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.
Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.
