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