z3_avr_solver.py

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()