> For the complete documentation index, see [llms.txt](https://jesuscries.gitbook.io/home/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://jesuscries.gitbook.io/home/ctf-writeups/reverse-engineering/acs-2023-licrackense-pt-i.md).

# 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).

<figure><img src="/files/5VuzuzxPxh4p07olplDu" alt=""><figcaption></figcaption></figure>

## 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.

<figure><img src="/files/1PI78YvsA8LH5wiQo9VJ" alt=""><figcaption></figcaption></figure>

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.)

<figure><img src="/files/NHxMpsxJQwJ3gWL9EX5R" alt=""><figcaption></figcaption></figure>

Running Angr gives us the license key in just under 15 seconds!

<figure><img src="/files/KaEJOHRs3TpKbKospRre" alt=""><figcaption></figcaption></figure>

**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:

<figure><img src="/files/JnoV7zJ3yiH2a63WNUHR" alt=""><figcaption></figcaption></figure>

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.

<figure><img src="/files/FL87khVe4YL1kPMph38p" alt=""><figcaption></figcaption></figure>

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.

<figure><img src="/files/rDfigRHzugPjw8veLUfu" alt=""><figcaption></figcaption></figure>

**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)
```