Skip to content

Instantly share code, notes, and snippets.

@shahrilnet
Last active October 15, 2019 16:42
Show Gist options
  • Save shahrilnet/da33b3e85494535bfc1576f3302e3a61 to your computer and use it in GitHub Desktop.
Save shahrilnet/da33b3e85494535bfc1576f3302e3a61 to your computer and use it in GitHub Desktop.
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