Skip to content

Instantly share code, notes, and snippets.

@jasperla
Created June 28, 2020 12:13
Show Gist options
  • Save jasperla/e358e24f5c42cfd74533d03ba552e60e to your computer and use it in GitHub Desktop.
Save jasperla/e358e24f5c42cfd74533d03ba552e60e to your computer and use it in GitHub Desktop.
#!/usr/bin/env python3
#
# https://z3prover.github.io/api/html/namespacez3py.html
# https://ericpony.github.io/z3py-tutorial/guide-examples.htm
import sys
from z3 import *
def add_constraints(solver, badbytes, *vars):
for v in vars:
# Ensure the parameters are within ASCII range
solver.add(v > 0)
solver.add(v < 0x80)
# Also weed out any badbytes
[solver.add(v != b) for b in badbytes]
def z3_model_solve(solver, badbytes, *vars):
add_constraints(solver, badbytes, *vars)
solver.check()
try:
model = solver.model()
results = {}
for v in vars:
results[v] = model[v].as_long()
return results
except Z3Exception:
return None
def z3_model_2(byte, badbytes):
x, y = Ints('x y')
s = Solver()
s.add(x + y == byte)
m = z3_model_solve(s, badbytes, x, y)
if m:
print(f'{hex(byte)} solved: ', end='')
print(m)
return True
else:
return None
def z3_model_3(byte, badbytes):
x, y, z = Ints('x y z')
s = Solver()
s.add(x + y + z == byte)
m = z3_model_solve(s, badbytes, x, y, z)
if m:
print(f'{hex(byte)} solved: ', end='')
print(m)
return True
else:
return None
def main():
badbytes = [0x00, 0x14, 0x15, 0x30]
byte = 0xff
if not z3_model_2(byte, badbytes):
print(f'{hex(byte)} not solvable with two parameters; attempting with three')
z3_model_3(byte, badbytes)
if __name__ == '__main__':
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment