We have to provide a string that matches a specific value when hashed with FNV. Z3 is able to directly solve the challenge, if used carefully.
Event Link: DownUnder CTF 2023
Challenge Description
The challenge consists in a simple implementation of FNV hash:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
def fnv1(s):
h = 0xcbf29ce484222325
for b in s:
print(f'{b = }')
h *= 0x00000100000001b3
h &= 0xffffffffffffffff
print(f'Check {hex(h) = }')
h ^= b
print(f'{hex(h) = }')
return h
TARGET = 0x1337133713371337
s = bytearray.fromhex(input())
if fnv1(s) == TARGET:
print('Well done!')
print(os.getenv('FLAG'))
Our goal FNV is a non-cryptographic hash function. We want to find an input that hashes to TARGET = 0x1337133713371337.
Solution
Apparently there were two different intended solutions, one based on LLL and the other one on MITM (this one was actually found by Robin during the challenge). However, I tried (and failed) to implent the hash collision using z3 (following this approach). The idea is to re-implement fnv to operate on z3 BitVec and then just throw them into a solver. After the CTF I found in the discord a solution with only two small differences from mine:
- the multiplication step was instead a multiplication by a
BitVecVal; - I runned my code sequentially, increasing each time the lenght of the input vector; they run it in parallel with different lenght.
I need to benchmark the first part, since it can actually make a difference depending on the implementation but I’m not sure. However I think the second one is more important: when I patched and run my code it finished in around 1h on an input lenght of 10, but it didn’t terminate for 7 (which was the point I got stuck during the CTF).
This is my final code:
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
from z3 import *
import sys
TARGET = BitVecVal(0x1337133713371337, 64)
mul = BitVecVal(0x00000100000001b3, 64)
def fnv1(s):
h = BitVecVal(0xcbf29ce484222325, 64)
for b in s:
h = h * mul
h = h ^ ZeroExt((64-8), b)
return h
s = Solver()
l = int(sys.argv[1])
bs = [BitVec(f'b_{n}', 8) for n in range(l)]
s.add(fnv1(bs) == TARGET)
assert s.check() == sat, f'Unsat for {l = }'
m = s.model()
out = ''
for bi in bs:
out += hex(m[bi].as_long())[2:]
print(f'{out = }')