Skip to content

Instantly share code, notes, and snippets.

@ion1
Last active May 29, 2021 11:57
Show Gist options
  • Save ion1/107288cd282d4c9586bc6f397fbd2b75 to your computer and use it in GitHub Desktop.
Save ion1/107288cd282d4c9586bc6f397fbd2b75 to your computer and use it in GitHub Desktop.
Finding a hash collision with z3
from itertools import cycle
from z3 import *
class NameGen:
def __init__(self, prefix):
self.prefix = prefix
self.count = 0
def gen(self):
name = f"{self.prefix}{self.count}"
self.count += 1
return name
def main():
s = Solver()
xs = [BitVecVal(ord(x), 32) for x in "Hello there"]
xhash = hash(s, xs)
for length in range(0, 20, 2):
print(f"Trying length {length}")
s.push()
y_gen = NameGen("y")
ys = [
*[BitVecVal(ord(c), 32) for c in "General Ke"],
*[
with_constraint(
s,
BitVec(y_gen.gen(), 32),
lambda y: And(
y >= ord("a"),
y <= ord("z"),
Or(y == ord("y"), is_vowel(y) == (i % 2 != 0)),
),
)
for i in range(length)
],
*[BitVecVal(ord(c), 32) for c in "bi"],
]
yhash = hash(s, ys)
s.add(xhash == yhash)
if s.check() == sat:
while s.check() == sat:
m = s.model()
x_str = "".join([chr(m.evaluate(y).as_long()) for y in ys])
print(x_str)
# Exclude this solution and try again to find other solutions
# with the same length.
s.add(Or(*[y != m.evaluate(y) for y in ys]))
break
s.pop()
def hash(s, values):
h = BitVecVal(5381, 32)
for x in reversed(values):
h = (h * 33) ^ x
return h
def with_constraint(s, val, constraints):
s.add(constraints(val))
return val
def is_vowel(x):
return Or(*[x == ord(c) for c in "AEIOUaeiou"])
if __name__ == "__main__":
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment