Skip to content

Instantly share code, notes, and snippets.

Last active Oct 15, 2019
What would you like to do?
Generate valid input (printable) for's collision
import struct
from z3 import *
p = [BitVec('p{}'.format(i), 32) for i in range(5)]
s = Solver()
for a in p:
for i in range(4):
s.add(((a >> i*8) & 0xff) >= 0x30)
s.add(((a >> i*8) & 0xff) <= 0x7a)
s.add(((a >> i*8) & 0xff) != 0x60)
s.add(p[0] + p[1] + p[2] + p[3] + p[4] == 0x21DD09EC)
if s.check() == sat:
m = s.model()
print(''.join(struct.pack("<I", m[a].as_long()).decode() for a in p))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment