Skip to content

Instantly share code, notes, and snippets.

@shahril96
Last active Oct 15, 2019
Embed
What would you like to do?
Generate valid input (printable) for pwnable.kr'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))
else:
print("Unsat")
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment