Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
import serial
from z3 import *
def read_until(serial, until):
out = ''
while until not in out:
out += serial.read(1)
return out
def get_password():
value = [BitVec('i_%i' % i,8) for i in range(13)]
s = Solver()
s.add(value[7] + value[8] == 0xd3)
s.add(value[8] * value[9] == 0x15c0)
s.add(value[0] * value[1] == 0x13b7)
s.add(value[2] * value[3] == 0x1782)
s.add(value[3] + value[4] == 0x92)
s.add(value[6] * value[7] == 0x2b0c)
s.add(value[5] + value[6] == 0xa5)
s.add(value[9] + value[10] == 0x8f)
s.add(value[1] + value[2] == 0xa7)
s.add(value[10] * value[11] == 0x2873)
s.add(value[12] * 13 == 0x297)
s.add(value[4] * value[5] == 0x122f)
s.add(value[11] + value[12] == 0xa0)
for x in range(13):
s.add(value[x] >= 0)
s.check()
m = s.model()
output = []
for x in value:
output.append(chr(int(m[x].as_long())))
passw = ''.join(output)
print("[+] Found Password: " + passw)
return passw
def main():
ser = serial.Serial("/dev/ttyUSB0", 19200, timeout=0.1)
passw = get_password()
input = read_until(ser, "Input:")
print("[!] Sending input to driver...")
ser.write(passw + '\r')
for i in range(2):
flag = ser.readline()
print(flag)
ser.close()
if __name__ == '__main__':
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment