Z3 for Reverse Engineering: Modeling, Debugging and Solving

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
    return (uint8_t)((v << r) | (v >> (8 - r)));
8
}
9

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

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

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

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

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

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

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

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

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

Formula

1
uint32_t v = 0x13579BDF;
2
for (int i = 0; i < 24; i++) {
3
    v = (v + (x[i] ^ 0x5A) * (i + 3)) ^ (v >> 7);
4
    v = (v + 0x1234) & 0xFFFFFFFF;
5
}
6
if ((x[3] + x[8] - x[15]) & 0xFF != 0xA4) return 0;
7
if (((x[10] << 3) | (x[10] >> 5)) ^ x[1] != 0x2C) return 0;
8
if (v != 0x135A0D76) return 0;

위 Formula는 위 C 코드와 동일하게 맞춘 버전이다. 최종 상수는 Z3로 뽑은 v_target을 그대로 사용한다.

이런 유형은 식을 제대로 뽑으면 Z3가 대부분 풀어준다.

이걸 그대로 Z3로 옮기면 된다. 추가로 타입과 오버플로우에 주의하자.

uint8_t는 BitVec(8)
uint32_t는 BitVec(32)
& 0xFFFFFFFF는 32비트 오버플로우 유지
x[i]는 연산 전에 32비트로 확장

Basic 예시를 수식으로 정리하면 아래처럼 된다.

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}}

여기서 $v_{\text{init}}$ 은 0x13579BDF, $c$ 는 0x5A, $d$ 는 0x1234다.

추가 조건은 아래와 같이 정리된다.

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

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

v_{24} = t

$a$ 는 0xA4, $b$ 는 0x2C, $t$ 는 0x135A0D76이다.

그대로 Z3로 구현하자.

부분적으로 선형처럼 보이지만 전체는 비선형이다. XOR/ROL은 GF(2) 기준에서 선형(또는 affine)으로 볼 수 있지만, ADDITION은 CARRY 때문에 비선형이다. 따라서 선형 해법만으로는 풀기 어렵고 비트벡터 SMT가 필요하다.

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
    # Printable로만 제한 (탐색 축소)
12
    for i in range(24):
13
        s.add(x[i] >= 0x20)
14
        s.add(x[i] <= 0x7E)
15

16
    v = BitVecVal(0x13579BDF, 32)
17

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

23
    return s, v
24

25
# 개별 조건 정의
26
sum_cond = (ZeroExt(24, x[3]) + ZeroExt(24, x[8]) - ZeroExt(24, x[15])) & 0xFF == 0xA4
27
rot_cond = (rol8(x[10], 3) ^ x[1]) == 0x2C
28

29
# 디버깅용: 조건 하나씩 체크
30
checks = [
31
    ("range", And([x[i] >= 0x20 for i in range(24)] + [x[i] <= 0x7E for i in range(24)])),
32
    ("sum", sum_cond),
33
    ("rot", rot_cond),
34
]
35

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

41
# sum + rot만 만족하는 해에서 v 값을 뽑는다.
42
s_mid, v_mid = build_base_solver()
43
s_mid.add(sum_cond)
44
s_mid.add(rot_cond)
45

46
if s_mid.check() == sat:
47
    m_mid = s_mid.model()
48
    v_target = m_mid.eval(v_mid).as_long()
49
    print("v_target =", hex(v_target))
50

51
    s_full, v_full = build_base_solver()
52
    s_full.add(sum_cond)
53
    s_full.add(rot_cond)
54
    s_full.add(v_full == v_target)
55

56
    if s_full.check() == sat:
57
        m = s_full.model()
58
        ans = bytes([m[x[i]].as_long() for i in range(24)])
59
        print(ans)
60
else:
61
    print("unsat")

위 코드에서 출력되는 v_target이 C 문제의 최종 상수다.

z3_basic

ZeroExt(24, x[i])를 써서 8비트 $\rightarrow$ 32비트 확장
& 0xFFFFFFFF로 32비트 오버플로우 유지
Python int와 Z3 BitVec를 구분하자 $\rightarrow$ BitVecVal

2. Advanced Example

(table + 혼합 라운드 + 누적 체크)

실제로 자주 나오는 테이블 기반 혼합 + 누적 체크 유형이다

1
입력: 32바이트
2
라운드:
3
1) 256바이트 테이블 T로 입력 바이트를 치환
4
2) 32비트 누적값 v 갱신 (xor/add/rol 혼합)
5
3) 중간마다 부분 체크
6
최종: v == 0x7A3C91F2

수식으로 정리하면 이런 형태다.

위 조건은

테이블 치환 때문에 역산이 어렵다.
누적값에 rol/xor/add가 섞여 있어 식이 폭발한다.
중간 체크가 여러 개여서 부분적으로 모순이 생기기 쉽다.

여기서도 선형/비선형이 섞인다. XOR/ROL은 선형에 가깝지만, ADDITION은 CARRY 때문에 비선형이고 테이블 치환은 거의 완전 비선형이다. 이 조합 때문에 단순 선형 해법이 잘 안 먹힌다.

Formula

차근차근 짜보자.

초기값은 0xC0FFEE00 같은 상수라고 가정한다.

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

여기서 $c$ 는 0x13 같은 라운드 상수다.

중간 체크

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

$m$ 은 상수 값

Modeling

1
from z3 import *
2

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

6
# 테이블 예시
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(x[i] >= 0x20)
15
    s.add(x[i] <= 0x7E)
16

17
v = BitVecVal(0xC0FFEE00, 32)
18

19
for i in range(32):
20
    # T[x[i]]를 만들기 위한 식
21
    tval = Sum([If(x[i] == k, BitVecVal(T[k], 8), 0) for k in range(256)])
22
    t32 = ZeroExt(24, tval)
23

24
    v = rol32(v, 5) + (t32 ^ BitVecVal(i * 0x13, 32)) + LShR(v, 3)
25
    v = v & 0xFFFFFFFF
26

27
# 중간 체크
28
def Tlookup(b):
29
    return Sum([If(b == k, BitVecVal(T[k], 8), 0) for k in range(256)])
30

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

35
# 최종 조건
36
s.add(v == 0x7A3C91F2)
37

38
if s.check() == sat:
39
    m = s.model()
40
    ans = bytes([m[x[i]].as_long() for i in range(32)])
41
    print(ans)

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

Table Optimization

위 방식은 If 256개를 합치는 형태라 느릴 수 있다. 보통은 아래 방법을 쓴다.

Z3 Array로 테이블을 만들고 Select 사용

1
Arr = Array('Arr', BitVecSort(8), BitVecSort(8))
2
arr_init = Arr
3
for k in range(256):
4
    arr_init = Store(arr_init, BitVecVal(k, 8), BitVecVal(T[k], 8))
5

6
tval = Select(arr_init, x[i])

이렇게 바꾸면 속도가 개선된다.

3. Fault

자주 하는 실수를 모아보았다.

signed/unsigned 혼동 char가 signed인지 unsigned인지 확인해야 한다. 보통 리버싱에서는 uint8_t로 보는 게 안전하다. signed 연산이면 SignExt가 필요하다.
연산 순서 (a + b) ^ c와 a + (b ^ c)는 완전히 다르다. 어셈블리 기준으로 그대로 따라야 한다.
8비트 연산 승격 C에서는 uint8_t도 연산 시 int로 승격된다. 즉 실제 바이너리는 32비트로 계산 후 다시 잘리는 경우가 많다. 이걸 놓치면 모델이 틀어진다.

4. Debugging

조건을 잘게 쪼개기

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

이걸 반복하면 어느 조건에서 꼬였는지 나온다.

XOR/ROL만 남기면 선형처럼 풀릴 수도 있지만, ADDITION/테이블이 섞이면 비선형이 되어 SMT가 필요해진다.

checks로 단독 검사하기

checks 배열도 디버깅에 포함된다. 중요한 건 이미 모든 제약이 들어간 Solver에 추가로 넣지 말고, 매번 새 Solver를 만들어 단독으로 검사해야 한다는 점이다.

1
checks = [
2
    ("range", And([x[i] >= 0x20 for i in range(24)] + [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())

range가 unsat이면 입력 범위 자체가 모순이다. sum이나 rot이 unsat면 해당 식이 잘못 뽑혔거나 타입/오버플로우가 틀린 경우다.
이 단계에서 어디가 꼬이는지 바로 좁힐 수 있다.

중간값 검증

IDA/ghidra에서 계산한 중간값이 있으면 그대로 넣어본다.

1
s.add(v == 0x1234ABCD)

여기서 unsat가 뜨면 모델링이 틀렸다.

모델 출력 후 직접 검증

1
m = s.model()
2
print([m[x[i]].as_long() for i in range(24)])

이 값으로 실제 바이너리에 넣어서 통과하는지 확인한다.

5. Optimization

범위 제한: 입력이 대문자/숫자만 허용되면 바로 줄인다.
불필요 조건 제거: 결과에 영향 없는 조건은 빼라.
표현식 캐싱: 같은 표현은 변수로 만들어 재사용.
부분 solve: 먼저 절반만 풀고 나머지를 고정.

Z3는 제약이 명확하면 빠르다. 모호하면 느리다.

z3는 만능은 아니다. 그래도 수식만 정확히 만들면 대부분 풀린다. 결국 실력 차이는 식을 뽑는 능력과 타입, 오버플로우 감각에서 갈린다고 생각한다. 감이 잡히면 난제도 풀린다.

6. 실습

✨ 챌린지 공짜 다운로드 ✨

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
}

체커 흐름을 보면 입력은 48바이트 ASCII여야 한다.
LCG 기반 키스트림 XOR로 각 바이트를 고정한다.
24개 위치에 대해 permutation + S-box XOR 제약을 추가한다.
6개 블록에 대해 3라운드 Feistel을 적용하고 L/R 결과를 맞춘다.
롤링 해시와 선형 합/ XOR 조건으로 최종 문자열을 확정한다.

실제로는 48바이트를 Z3 BitVec으로 모델링하고 모든 검사를 제약으로 넣어 풀어야 한다.

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_BV")
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

Top 3 Solver (Discord @badabodaa)

1
@Greedun RubiyaLab 2025.12.27
2
@Gunter RubiyaLab 2025.12.27