Z3 for Reverse Engineering: Modeling, Debugging and Solving

Z3 is most useful after a verifier has been lifted into precise expressions. The hard part is rarely calling s.check(); it is matching the binary’s types, operation order, shifts, and truncation points.

This post starts with a small fixed-width checker, then moves to symbolic table lookups, debugging, optimization, and a larger practice challenge.

1. Basic Example

1
// cc -O2 -std=c11 -Wall -Wextra -o z3_basic z3_basic.c
2
#include <stdint.h>
3
#include <stdio.h>
4
#include <string.h>
5

6
static uint8_t rol8(uint8_t v, unsigned r) {
7
    r &= 7u;
8
    return (uint8_t)((v << r) | (v >> ((8u - r) & 7u)));
9
}
10

11
int main(void) {
12
    char buf[128] = {0};
13
    if (!fgets(buf, sizeof(buf), stdin)) {
14
        return 1;
15
    }
16

17
    size_t len = strcspn(buf, "\n");
18
    if (len != 24) {
19
        puts("no");
20
        return 1;
21
    }
22

23
    uint8_t x[24];
24
    memcpy(x, buf, 24);
25

26
    for (int i = 0; i < 24; i++) {
27
        if (x[i] < 0x20 || x[i] > 0x7E) {
28
            puts("no");
29
            return 1;
30
        }
31
    }
32

33
    uint32_t v = 0x13579BDFu;
34
    for (int i = 0; i < 24; i++) {
35
        v = (v + ((uint32_t)(x[i] ^ 0x5Au) * (uint32_t)(i + 3))) ^ (v >> 7);
36
        v = v + 0x1234u;
37
    }
38

39
    if ((uint8_t)(x[3] + x[8] - x[15]) != 0xA4u) {
40
        puts("no");
41
        return 1;
42
    }
43

44
    if ((uint8_t)(rol8(x[10], 3) ^ x[1]) != 0x2Cu) {
45
        puts("no");
46
        return 1;
47
    }
48

49
    if (v != 0x135A0D76u) {
50
        puts("no");
51
        return 1;
52
    }
53

54
    puts("ok");
55
    return 0;
56
}

Formula

1
uint32_t v = 0x13579BDFu;
2
for (int i = 0; i < 24; i++) {
3
    v = (v + ((uint32_t)(x[i] ^ 0x5Au) * (uint32_t)(i + 3))) ^ (v >> 7);
4
    v = v + 0x1234u;
5
}
6
if ((((uint32_t)x[3] + x[8] - x[15]) & 0xFFu) != 0xA4u) return 0;
7
if (((rol8(x[10], 3) ^ x[1]) & 0xFFu) != 0x2Cu) return 0;
8
if (v != 0x135A0D76u) return 0;

The transcription keeps the same operation order as the checker. The extra parentheses around the two byte conditions are important: in C, equality binds more tightly than bitwise & or ^. The final accumulator target, 0x135A0D76, comes from the checker and should be modeled as a fixed constant.

The corresponding Z3 model needs the same widths and conversions.

Store each symbolic input byte as BitVec(8).
Store the accumulator as BitVec(32).
Zero-extend x[i] before the 32-bit multiplication and addition.
Use LShR for the logical right shift of uint32_t.
Remember that 32-bit bit-vector arithmetic already wraps modulo $2^{32}$ .

The basic recurrence is:

v_0 = v_{\text{init}}

v'_{i+1} = \left(v_i + (x_i \oplus c)(i+3)\right) \oplus (v_i \gg 7)

v_{i+1} = v'_{i+1} + d \pmod{2^{32}}

Here, $v_{\text{init}}$ is 0x13579BDF, $c$ is 0x5A, and $d$ is 0x1234. The shift in the first equation is logical because $v_i$ is unsigned.

The remaining conditions are:

(x_3 + x_8 - x_{15}) \bmod 256 = a

\text{rol}_8(x_{10}, 3) \oplus x_1 = b

v_{24} = t

$a$ is 0xA4, $b$ is 0x2C, and $t$ is 0x135A0D76.

Now the expressions can be translated directly into Z3.

XOR and fixed rotations are linear over $GF(2)$ , while XOR with a constant is affine. Modular addition introduces carry bits, so the complete recurrence is not a simple linear system. A bit-vector SMT model preserves those carries directly.

Modeling

1
from z3 import *
2

3
def rol8(v, r):
4
    return ((v << r) | LShR(v, 8 - r)) & 0xFF
5

6
x = [BitVec(f'x{i}', 8) for i in range(24)]
7

8
def build_base_solver():
9
    s = Solver()
10

11
    # Restrict the search to printable ASCII.
12
    for i in range(24):
13
        s.add(UGE(x[i], 0x20), ULE(x[i], 0x7E))
14

15
    v = BitVecVal(0x13579BDF, 32)
16

17
    for i in range(24):
18
        xi = ZeroExt(24, x[i])
19
        v = (v + (xi ^ 0x5A) * (i + 3)) ^ LShR(v, 7)
20
        v = v + 0x1234
21

22
    return s, v
23

24
# Define the local conditions.
25
sum_cond = (ZeroExt(24, x[3]) + ZeroExt(24, x[8]) - ZeroExt(24, x[15])) & 0xFF == 0xA4
26
rot_cond = (rol8(x[10], 3) ^ x[1]) == 0x2C
27

28
# Debug each optional condition with a fresh solver.
29
checks = [
30
    ("range", And([UGE(x[i], 0x20) for i in range(24)] + [ULE(x[i], 0x7E) for i in range(24)])),
31
    ("sum", sum_cond),
32
    ("rot", rot_cond),
33
]
34

35
for name, cond in checks:
36
    s_test, _ = build_base_solver()
37
    s_test.add(cond)
38
    print(name, s_test.check())
39

40
# Solve the complete checker using the target from the binary.
41
s, v = build_base_solver()
42
s.add(sum_cond)
43
s.add(rot_cond)
44
s.add(v == BitVecVal(0x135A0D76, 32))
45

46
if s.check() == sat:
47
    m = s.model()
48
    model_values = [m.eval(xi, model_completion=True) for xi in x]
49
    candidate = bytes(value.as_long() for value in model_values)
50
    print(candidate)
51

52
    # Block this model and ask whether another solution exists.
53
    s.push()
54
    s.add(Or([xi != value for xi, value in zip(x, model_values)]))
55
    print("unique" if s.check() == unsat else "multiple solutions")
56
    s.pop()
57
else:
58
    print("unsat")

This checker is intentionally underconstrained. Z3 returns one valid printable candidate, but the blocking clause finds another model. If a challenge expects a unique flag, add every format and cross-byte constraint present in the binary instead of assuming the first model is the intended answer.

The screenshot below records the one-time setup used to construct this synthetic example: a preliminary model produced 0x135A0D76, that value was placed in the C checker, and the resulting candidate was replayed against the compiled program. The finalized solver above starts from the checker constant, which is the workflow used when reversing a real binary. Because the checker has multiple solutions, the candidate bytes may also differ between runs or Z3 versions.

Original target generation and candidate replay

ZeroExt(24, x[i]) converts an unsigned 8-bit byte into a 32-bit operand.
LShR(v, 7) matches the logical shift of a uint32_t; v >> 7 in Z3 would be an arithmetic shift.
A 32-bit BitVec wraps automatically. Use a mask or Extract where the binary actually truncates to a smaller width.
Z3Py can coerce many Python integers from context, but BitVecVal(value, width) makes width-sensitive constants explicit.

2. Advanced Example

Table lookup + mixed recurrence + aggregate checks

This pattern appears frequently in larger verifiers: a symbolic table lookup feeds a mixed accumulator, while several local conditions constrain selected bytes.

1
Input: 32 bytes
2
Round:
3
1) Substitute an input byte through a 256-byte table T
4
2) Update a 32-bit accumulator v with XOR, ADD, and ROL
5
3) Apply partial checks at selected positions
6
Final: v == 0x7A3C91F2

The lifted verifier has the following properties.

A real S-box or permutation table makes direct algebraic inversion harder.
Mixing rotate, XOR, and addition causes the accumulator expression to grow quickly.
Multiple partial checks make a bad transcription become unsat, often before the final condition is added.

The concrete table below, T[i] = i ^ 0xA5, is intentionally simple and affine; it demonstrates symbolic lookup rather than S-box strength. In a real verifier, a nonlinear table combined with carry-producing addition is what defeats a straightforward linear solution.

Formula

Start with a fixed initial accumulator such as 0xC0FFEE00.

v_{i+1} = \text{rol}_{32}(v_i, 5) + (T[x_i] \oplus (i \cdot c)) + (v_i \gg 3)

Here, $c$ is a round constant such as 0x13, and the entire result wraps to 32 bits.

One intermediate condition is:

(T[x_7] + T[x_{19}] - T[x_{23}]) \bmod 256 = m

where $m$ is a fixed byte from the checker.

Modeling

1
from z3 import *
2

3
def rol32(v, r):
4
    return ((v << r) | LShR(v, 32 - r)) & 0xFFFFFFFF
5

6
# Deliberately simple lookup table for the modeling example.
7
T = [i ^ 0xA5 for i in range(256)]
8

9
x = [BitVec(f'x{i}', 8) for i in range(32)]
10
s = Solver()
11

12
# Printable
13
for i in range(32):
14
    s.add(UGE(x[i], 0x20), ULE(x[i], 0x7E))
15

16
def Tlookup(b):
17
    return Sum([If(b == k, BitVecVal(T[k], 8), BitVecVal(0, 8)) for k in range(256)])
18

19
v = BitVecVal(0xC0FFEE00, 32)
20

21
for i in range(32):
22
    # Symbolic T[x[i]] using a deliberately naive 256-way expression.
23
    tval = Tlookup(x[i])
24
    t32 = ZeroExt(24, tval)
25

26
    v = rol32(v, 5) + (t32 ^ BitVecVal(i * 0x13, 32)) + LShR(v, 3)
27

28
# Intermediate checks
29
s.add((Tlookup(x[7]) + Tlookup(x[19]) - Tlookup(x[23])) & 0xFF == 0xB6)
30
s.add((x[5] ^ x[11] ^ x[29]) == 0x2D)
31
s.add(((x[2] + x[9] + x[17]) & 0xFF) == 0x90)
32

33
# Final condition
34
s.add(v == 0x7A3C91F2)
35

36
if s.check() == sat:
37
    m = s.model()
38
    ans = bytes([m.eval(x[i], model_completion=True).as_long() for i in range(32)])
39
    print(ans)

1
> python3 solve2.py
2
b'r0&,f~D0v!p/zl"9GI\\CV86`xz `;|c.'

This is one satisfying model. Because the constraints are not unique, the exact bytes may change across Z3 versions or solver configurations. Use the blocking-clause pattern from the basic example if the challenge requires proof that the result is unique.

Table Lookup with Array

The first model builds a 256-way If expression for every lookup. A Z3 Array represents the same concrete table more directly.

1
arr = K(BitVecSort(8), BitVecVal(0, 8))
2
for k, value in enumerate(T):
3
    arr = Store(arr, BitVecVal(k, 8), BitVecVal(value, 8))
4

5
tval = Select(arr, x[i])

Starting from K gives every array index a defined value before the 256 stores are applied. Select avoids rebuilding the long conditional expression at each use. This usually reduces expression size, although the solver’s final performance still depends on the surrounding constraints.

3. Common Modeling Faults

Most failed solver scripts come from semantic mismatches rather than Z3 itself.

Signed versus unsigned values

Do not assume that a decompiler’s char is unsigned. Check the load, extension, comparison, and shift instructions. Use ZeroExt for an unsigned widening conversion and SignExt for a signed one. Z3’s overloaded comparisons on bit-vectors are signed, so use ULT, ULE, UGT, and UGE for unsigned comparisons.

Operation order

(a + b) ^ c and a + (b ^ c) are different expressions. Follow the assembly or decompiler expression in execution order, including every cast and temporary.

Integer promotion and truncation

In C, uint8_t operands are normally promoted to int before arithmetic. The result is truncated only when it is cast or stored back into a narrower object. Model the promoted expression at the width used by the binary, then truncate at the exact assignment or cast; using only 8-bit expressions everywhere can hide carries too early.

Logical versus arithmetic right shift

An unsigned C right shift maps to LShR. Z3’s >> operator on a bit-vector is arithmetic and preserves the sign bit. For rotations, use RotateLeft or RotateRight when the count is constant, or reproduce the binary’s masked variable-count expression explicitly.

4. Debugging

Add one condition at a time

1
s.push()
2
s.add(condition_1)
3
print(s.check())
4
s.pop()

push() and pop() preserve the base model while testing one extra condition. Repeating this narrows the first point at which the model becomes inconsistent.

A system containing only XOR and fixed rotations may admit a direct linear treatment. Addition with carries and nonlinear table lookups are the point where a bit-vector solver becomes much more convenient.

Test a checks list with fresh solvers

Do not add every optional condition to one already-constrained solver and then try to test them individually. Build a fresh base solver for each check so earlier optional constraints do not contaminate the result.

1
checks = [
2
    ("range", And([UGE(x[i], 0x20) for i in range(24)] + [ULE(x[i], 0x7E) for i in range(24)])),
3
    ("sum", sum_cond),
4
    ("rot", rot_cond),
5
]
6

7
for name, cond in checks:
8
    s_test, _ = build_base_solver()
9
    s_test.add(cond)
10
    print(name, s_test.check())

If range is unsat, the base input-domain model is contradictory. If sum or rot becomes unsat, recheck that expression’s operation order, width, and overflow behavior. This isolates a bad condition before the full recurrence hides it.

Check intermediate values

If IDA or Ghidra provides a concrete intermediate value, constrain the symbolic expression captured at that exact program point.

1
s.add(checkpoint_v == BitVecVal(0x1234ABCD, 32))

If this is unsat, the mismatch occurs at or before that checkpoint. Move the checkpoint earlier until the symbolic and concrete executions agree.

Replay the model

1
m = s.model()
2
candidate = bytes(m.eval(xi, model_completion=True).as_long() for xi in x)
3
print(candidate)

Pass the candidate to the original binary. A sat result validates the model you wrote, not the transcription from the binary.

5. Optimization

Restrict the domain: if the binary accepts only uppercase letters and digits, encode that exact range immediately.
Remove proven redundancy: drop a condition only after confirming that it is implied by the remaining constraints.
Reuse expressions: build repeated table lookups and round expressions once instead of reconstructing them.
Partition independent constraints: solve separable byte groups first, but do not split a recurrence or cross-byte condition arbitrarily.

Solver time depends on expression structure. Smaller domains, shared subexpressions, and early local checks often help more than changing tactics blindly.

Z3 is not a substitute for reversing. The decisive skill is still extracting the correct expression with the correct types, widths, and overflow behavior. Once those semantics are right, even a dense verifier becomes manageable.

6. Practice

✨ Free Challenge Download ✨

1
#include <stdio.h>
2
#include <stdint.h>
3
#include <string.h>
4

5
static uint32_t lcg_next(uint32_t *s) {
6
    *s = (*s * 1664525u) + 1013904223u;
7
    return *s;
8
}
9

10
static uint32_t rotl32(uint32_t x, unsigned r) {
11
    r &= 31u;
12
    return (x << r) | (x >> ((32u - r) & 31u));
13
}
14

15
static uint64_t rotl64(uint64_t x, unsigned r) {
16
    r &= 63u;
17
    return (x << r) | (x >> ((64u - r) & 63u));
18
}
19

20
static uint32_t read_le32(const uint8_t *p) {
21
    return (uint32_t)p[0]
22
        | ((uint32_t)p[1] << 8)
23
        | ((uint32_t)p[2] << 16)
24
        | ((uint32_t)p[3] << 24);
25
}
26

27
static void gen_perm(uint8_t perm[48]) {
28
    uint32_t s = 0xA3C59AC3u;
29
    for (int i = 0; i < 48; i++) {
30
        perm[i] = (uint8_t)i;
31
    }
32
    for (int i = 47; i > 0; i--) {
33
        s = lcg_next(&s);
34
        uint32_t j = s % (uint32_t)(i + 1);
35
        uint8_t tmp = perm[i];
36
        perm[i] = perm[j];
37
        perm[j] = tmp;
38
    }
39
}
40

41
static void gen_sbox(uint8_t sbox[24]) {
42
    uint32_t s = 0xC3D2E1F0u;
43
    for (int i = 0; i < 24; i++) {
44
        s = lcg_next(&s);
45
        sbox[i] = (uint8_t)s;
46
    }
47
}
48

49
static void gen_keys(uint32_t keys[18]) {
50
    uint32_t s = 0x1BADB002u;
51
    for (int i = 0; i < 18; i++) {
52
        s = lcg_next(&s);
53
        keys[i] = s;
54
    }
55
}
56

57
static void gen_tbox(uint32_t tbox[16]) {
58
    uint32_t s = 0xB16B00B5u;
59
    for (int i = 0; i < 16; i++) {
60
        s = lcg_next(&s);
61
        tbox[i] = s;
62
    }
63
}
64

65
static uint32_t feistel_f(uint32_t x, uint32_t k, const uint32_t tbox[16]) {
66
    uint32_t y = x + k;
67
    uint32_t z = rotl32(x ^ k, y & 31u);
68
    uint32_t m = (x * 0x045d9f3bu) ^ rotl32(y, 7);
69
    uint32_t t = tbox[(x ^ k) & 0xFu];
70
    uint32_t f = z + m + t + 0x9e3779b9u;
71
    f ^= (f >> 16);
72
    f += rotl32(f, 3);
73
    return f;
74
}
75

76
static int check_ascii(const uint8_t *buf, size_t len) {
77
    for (size_t i = 0; i < len; i++) {
78
        if (buf[i] < 0x20 || buf[i] > 0x7e) {
79
            return 0;
80
        }
81
    }
82
    return 1;
83
}
84

85
static int check_stream(const uint8_t *buf) {
86
    static const uint8_t stream_expected[48] = {
87
        0x24, 0xd9, 0x4e, 0x85, 0x4f, 0x7d, 0x68, 0xb7,
88
        0x08, 0x22, 0x1e, 0x4d, 0xd7, 0xdf, 0x99, 0x3d,
89
        0xac, 0xfe, 0xd4, 0x06, 0x68, 0xfd, 0x21, 0x68,
90
        0x42, 0xe3, 0x4d, 0x71, 0xec, 0x7d, 0xe6, 0xf4,
91
        0x5a, 0x18, 0x9e, 0xef, 0x9c, 0x5b, 0x0d, 0x3e,
92
        0x60, 0x78, 0x91, 0xfe, 0xc1, 0x93, 0x63, 0xf5
93
    };
94
    uint32_t s = 0xD00DFEEDu;
95
    for (int i = 0; i < 48; i++) {
96
        s = lcg_next(&s);
97
        uint8_t ks = (uint8_t)(s >> 24);
98
        if ((uint8_t)(buf[i] ^ ks) != stream_expected[i]) {
99
            return 0;
100
        }
101
    }
102
    return 1;
103
}
104

105
static int check_perm_sbox(const uint8_t *buf) {
106
    static const uint8_t perm_expected[24] = {
107
        0xe3, 0xc0, 0xe9, 0x57, 0x6c, 0x97, 0xa9, 0xac,
108
        0x27, 0xee, 0x52, 0x13, 0x52, 0x01, 0x15, 0x22,
109
        0xe4, 0x02, 0x4e, 0x09, 0x70, 0xb0, 0x08, 0x9c
110
    };
111
    uint8_t perm[48];
112
    uint8_t sbox[24];
113
    gen_perm(perm);
114
    gen_sbox(sbox);
115
    for (int i = 0; i < 24; i++) {
116
        uint8_t v = (uint8_t)(buf[perm[i]] ^ sbox[i]);
117
        if (v != perm_expected[i]) {
118
            return 0;
119
        }
120
    }
121
    return 1;
122
}
123

124
static int check_feistel(const uint8_t *buf) {
125
    static const uint32_t expL[6] = {
126
        0xc808b416u, 0xe9100223u, 0x5031e4ccu,
127
        0x610df482u, 0x22c9a088u, 0x05f105c9u
128
    };
129
    static const uint32_t expR[6] = {
130
        0xa217b24bu, 0xd5881d02u, 0x9f8c09e4u,
131
        0x9605e10au, 0xe4fb1a56u, 0xb20a9001u
132
    };
133
    uint32_t keys[18];
134
    uint32_t tbox[16];
135
    gen_keys(keys);
136
    gen_tbox(tbox);
137

138
    for (int blk = 0; blk < 6; blk++) {
139
        const uint8_t *p = buf + (blk * 8);
140
        uint32_t L = read_le32(p);
141
        uint32_t R = read_le32(p + 4);
142
        for (int r = 0; r < 3; r++) {
143
            uint32_t k = keys[(blk * 3) + r];
144
            uint32_t f = feistel_f(R, k, tbox);
145
            uint32_t newL = R;
146
            R = L ^ f;
147
            L = newL;
148
        }
149
        if (L != expL[blk] || R != expR[blk]) {
150
            return 0;
151
        }
152
    }
153
    return 1;
154
}
155

156
static int check_hash(const uint8_t *buf) {
157
    const uint64_t expected = 0x8a7ad627100d088aULL;
158
    uint64_t h = 0x0123456789ABCDEFULL;
159
    for (int i = 0; i < 48; i++) {
160
        h ^= (uint64_t)(buf[i] + i);
161
        h *= 0x100000001B3ULL;
162
        h = rotl64(h, 17);
163
        h ^= (h >> 23);
164
    }
165
    return h == expected;
166
}
167

168
static int check_sums(const uint8_t *buf) {
169
    const uint32_t sum_even_expected = 0x0000d028u;
170
    const uint32_t sum_odd_expected  = 0x0000e5e8u;
171
    const uint8_t xor_expected = 0x60u;
172

173
    uint32_t sum_even = 0;
174
    uint32_t sum_odd = 0;
175
    uint8_t xor_all = 0;
176

177
    for (int i = 0; i < 48; i++) {
178
        if ((i & 1) == 0) {
179
            sum_even += (uint32_t)buf[i] * (uint32_t)(i + 1);
180
        } else {
181
            sum_odd += (uint32_t)buf[i] * (uint32_t)(i + 1);
182
        }
183
        xor_all ^= buf[i];
184
    }
185
    return sum_even == sum_even_expected
186
        && sum_odd == sum_odd_expected
187
        && xor_all == xor_expected;
188
}
189

190
int main(void) {
191
    char input[128];
192
    if (!fgets(input, sizeof(input), stdin)) {
193
        return 1;
194
    }
195
    size_t len = strcspn(input, "\r\n");
196
    input[len] = '\0';
197

198
    if (len != 48) {
199
        puts("wrong");
200
        return 0;
201
    }
202

203
    const uint8_t *buf = (const uint8_t *)input;
204
    if (!check_ascii(buf, len)) {
205
        puts("wrong");
206
        return 0;
207
    }
208

209
    if (check_stream(buf) &&
210
        check_perm_sbox(buf) &&
211
        check_feistel(buf) &&
212
        check_hash(buf) &&
213
        check_sums(buf)) {
214
        puts("correct");
215
    } else {
216
        puts("wrong");
217
    }
218
    return 0;
219
}

The input must be exactly 48 printable ASCII bytes.
An LCG-derived keystream XOR constrains every byte.
Permutation and S-box XOR constraints cover 24 selected positions.
Six 8-byte blocks pass through three Feistel rounds and must match the expected left and right words.
A rolling hash, weighted sums, and a final XOR provide independent consistency checks.

Model the 48 input bytes as bit-vectors and translate each checker function at its native width.

1
from z3 import *
2

3
A = 1664525
4
C = 1013904223
5

6
def lcg(x):
7
    return (x * A + C) & 0xFFFFFFFF
8

9
def gen_perm():
10
    state = 0xA3C59AC3
11
    perm = list(range(48))
12
    for i in range(47, 0, -1):
13
        state = lcg(state)
14
        j = state % (i + 1)
15
        perm[i], perm[j] = perm[j], perm[i]
16
    return perm
17

18
def gen_sbox():
19
    state = 0xC3D2E1F0
20
    sbox = []
21
    for _ in range(24):
22
        state = lcg(state)
23
        sbox.append(state & 0xFF)
24
    return sbox
25

26
def gen_keys():
27
    state = 0x1BADB002
28
    keys = []
29
    for _ in range(18):
30
        state = lcg(state)
31
        keys.append(state)
32
    return keys
33

34
def gen_tbox():
35
    state = 0xB16B00B5
36
    tbox = []
37
    for _ in range(16):
38
        state = lcg(state)
39
        tbox.append(state)
40
    return tbox
41

42
perm_expected = [
43
    0xe3, 0xc0, 0xe9, 0x57, 0x6c, 0x97, 0xa9, 0xac,
44
    0x27, 0xee, 0x52, 0x13, 0x52, 0x01, 0x15, 0x22,
45
    0xe4, 0x02, 0x4e, 0x09, 0x70, 0xb0, 0x08, 0x9c
46
]
47

48
stream_expected = [
49
    0x24, 0xd9, 0x4e, 0x85, 0x4f, 0x7d, 0x68, 0xb7,
50
    0x08, 0x22, 0x1e, 0x4d, 0xd7, 0xdf, 0x99, 0x3d,
51
    0xac, 0xfe, 0xd4, 0x06, 0x68, 0xfd, 0x21, 0x68,
52
    0x42, 0xe3, 0x4d, 0x71, 0xec, 0x7d, 0xe6, 0xf4,
53
    0x5a, 0x18, 0x9e, 0xef, 0x9c, 0x5b, 0x0d, 0x3e,
54
    0x60, 0x78, 0x91, 0xfe, 0xc1, 0x93, 0x63, 0xf5
55
]
56

57
expL = [0xc808b416, 0xe9100223, 0x5031e4cc, 0x610df482, 0x22c9a088, 0x05f105c9]
58
expR = [0xa217b24b, 0xd5881d02, 0x9f8c09e4, 0x9605e10a, 0xe4fb1a56, 0xb20a9001]
59

60
hash_expected = 0x8a7ad627100d088a
61
sum_even_expected = 0x0000d028
62
sum_odd_expected = 0x0000e5e8
63
xor_expected = 0x60
64

65
b = [BitVec(f"b{i}", 8) for i in range(48)]
66
s = SolverFor("QF_AUFBV")
67

68
for i in range(48):
69
    s.add(UGE(b[i], 0x20), ULE(b[i], 0x7e))
70

71
state = 0xD00DFEED
72
for i in range(48):
73
    state = lcg(state)
74
    ks = (state >> 24) & 0xFF
75
    s.add(b[i] ^ BitVecVal(ks, 8) == BitVecVal(stream_expected[i], 8))
76

77
perm = gen_perm()
78
sbox = gen_sbox()
79
for i in range(24):
80
    s.add(b[perm[i]] ^ BitVecVal(sbox[i], 8) == BitVecVal(perm_expected[i], 8))
81

82
keys = gen_keys()
83
tbox = gen_tbox()
84
tbox_arr = K(BitVecSort(4), BitVecVal(0, 32))
85
for i, v in enumerate(tbox):
86
    tbox_arr = Store(tbox_arr, BitVecVal(i, 4), BitVecVal(v, 32))
87

88
def rotl32_var(x, r):
89
    r = r & BitVecVal(31, 32)
90
    inv = (-r) & BitVecVal(31, 32)
91
    return (x << r) | LShR(x, inv)
92

93
def feistel_f(x, k):
94
    y = x + k
95
    z = rotl32_var(x ^ k, y)
96
    m = (x * BitVecVal(0x045d9f3b, 32)) ^ RotateLeft(y, 7)
97
    idx = Extract(3, 0, x ^ k)
98
    t = Select(tbox_arr, idx)
99
    f = z + m + t + BitVecVal(0x9e3779b9, 32)
100
    f = f ^ LShR(f, 16)
101
    f = f + rotl32_var(f, BitVecVal(3, 32))
102
    return f
103

104
def pack_le32(bs):
105
    return Concat(bs[3], bs[2], bs[1], bs[0])
106

107
for blk in range(6):
108
    off = blk * 8
109
    L = pack_le32(b[off:off+4])
110
    R = pack_le32(b[off+4:off+8])
111
    for r in range(3):
112
        k = BitVecVal(keys[blk * 3 + r], 32)
113
        f = feistel_f(R, k)
114
        L, R = R, L ^ f
115
    s.add(L == BitVecVal(expL[blk], 32))
116
    s.add(R == BitVecVal(expR[blk], 32))
117

118
h = BitVecVal(0x0123456789ABCDEF, 64)
119
for i in range(48):
120
    h = h ^ (ZeroExt(56, b[i]) + BitVecVal(i, 64))
121
    h = h * BitVecVal(0x100000001B3, 64)
122
    h = RotateLeft(h, 17)
123
    h = h ^ LShR(h, 23)
124
s.add(h == BitVecVal(hash_expected, 64))
125

126
sum_even = BitVecVal(0, 32)
127
sum_odd = BitVecVal(0, 32)
128
xor_all = BitVecVal(0, 8)
129
for i in range(48):
130
    if i % 2 == 0:
131
        sum_even = sum_even + ZeroExt(24, b[i]) * (i + 1)
132
    else:
133
        sum_odd = sum_odd + ZeroExt(24, b[i]) * (i + 1)
134
    xor_all = xor_all ^ b[i]
135

136
s.add(sum_even == BitVecVal(sum_even_expected, 32))
137
s.add(sum_odd == BitVecVal(sum_odd_expected, 32))
138
s.add(xor_all == BitVecVal(xor_expected, 8))
139

140
if s.check() != sat:
141
    print("unsat")
142
    raise SystemExit(1)
143

144
m = s.model()
145
candidate = "".join(chr(m.eval(b[i]).as_long()) for i in range(48))
146
print(candidate)
147

148
lia = SolverFor("QF_LIA")
149
x = [Int(f"x{i}") for i in range(48)]
150
for i in range(48):
151
    lia.add(x[i] == ord(candidate[i]))
152
    lia.add(x[i] >= 0x20, x[i] <= 0x7e)
153

154
lia.add(Sum([x[i] * (i + 1) for i in range(0, 48, 2)]) == sum_even_expected)
155
lia.add(Sum([x[i] * (i + 1) for i in range(1, 48, 2)]) == sum_odd_expected)
156

157
assert lia.check() == sat
158

159
xor_val = 0
160
for ch in candidate:
161
    xor_val ^= ord(ch)
162
assert xor_val == xor_expected

In this particular checker, the stream equations already determine all 48 bytes. The permutation, Feistel, hash, sum, and XOR constraints therefore act as independent validation of both the candidate and the transcription. The final QF_LIA block does not discover a second solution; it rechecks the weighted sums after fixing every integer to the candidate byte.

Top 3 Solver (Discord @badabodaa)

1
@Greedun RubiyaLab 2025.12.27
2
@Gunter RubiyaLab 2025.12.27