Locksmith Solution - Security Fest 2019

locksmith_solve.py

from pwn import *
from z3 import *
import re
import time

def get_solution(diff):
        print diff
        s = Solver()

        a = Int('a')
        b = Int('b')
        c = Int('c')
        d = Int('d')
        e = Int('e')
        f = Int('f')
        g = Int('g')
        h = Int('h')
        i = Int('i')

        s.add(a >= 0)
        s.add(a <= 50)
        s.add(b >= 0)
        s.add(b <= 50)
        s.add(c >= 0)
        s.add(c <= 50)
        s.add(d >= 0)
        s.add(d <= 50)
        s.add(e >= 0)
        s.add(e <= 50)
        s.add(f >= 0)
        s.add(f <= 50)
        s.add(g >= 0)
        s.add(g <= 50)
        s.add(h >= 0)
        s.add(h <= 50)
        s.add(i >= 0)
        s.add(i <= 50)

        print "The equations are:"

        for item in range(len(diff)):
                t = diff[item]
                equation = str(initial[item]) + " + "
                for j in range(len(t)):
                        equation += str(t[j]) + " * " + coefficients[j] + " + "
                sol = equation[:-3]
                sol += " == " + str(target_value)
                print sol
                F = eval(sol)
                s.add(F)

        print s.check()
        m = s.model()

        freq = []

        freq.append(m[a].as_long())
        freq.append(m[b].as_long())
        freq.append(m[c].as_long())
        freq.append(m[d].as_long())
        freq.append(m[e].as_long())
        freq.append(m[f].as_long())
        freq.append(m[g].as_long())
        freq.append(m[h].as_long())
        freq.append(m[i].as_long())

        print "Solution is: "
        print freq

        return freq

if __name__ == "__main__":
        p = remote("locksmith-01.pwn.beer",31337)

        time.sleep(1)
        p.recv()

        rounds = 0

        while True:
                print "Round number: %d" %(rounds)
                p.sendline("0")
                time.sleep(0.2)
                d = p.recv()
                base = []
                target = []

                m = re.findall(r'0m   (.*)?    |\n', d)
                initial = m[1].split()
                target = m[3].split()

                base = initial
                print "The initial array is: "
                print initial
                print "The target array is: "
                print target
                target_value = int(target[0])
                print "The desired target value is: %d" %(target_value)

                diff = [[], [], [], [], [], [], [], [], []]
                coefficients = list('abcdefghi')

                for i in range(1, 10):
                        p.sendline(str(i))
                        time.sleep(0.3)
                        d = p.recv()
                        m = re.findall(r'0m   (.*)?    |\n', d)
                        new = m[1].split()
                        new
                        for j in range(len(new)):
                                diff[j].append(int(new[j]) - int(base[j]))
                        base = new

                p.sendline("0")

                print "Fetching the solution"

                freq = get_solution(diff)

                for i in range(9):
                        count = freq[i]
                        if count != 0:
                                for j in range(count):
                                        print "Sending option: %d" %(i+1)
                                        p.sendline(str(i+1))
                                        p.recv()

                p.sendline("0")
                time.sleep(0.1)
                if rounds > 90:
                        print p.recv()
                else:
                        p.recv()
                rounds += 1