MidnightSun Quals: Revver

April 4, 2022 · 18 min read · rev z3 ·

Share on:

Overview

Solved by: zzz, Zopazz

Writeup by: Zopazz

Description:

Automated reversing is a solved problem, right.

Writeup

General challenge information

In this challenge we were provided with a netcat session, which would respond with one of 20 random dynamically generated shellcodes encoded as hex.

The session would then prompt for an answer, which would satisfy the shellcodes input check.

The goal of the challenge was to find a way to dynamically solve all 20 binaries, which would then give the flag. Since the binaries would have a different solution every time, it was not possible to just reverse them one by one and some kind of dynamic solve script was required.

It’s important to note that each binary differed in how it accepted user input, which could either be via. path, a file, a socket etc.. This was randomized each run, and therefore using a tool like angr, seemed to bring way too much overhead into the equation, as we would not even have to make the binary run. We would also have to make angr solve it afterwards.

We therefore decided to write our own solve scripts to solve these binaries dynamically

The binaries

We quickly realized that all the binaries sent, although they would have different answers each time, relied on 5 different ways of checking the user input.The way used to check the user input was determined by the number of the binary (1-20) mod 5.

The binary check mechanisms were as follows:

Checks whether the user input is equal to a string found in the binary (we called it base64 since it looks like base64)
Checks whether the user input is equal to an array of 10 chars xored with a static value
Checks whether the user input satisfies a CRC32 check of a specified length, ASCII only
Generates a table from a string and transforms the userinput, then checks the user input against the table and xors it with a hardcoded value
Checks whether the user input is equal to two arrays of variable length added together.

Knowing this, we could start working on dynamically extracting the information we needed from the binaries and creating algorithms to solve them dynamically.

We opted to find unique byte sequences each type of binary shared, then indexing into the binary to extract the information we needed

Binary 0

For this we just needed to extract the string within the binary. We noticed that all binaries of this trype, no matter the iteration, had a “rep movsb” instruction right after loading the offset of the string:

This meant we could just find the occurence of this instruction, then index backwards inside the binary to find the offset of the string and extract it:

Implementation:

1
2
3
4
5
6
def solve_base64(data):
    idx = data.find(b'\xF3\xA4') #Grab rep movsb
    instrs = data[idx - 0xd:][:0x20] #Find lea instruction, loading string
    off = u16(instrs[2:2+2]) #Get the string offset
    b64_data = data[off:].split(b"\x00")[0] #Get the extract the string, we know it ends at a null byte
    return b64_data

Binary 1

For this we need to extract 2 things. We need to extract the character array it checks our input against along with the xor value.

Every binary contains a pop ebx, before the array is allocated, following by the mov instructions:

This allows us to searc for the bytes of pop ebx and the first bytes of the mov instruction to find the beginning of the allocation of the array.

Since each mov instruction is exactly 4 bytes long, we can then extract 40 bytes forward and grab the last 2 bytes of each using string manipulation.

The following code extracts the array:

1
2
3
4
5
6
7
8
9
lookingfor = b'\x5B\xC6\x45'
idxstart = data.find(lookingfor)+1
idxend = idxstart + 40

valarray1 = data[idxstart:idxend].split(b'\xc6E')[1:]

valarray2 = []
for item in valarray1:
    valarray2.append(item[1])

The current array value is always xor’ed with the low byte of ecx and an xor instruction like this only occurs once in the binaries:

We can search for the beginning of these instructions (80 F1) to find the offset and then extract the xor value:

1
xorval = data[data.find(b'\x80\xF1')+2]

Then we can xor the values together to get the correct answer.

Full implementation:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
def solveone(data):
    lookingfor = b'\x5B\xC6\x45'
    idxstart = data.find(lookingfor)+1
    idxend = idxstart + 40

    valarray1 = data[idxstart:idxend].split(b'\xc6E')[1:]

    valarray2 = []
    for item in valarray1:
        valarray2.append(item[1])

    xorval = data[data.find(b'\x80\xF1')+2]
    
    sol = b''
    for item in valarray2:
        sol+=p8(item^xorval)
    
    return sol

Binary 2

This one is a bit more complicated as it requires us to extract the CRC32 target value along with the desired length of the input.

We then need to find an input string consisting of only ASCII characters, which satisfies these constraints.

After talking it over we agreed on solving this using z3, but as none of us solving this challenge had any idea of how to actually solve stuff using z3, we opted to find existing implementations.

Unfortunately we could not find an implementation where we could supply a length and stay within the constraints of ascii, so we decided to instead glue 2 different scripts together and call it a day.

The scripts were:

https://gist.github.com/percontation/11310679 which constrains the search space to only ascii but can only solve if the length is a multiple of 4 (as it deals only with 32 bit blocks)
https://github.com/sam-b/z3-stuff/blob/master/crc32/crc32.py which doesn’t constrain the search space to only ascii but let’s us solve any length.

We then found our best superglue and duct tape and did some arts and crafts to create a z3 solver which fit our constraints.

Extracting the goal CRC and length from these binaries wasn’t a one fit all solution, we had to write 3 different functions to extract these values:

solve_two which solves binary 2
solve_seven which solves binary 7 and 17
solve_twelve which solves binary 12.

Extraction of these values worked about the same way as in earlier examples. Once we had the values we ran it through our super duper best written z3 solver ever created (which definetely wasn’t hacked together hapharzardly).

The implementation of the aforementionened solvers can be seen here:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
polynomial = 0xEDB88320

def f_crc32(data,size,prev=0):
 crc = prev ^ 0xFFFFFFFF
 for i in range(0,size,8):
  crc = crc ^ (z3.LShR(data,i) & 0xFF)
  for _ in range(8):
   crc = If(crc & 1 == BitVecVal(1, size), z3.LShR(crc,1) ^ polynomial, z3.LShR(crc,1))
 return crc ^ 0xFFFFFFFF

def isAscii(bv, shamt):
    # Note the use of z3.And here. Using python's `and` would be incorrect!
    return And(32 <= (LShR(bv,  shamt) & 0xff), (LShR(bv, shamt) & 0xff) < 127)


def solve_seven(data):
    off = data.find(b"\x3B\xC6\x74\x02")

    input_len_off = off - 7
    input_len = data[input_len_off]
    print("input length", hex(input_len))

    crc_val_off = off - 0xf
    crc_val = u32(data[crc_val_off:crc_val_off+4])
    print(f"crc: {crc_val:#x}")

    size = input_len * 8
    target = crc_val
    s = z3.Solver()
    data = z3.BitVec('data',size)
    s.add(f_crc32(data,size) == target)

    for i in range(input_len):
        s.add(isAscii(data, i * 8))

    if s.check() == z3.sat:
       result = long_to_bytes(int(str(s.model()[data])))
    else:
        print("unsat :(")
        exit(0)
    return result[::-1]


def solve_twelve(data):
    off = data.find(bytes.fromhex("59 F3 A4 33 DB"))

    input_len_off = off - 1
    input_len = data[input_len_off]
    print("input length", hex(input_len))

    crc_val_off = off + 6
    crc_val = u32(data[crc_val_off:crc_val_off+4])
    print(f"crc: {crc_val:#x}")

    size = input_len * 8
    target = crc_val
    s = z3.Solver()
    data = z3.BitVec('data',size)
    s.add(f_crc32(data,size) == target)

    for i in range(input_len):
        s.add(isAscii(data, i * 8))

    if s.check() == z3.sat:
       result = long_to_bytes(int(str(s.model()[data])))
    else:
        print("unsat :(")
        exit(0)
    return result[::-1]

def solve_two(data):
    off = data.find(b"\x8D\x45\x98")

    input_len_off = off + 20
    input_len = data[input_len_off]
    print("input length", hex(input_len))

    crc_val_off = input_len_off+12

    print(hex(crc_val_off))
    crc_val = u32(data[crc_val_off:crc_val_off+4])
    print(f"crc: {crc_val:#x}")

    size = input_len * 8
    target = crc_val
    s = z3.Solver()
    data = z3.BitVec('data',size)
    s.add(f_crc32(data,size) == target)

    for i in range(input_len):
        s.add(isAscii(data, i * 8))

    if s.check() == z3.sat:
       result = long_to_bytes(int(str(s.model()[data])))
       print(hex(zlib.crc32(result[::-1])))
    else:
        print("unsat :(")
        exit(0)
    return result[::-1]

Binary 3

Binary 3 again required us to write 3 solve functions as we had no consistent way of extracting the data we needed consistently.

We needed to extract:

The answer xor values for after transforms
The input for the table creation (a string located in the binary)
The input length

For solving this one we created a function to emulate the creation of the table:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
def create_table(src, src_len):
    dst = [0] * 0x258
    for i in range(0x100):
        dst[i] = i
    v5 = 0
    for j in range(0x100):
        v5 = (dst[j] + src[j % src_len] + v5) & 0xff
        v7 = dst[j]
        dst[j] = dst[v5]
        dst[v5] = v7
    dst[256] = 0
    dst[257] = 0
    return dst

We then created a function to emulate the transformation of the input:

1
2
3
4
5
6
7
8
9
def transform_input_and_table(a1):
    v1 = (a1[0x100] + 1) & 0xff
    v2 = (a1[v1] + a1[257]) & 0xff
    a1[256] = v1
    a1[257] = v2
    v4 = a1[v2]
    a1[v2] = a1[v1]
    a1[v1] = v4
    return a1[(a1[v2] + v4) & 0xff], a1

Once this was done we could run the functions as normal. We could then get the answer of the binary by:

Creating a table by supplying the string found in the binary
Loop through the answer array transforming the table for each character in the answer array and outputting the transformed input
xor the output of the transform with the answer

Implementation:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
def solve_three(data):
    def create_table(src, src_len):
        dst = [0] * 0x258
        for i in range(0x100):
            dst[i] = i;

        v5 = 0
        for j in range(0x100):
            v5 = (dst[j] + src[j % src_len] + v5) & 0xff
            v7 = dst[j]
            dst[j] = dst[v5]
            dst[v5] = v7

        dst[256] = 0
        dst[257] = 0
        return dst


    def transform_input_and_table(a1):
        v1 = (a1[0x100] + 1) & 0xff
        v2 = (a1[v1] + a1[257]) & 0xff
        a1[256] = v1
        a1[257] = v2
        v4 = a1[v2]
        a1[v2] = a1[v1]
        a1[v1] = v4
        return a1[(a1[v2] + v4) & 0xff], a1
    
    

    input_len_off = data.find(b'\x59\xf3\xa4') - 1
    input_len = data[input_len_off]
    print("input length", hex(input_len))

    answer_off = input_len_off - 9
    print("answer_off", hex(answer_off))
    answer_imm = u16(data[answer_off:answer_off+2])
    print(hex(answer_imm))

    answer = data[answer_imm : ].split(b"\x00")[0]
    print(answer)

    off = data.find(b'\x8B\xCB\xe8') + 0xc
    b64_off = u16(data[off:off+2])
    print("off", hex(off))
    print(hex(b64_off))
    b64_data = data[b64_off:].split(b'\x00')[0]

    print(b64_data)
    b1 = create_table(b64_data, len(b64_data))

    print(b1)
    solution = b''

    for x in answer:
        c, b1 = transform_input_and_table(b1)
        solution += p8(x ^ c)
    
    print("answer", solution)
    return solution

The 2 other functions look the same, but just extracts different offsets in the binary.

In the end we created 3 functions with the following functionality:

solve_three, solves binary 3
solve_eight, solves binary 8 and 13
solve_eigtheen, solves binary 18

Binary 4

For binary 4 we needed to extract the 2 different arrays created, which came right after each other.

Luckily binary 4 and it’s counterparts had almost the same instructions right before allocating the string on the stack. They either had:

1
2
push 1;
pop edi;

1
2
push 1;
pop esi;

We realized that if we search for push 1; pop edi but it ends up not using that sequence, when allocating the string, the index returned will be below 100. We can therefore first search for that sequence, check whether or not the index we find, is above or below 100 and if it is, we just search for the other sequence.

Since the arrays are a variable length, we also needed to figure out how big they were. Luckily they all end with the same instruction after allocating all the variables on the stack:

We can therefore just look from the start offset untill we hit the xor ecx, ecx instruction.

Since both arrays get allocated in one big mess, we don’t have an exact value we can find for how big they are. But since they are both the same length, we can just extract the full thing and then split the array in half to get two seperate ones.

Then all we need to do is subtract one from the other, then and the result with 0xffff to emulate underflows.

Implementation of this can be seen here:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
def solvefour(data):
    lookingfor = b'\x6a\x01\x5f'

    idxstart = data.find(lookingfor)+3

    if idxstart<100:
        lookingfor = b'\x6a\x01\x5e'
        idxstart = data.find(lookingfor)+3

    idxend = data[idxstart:].find(b'\x33\xc9')+idxstart
    instructionarray = data[idxstart:idxend].split(b'\x66\xc7')[1:]

    valarraybytes = []

    for item in instructionarray:
        valarraybytes.append(item[-2:])
    
    valarray1 = valarraybytes[:int(len(valarraybytes)/2)]
    valarray2 = valarraybytes[int(len(valarraybytes)/2):]

    sol = b''
    for i in range(len(valarray1)):
        sol+=(u16(valarray2[i]) - u16(valarray1[i]) & 0xffff).to_bytes(2,"big")
    
    return sol

The full solution

Now that we have solve functions for each binary, we can then connect to the netcat session and solve them, using our solve functions and pwntools:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
solvers = {
    "three":solve_three,
    "eight":solve_eight,
    "thirteen":solve_eight,
    "eighteen":solve_eighteen,
    
    'two':solve_two,
    "seven":solve_seven,
    "seventeen":solve_seven,
    "twelve":solve_twelve,
    
    "one": solveone,
    "six": solveone,
    "eleven": solveone,
    "sixteen": solveone,
    
    "four":solvefour,
    "nine":solvefour,
    "fourteen":solvefour,
    "nineteen":solvefour,

    "five"    : solve_base64,
    "ten"     : solve_base64,
    "fiveteen": solve_base64,
    "twenty"  : solve_base64,
}


io = remote("revver-01.hfsc.tf", 3320)
io.sendlineafter("2)", "2")

for i in range(20):
    print("curr", hex(i))
    io.recvuntil("RANDOM BINARY ")

    which_bin = io.recvline().decode()[:-1].lower()
    data = bytes.fromhex(io.recvline().decode())
    print(which_bin)
    
    answer = solvers[which_bin](data)
    print("our answer:", answer)
    io.sendlineafter("ANSWER:",  answer)

io.interactive()

This gives us the flag:

1
midnight{Reversing_got_alot_easier_with_backup_cameras}

Full solve script:

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
from pwn import *
from z3 import *
import z3
import sys
import zlib
from Crypto.Util.number import long_to_bytes
context.arch = "i386"

def solve_base64(data):
    idx = data.find(b'\xF3\xA4')
    print(hex(idx))
    instrs = data[idx - 0xd:][:0x20]
    print(disasm(instrs))

    off = u16(instrs[2:2+2])
    print(hex(off))
    b64_data = data[off:].split(b"\x00")[0]
    print(b64_data)
    return b64_data

def solveone(data):
    lookingfor = b'\x5B\xC6\x45'
    idxstart = data.find(lookingfor)+1
    idxend = idxstart + 40

    valarray1 = data[idxstart:idxend].split(b'\xc6E')[1:]

    valarray2 = []
    for item in valarray1:
        valarray2.append(item[1])

    xorval = data[data.find(b'\x80\xF1')+2]
    
    sol = b''
    for item in valarray2:
        sol+=p8(item^xorval)
    
    return sol

def solvefour(data):
    lookingfor = b'\x6a\x01\x5f'

    idxstart = data.find(lookingfor)+3

    if idxstart<100:
        lookingfor = b'\x6a\x01\x5e'
        idxstart = data.find(lookingfor)+3

    idxend = data[idxstart:].find(b'\x33\xc9')+idxstart
    instructionarray = data[idxstart:idxend].split(b'\x66\xc7')[1:]

    valarraybytes = []

    for item in instructionarray:
        valarraybytes.append(item[-2:])
    
    valarray1 = valarraybytes[:int(len(valarraybytes)/2)]
    valarray2 = valarraybytes[int(len(valarraybytes)/2):]

    sol = b''
    for i in range(len(valarray1)):
        sol+=(u16(valarray2[i]) - u16(valarray1[i]) & 0xffff).to_bytes(2,"big")
    
    return sol




def solve_three(data):
    def create_table(src, src_len):
        dst = [0] * 0x258
        for i in range(0x100):
            dst[i] = i;

        v5 = 0
        for j in range(0x100):
            v5 = (dst[j] + src[j % src_len] + v5) & 0xff
            v7 = dst[j]
            dst[j] = dst[v5]
            dst[v5] = v7

        dst[256] = 0
        dst[257] = 0
        return dst


    def transform_input_and_table(a1):
        v1 = (a1[0x100] + 1) & 0xff
        v2 = (a1[v1] + a1[257]) & 0xff
        a1[256] = v1
        a1[257] = v2
        v4 = a1[v2]
        a1[v2] = a1[v1]
        a1[v1] = v4
        return a1[(a1[v2] + v4) & 0xff], a1
    
    

    input_len_off = data.find(b'\x59\xf3\xa4') - 1
    input_len = data[input_len_off]
    print("input length", hex(input_len))

    answer_off = input_len_off - 9
    print("answer_off", hex(answer_off))
    answer_imm = u16(data[answer_off:answer_off+2])
    print(hex(answer_imm))

    answer = data[answer_imm : ].split(b"\x00")[0]
    print(answer)

    off = data.find(b'\x8B\xCB\xe8') + 0xc
    b64_off = u16(data[off:off+2])
    print("off", hex(off))
    print(hex(b64_off))
    b64_data = data[b64_off:].split(b'\x00')[0]

    print(b64_data)
    b1 = create_table(b64_data, len(b64_data))

    print(b1)
    solution = b''

    for x in answer:
        c, b1 = transform_input_and_table(b1)
        solution += p8(x ^ c)
    
    print("answer", solution)
    return solution


def solve_eight(data):
    def create_table(src, src_len):
        dst = [0] * 0x258
        for i in range(0x100):
            dst[i] = i;

        v5 = 0
        for j in range(0x100):
            v5 = (dst[j] + src[j % src_len] + v5) & 0xff
            v7 = dst[j]
            dst[j] = dst[v5]
            dst[v5] = v7

        dst[256] = 0
        dst[257] = 0
        return dst


    def transform_input_and_table(a1):
        v1 = (a1[0x100] + 1) & 0xff
        v2 = (a1[v1] + a1[257]) & 0xff
        a1[256] = v1
        a1[257] = v2
        v4 = a1[v2]
        a1[v2] = a1[v1]
        a1[v1] = v4
        return a1[(a1[v2] + v4) & 0xff], a1
    
    input_len_off = data.find(b'\x59\xf3\xa4') - 1
    print(hex(input_len_off))
    input_len = data[input_len_off]
    print("input length", hex(input_len))

    answer_off = data.find(b'\x59\xf3\xa4', input_len_off + 4) - 0xa
    print("answer_off", hex(answer_off))
    answer_imm = u16(data[answer_off:answer_off+2])
    print(hex(answer_imm))

    answer = data[answer_imm : ].split(b"\x00")[0]
    print(answer)

    off = input_len_off + 9
    b64_off = u16(data[off:off+2])
    print("off", hex(off))
    print(hex(b64_off))
    b64_data = data[b64_off:].split(b'\x00')[0]

    print("b64_data", b64_data)
    b1 = create_table(b64_data, len(b64_data))

    print(b1)
    solution = b''

    for x in answer:
        c, b1 = transform_input_and_table(b1)
        solution += p8(x ^ c)
    
    print("answer", solution)
    return solution



def solve_eighteen(data):
    def create_table(src, src_len):
        dst = [0] * 0x258
        for i in range(0x100):
            dst[i] = i;

        v5 = 0
        for j in range(0x100):
            v5 = (dst[j] + src[j % src_len] + v5) & 0xff
            v7 = dst[j]
            dst[j] = dst[v5]
            dst[v5] = v7

        dst[256] = 0
        dst[257] = 0
        return dst


    def transform_input_and_table(a1):
        v1 = (a1[0x100] + 1) & 0xff
        v2 = (a1[v1] + a1[257]) & 0xff
        a1[256] = v1
        a1[257] = v2
        v4 = a1[v2]
        a1[v2] = a1[v1]
        a1[v1] = v4
        return a1[(a1[v2] + v4) & 0xff], a1
    
    

    input_len_off = data.find(b'\x59\xf3\xa4') - 1
    input_len = data[input_len_off]
    print("input length", hex(input_len))

    answer_off = input_len_off - 9
    print("answer_off", hex(answer_off))
    answer_imm = u16(data[answer_off:answer_off+2])
    print(hex(answer_imm))

    answer = data[answer_imm : ].split(b"\x00")[0]
    print(answer)

    off = data.find(b'\x49\xf2\xae') - 0x12
    b64_off = u16(data[off:off+2])
    print("off", hex(off))
    print(hex(b64_off))
    b64_data = data[b64_off:].split(b'\x00')[0]

    print(b64_data)
    b1 = create_table(b64_data, len(b64_data))

    print(b1)
    solution = b''

    for x in answer:
        c, b1 = transform_input_and_table(b1)
        solution += p8(x ^ c)
    
    print("answer", solution)
    return solution




polynomial = 0xEDB88320

def f_crc32(data,size,prev=0):
 crc = prev ^ 0xFFFFFFFF
 for i in range(0,size,8):
  crc = crc ^ (z3.LShR(data,i) & 0xFF)
  for _ in range(8):
   crc = If(crc & 1 == BitVecVal(1, size), z3.LShR(crc,1) ^ polynomial, z3.LShR(crc,1))
 return crc ^ 0xFFFFFFFF

def isAscii(bv, shamt):
    # Note the use of z3.And here. Using python's `and` would be incorrect!
    return And(32 <= (LShR(bv,  shamt) & 0xff), (LShR(bv, shamt) & 0xff) < 127)


def solve_seven(data):
    off = data.find(b"\x3B\xC6\x74\x02")

    input_len_off = off - 7
    input_len = data[input_len_off]
    print("input length", hex(input_len))

    crc_val_off = off - 0xf
    crc_val = u32(data[crc_val_off:crc_val_off+4])
    print(f"crc: {crc_val:#x}")

    size = input_len * 8
    target = crc_val
    s = z3.Solver()
    data = z3.BitVec('data',size)
    s.add(f_crc32(data,size) == target)

    for i in range(input_len):
        s.add(isAscii(data, i * 8))

    if s.check() == z3.sat:
       result = long_to_bytes(int(str(s.model()[data])))
    else:
        print("unsat :(")
        exit(0)
    return result[::-1]


def solve_twelve(data):
    off = data.find(bytes.fromhex("59 F3 A4 33 DB"))

    input_len_off = off - 1
    input_len = data[input_len_off]
    print("input length", hex(input_len))

    crc_val_off = off + 6
    crc_val = u32(data[crc_val_off:crc_val_off+4])
    print(f"crc: {crc_val:#x}")

    size = input_len * 8
    target = crc_val
    s = z3.Solver()
    data = z3.BitVec('data',size)
    s.add(f_crc32(data,size) == target)

    for i in range(input_len):
        s.add(isAscii(data, i * 8))

    if s.check() == z3.sat:
       result = long_to_bytes(int(str(s.model()[data])))
    else:
        print("unsat :(")
        exit(0)
    return result[::-1]

def solve_two(data):
    off = data.find(b"\x8D\x45\x98")

    input_len_off = off + 20
    input_len = data[input_len_off]
    print("input length", hex(input_len))

    crc_val_off = input_len_off+12

    print(hex(crc_val_off))
    crc_val = u32(data[crc_val_off:crc_val_off+4])
    print(f"crc: {crc_val:#x}")

    size = input_len * 8
    target = crc_val
    s = z3.Solver()
    data = z3.BitVec('data',size)
    s.add(f_crc32(data,size) == target)

    for i in range(input_len):
        s.add(isAscii(data, i * 8))

    if s.check() == z3.sat:
       result = long_to_bytes(int(str(s.model()[data])))
       print(hex(zlib.crc32(result[::-1])))
    else:
        print("unsat :(")
        exit(0)
    return result[::-1]

solvers = {
    "three":solve_three,
    "eight":solve_eight,
    "thirteen":solve_eight,
    "eighteen":solve_eighteen,

    'two':solve_two,
    "seven":solve_seven,
    "seventeen":solve_seven,
    "twelve":solve_twelve,

    "one": solveone,
    "six": solveone,
    "eleven": solveone,
    "sixteen": solveone,

    "four":solvefour,
    "nine":solvefour,
    "fourteen":solvefour,
    "nineteen":solvefour,

    "five"    : solve_base64,
    "ten"     : solve_base64,
    "fiveteen": solve_base64,
    "twenty"  : solve_base64,
}


io = remote("revver-01.hfsc.tf", 3320)
io.sendlineafter("2)", "2")

for i in range(20):
    print("curr", hex(i))
    io.recvuntil("RANDOM BINARY ")

    which_bin = io.recvline().decode()[:-1].lower()
    data = bytes.fromhex(io.recvline().decode())
    print(which_bin)
    
    answer = solvers[which_bin](data)
    print("our answer:", answer)
    io.sendlineafter("ANSWER:",  answer)

io.interactive()