This gist contains all the files required to solve the challenge 2k from redpwnctf21

2k_disassembler.py

# helper is a custom helper script containing parse, opcode desc, etc
from helper import *

rsp = []
ctr1 = 0
v13 = 0
dctr = 0
ii=0
data = [0]*100
op_desc = OPCODE_DESC
output = []
bbl = []
tbbl = []
inp = [112, 66, 55, 51, 56, 49, 53, 48, 114, 72, 116, 54, 48, 55, 49, 52, 78, 80, 53, 48, 49, 115, 57, 50, 52, 50, 48, 71, 51, 120, 85, 89, 48, 49, 51, 59, 87, 111, 123, 61, 54, 57, 104, 52, 50, 79, 98, 55, 51, 54, 66, 49, 121, 123, 64, 63, 49, 48, 52, 55, 117, 119, 96, 54]
# pB738150rHt60714NP501s92420G3xUY013;Wo{=69h42Ob736B1y{@?1047uw`6
# SB286354UtH61740ce103:6242A30?I7013XJycG69B/2kF=:/h;MOtK1042SU:|
# flag = "flag{kenken_is_just_z3_064c4}"

f = open('prog.bin','rb').read()
dump_len = len(f)


def extract(op,rsp,ctr1):
    global bbl
    global tbbl

    if ctr1 >= 0x2a3c:
        tbbl.append((op, ctr1))
    if op == 0x32 and len(rsp) == 2 and rsp[-1] == 0x4:
        bbl.append(tbbl[:-2])
        tbbl = []


def disasm(op, c):
    global rsp
    global ctr1
    global v13
    global dctr
    global ii
    global data
    global inp
    global output
    global n

    if c > dump_len:
        return -1

    print(f"\n[{hex(op):<3}]:[{hex(c):<3}]\t")
    # print("MOV dctr, ctr1+1")
    print(op_desc[op]+'\n')

    extract(op,rsp,ctr1)

    dctr = ctr1 + 1
    if op == 0x1:
        rsp.append(rsp[-1])
        ctr1+=1

    elif op == 0x2:
        rsp = rsp[:-1]
        ctr1+=1
        
    elif op == 0x3:
        if rsp[-1] == -1:
            rsp = rsp[:-1]
            ctr1+=1
        elif rsp[-1] != 0:
            print(f"[+] RETURN: {rsp[-1]}")
            return -1
        else:
            print("[+] READING FLAG FILE")
            return 1
        
    elif op == 0x10:
        rsp[-2] = rsp[-1] + rsp[-2]
        rsp = rsp[:-1]
        ctr1+=1
        
    elif op == 0x11:
        rsp[-2] = rsp[-1] - rsp[-2]
        rsp = rsp[:-1]
        ctr1+=1
        
    elif op == 0x12:
        rsp[-2] = rsp[-1] * rsp[-2]
        rsp = rsp[:-1]
        ctr1+=1
          
    elif op == 0x13:
        rsp[-2] = rsp[-1] // rsp[-2]
        rsp = rsp[:-1]
        ctr1+=1
        
    elif op == 0x14:
        rsp[-2] = rsp[-1] % rsp[-2]
        rsp = rsp[:-1]
        ctr1+=1
        
    elif op == 0x15:
        tmp = rsp[-1]
        rsp.pop(-1)
        res = rsp[-2]*rsp[-1]%tmp
        rsp = rsp[:-2]
        rsp.append(res)
        ctr1 = dctr
        
    elif op == 0x16:
        rsp[-2] = 1 if rsp[-1] == rsp[-2] else 0
        ctr1+=1
        rsp = rsp[:-1]
        
    elif op == 0x17:
        if rsp[-1] < 0:
            rsp[-1] = -1
        elif rsp[-1] > 0:
            rsp[-1] = 1
        ctr1+=1
        
    elif op == 0x20:
        rsp.append(inp[ii])
        ii+=1
        ctr1 = dctr
        
    elif op == 0x21:
        v30 = rsp[-1]
        rsp = rsp[:-1]
        ctr1 = dctr
        print(chr(v30))
        output.append(v30)
        
    elif op == 0x22:
        ctr1+=3
        rsp.append((f[dctr+1]<<8) | f[dctr])
        
    elif op == 0x30:
        v30 = rsp.pop(-1)
        ctr1 = abs(v30)
        
    elif op == 0x31:
        if rsp[-2] != 0:    #  Adjust/Remove the condition in order to extract
            rsp = rsp[:-2]  #  all equations with test input
            ctr1+=1         #  Keep it if using valid input
        else:
            ctr1 = rsp[-1]
            rsp = rsp[:-2]
        
    elif op == 0x32:
        if rsp[-2] != 0:     #  Adjust/Remove the condition in order to extract
            ctr1 = rsp[-1]   #  all equations with test input
            rsp = rsp[:-2]   #  Keep it if using valid input
        else:
            rsp = rsp[:-2]
            ctr1+=1
        
    elif op == 0x33:
        if rsp[-2] < 0:
            ctr1 = rsp[-1]
            rsp = rsp[:-2]
        else:
            rsp = rsp[:-2]
            ctr1+=1
        
    elif op == 0x34:
        if rsp[-2] <= 0:
            rsp = rsp[:-2]
            ctr1+=1
        else:
            ctr1 = rsp[-1]
            rsp = rsp[-2]
        
    elif op == 0x35:
        if rsp[-2] > 0:
            rsp = rsp[:-2]
            ctr1+=1
        else:
            ctr1 = rsp[-1]
            rsp = rsp[-2]
        
    elif op == 0x36:
        if rsp[-2] >= 0:
            ctr1 = rsp[-1]
            rsp = rsp[:-2]
        else:
            rsp = rsp[:-2]
            ctr1+=1
        
    elif op == 0x40:
        v33 = rsp.pop(-1)
        data[v13] = v33
        ctr1 = dctr
        
    elif op == 0x41:
        ctr1+=1
        rsp.append(data[v13])
        
    elif op == 0x50:
        v13+=1
        ctr1+=1
        
    elif op == 0x51:
        v13-=1
        ctr1+=1
        
    elif op == 0x52:
        v13 = (rsp[-1]+v13) & 0xff
        ctr1+=1
        rsp = rsp[:-1]
        
    elif op == 0x53:
        v13 = (v13 - rsp[-1]) & 0xff
        ctr1+=1
        rsp = rsp[:-1]
            
    else:
        print(f"""[!] UNKNOWN OPCODE: {hex(op)}""", end='')
        return -1

    # print_stack(rsp)
    # print_data(data)
    # print_reg(v13,ctr1,dctr,ii)
    return ctr1


def main():
    i=0
    while i < len(f):
        res = disasm(f[i],i)
        if res == -1:
            print("[!] ERROR")
            break
        if res == 1:
            print("[+] SUCCESS!")
            break
        i = res

    equations = parse(bbl,f)

    print("\n---------------------\n")
    print("[*] Extracted equations:\n")
    print(equations)    # Pass the dictionary to z3_solver.py


main()

helper.py

OPCODE_DESC = {
0x1:  """PUSH [rsp-1]
INC ctr1""",
0x2:  """POP
INC ctr1""",
0x3:  """IF [rsp-1] == 0
    READ FLAG""",
0x10: """ADD [rsp-2], [rsp-1]+[rsp-2]
    DEC rsp
    INC ctr1""",
0x11: """SUB [rsp-2], [rsp-1]-[rsp-2]
DEC rsp
INC ctr1""",
0x12: """MUL [rsp-2], [rsp-1]*[rsp-2]
DEC rsp
INC ctr1""",
0x13: """DIV [rsp-2], [rsp-1]/[rsp-2]
DEC rsp
INC ctr1""",
0x14: """MOD [rsp-2], [rsp-1]%[rsp-2]
DEC rsp
INC ctr1""",
0x15: """POP tmp1
POP tmp2
POP tmp3
MOV res, tmp3*tmp2%tmp1
PUSH res""",
0x16: """MOV [rsp-2], [rsp-1] == [rsp-2]
DEC rsp
INC ctr1""",
0x17: """IF [rsp-1] < 0:
    MOV [rsp-1], -1
ELIF [rsp-1] > 0:
    MOV [rsp-1], 1
INC ctr1""",
0x20: """PUSH getc(stdin)
ctr1 = dctr""",
0x21: """POP v30
IF v30 > 0xFF
    exit()
print(v30)
MOV ctr1, dctr""",
0x22: """IF dctr+2 >= size
    exit()
PUSH word data[dctr]
ADD ctr1, ctr1+3""",
0x30: """POP word v31
MOV ctr1, abs(v31)""",
0x31: """IF [rsp-2] != 0:
    MOV rsp, rsp-2
ctr1 = [rsp-1]
MOV rsp, rsp-2""",
0x32: """IF [rsp-2] !=0:
    ctr1 = [rsp-1]
    MOV rsp, rsp-2
MOV rsp, rsp-2""",
0x33: """IF [rsp-2]<0:
    ctr1 = [rsp-1]
    MOV rsp, rsp-2
MOV rsp, rsp-2""",
0x34: """IF [rsp-2]<=0:
    MOV rsp, rsp-2
ctr1 = [rsp-1]
MOV rsp, rsp-2""",
0x35: """IF [rsp-2]>0:
    MOV rsp, rsp-2
ctr1 = [rsp-1]
MOV rsp, rsp-2""",
0x36: """IF [rsp-2]>=0:
    ctr1 = [rsp-1]
    MOV rsp, rsp-2
MOV rsp, rsp-2""",
0x40: """POP v34
MOV [data[v13]], v34
MOV ctr1, dctr""",
0x41: """PUSH [data[v13]]
MOV ctr1, dctr""",
0x50: """INC v13
INC ctr1""",
0x51: """DEC v13
INC ctr1""",
0x52: """POP tmp0
MOV v13, tmp0+v13
INC ctr1""",
0x53: """POP tmp0
MOV v13, v13-tmp0
INC ctr1"""
}


equations = {"add_2":[], "add_3":[], "equate_3": [], "equate_4":[], "mod_equate_2":[], "sub_2":[], "equal_2":[]}


def parse(bbl, f):
    PUSH_OPERAND = [0x22, 0x52, 0x41]
    SUB_2 = (16,2)
    EQUATE_3 = (21,3)
    EQUATE_4 = (28,4) 
    ADD_2 = (13,2)
    ADD_3 = (19,3)
    MOD_EQUATE_2 = (64,2)
    EQUAL_2 = (7,2)

    for llist in bbl:
        eq = []
        bbl_len = len(llist)

        i = 1
        while True:
            if i+2 >= bbl_len:
                break
            if [llist[i][0],llist[i+1][0],llist[i+2][0]] == PUSH_OPERAND:
                ctr = llist[i][1]
                res = f[ctr+1]
                eq.append(res)
                i+=3
            i+=1
        ctr = llist[0][1]
        res = [f[ctr+1]]
        if bbl_len == SUB_2[0]:
            eq = eq[:SUB_2[1]] + res
            equations["sub_2"].append(eq)
        elif bbl_len == EQUATE_3[0]:
            eq = eq[:EQUATE_3[1]] + res
            equations["equate_3"].append(eq)
        elif bbl_len == EQUATE_4[0]:
            eq = eq[:EQUATE_4[1]] + res
            equations["equate_4"].append(eq)
        elif bbl_len == ADD_2[0]:
            eq = eq[:ADD_2[1]] + res
            equations["add_2"].append(eq)
        elif bbl_len == ADD_3[0]:
            eq = eq[:ADD_3[1]] + res
            equations["add_3"].append(eq)
        elif bbl_len == MOD_EQUATE_2[0]:
            eq = eq[:MOD_EQUATE_2[1]] + res
            equations["mod_equate_2"].append(eq)
        elif bbl_len == EQUAL_2[0]:
            eq = eq[:EQUAL_2[1]] + res
            equations["equal_2"].append(eq)
    return equations

def print_stack(rsp):
    print("[*] STACK:")
    print([hex(i) for i in rsp])

def print_data(data):
    print("[*] DATA:")
    print([hex(i) for i in data if i != 0])

def print_reg(v13,ctr1,dctr,ii):
    print("[*] REG:")
    print(f"v13: {v13}, ctr1:{ctr1}, dctr:{dctr}, ii:{ii}")

z3_solver.py

from z3 import *

off = [(0, 1),(0, 8),(0, 2),(0, 16),(1, 2),(8, 16),(0, 3),(0, 24),(1, 3),(8, 24),(2, 3),(16, 24),(0, 4),(0, 32),(1, 4),(8, 32),(2, 4),(16, 32),(3, 4),(24, 32),(0, 5),(0, 40),(1, 5),(8, 40),(2, 5),(16, 40),(3, 5),(24, 40),(4, 5),(32, 40),(0, 6),(0, 48),(1, 6),(8, 48),(2, 6),(16, 48),(3, 6),(24, 48),(4, 6),(32, 48),(5, 6),(40, 48),(0, 7),(0, 56),(1, 7),(8, 56),(2, 7),(16, 56),(3, 7),(24, 56),(4, 7),(32, 56),(5, 7),(40, 56),(6, 7),(48, 56),(8, 9),(1, 9),(8, 10),(1, 17),(9, 10),(9, 17),(8, 11),(1, 25),(9, 11),(9, 25),(10, 11),(17, 25),(8, 12),(1, 33),(9, 12),(9, 33),(10, 12),(17, 33),(11, 12),(25, 33),(8, 13),(1, 41),(9, 13),(9, 41),(10, 13),(17, 41),(11, 13),(25, 41),(12, 13),(33, 41),(8, 14),(1, 49),(9, 14),(9, 49),(10, 14),(17, 49),(11, 14),(25, 49),(12, 14),(33, 49),(13, 14),(41, 49),(8, 15),(1, 57),(9, 15),(9, 57),(10, 15),(17, 57),(11, 15),(25, 57),(12, 15),(33, 57),(13, 15),(41, 57),(14, 15),(49, 57),(16, 17),(2, 10),(16, 18),(2, 18),(17, 18),(10, 18),(16, 19),(2, 26),(17, 19),(10, 26),(18, 19),(18, 26),(16, 20),(2, 34),(17, 20),(10, 34),(18, 20),(18, 34),(19, 20),(26, 34),(16, 21),(2, 42),(17, 21),(10, 42),(18, 21),(18, 42),(19, 21),(26, 42),(20, 21),(34, 42),(16, 22),(2, 50),(17, 22),(10, 50),(18, 22),(18, 50),(19, 22),(26, 50),(20, 22),(34, 50),(21, 22),(42, 50),(16, 23),(2, 58),(17, 23),(10, 58),(18, 23),(18, 58),(19, 23),(26, 58),(20, 23),(34, 58),(21, 23),(42, 58),(22, 23),(50, 58),(24, 25),(3, 11),(24, 26),(3, 19),(25, 26),(11, 19),(24, 27),(3, 27),(25, 27),(11, 27),(26, 27),(19, 27),(24, 28),(3, 35),(25, 28),(11, 35),(26, 28),(19, 35),(27, 28),(27, 35),(24, 29),(3, 43),(25, 29),(11, 43),(26, 29),(19, 43),(27, 29),(27, 43),(28, 29),(35, 43),(24, 30),(3, 51),(25, 30),(11, 51),(26, 30),(19, 51),(27, 30),(27, 51),(28, 30),(35, 51),(29, 30),(43, 51),(24, 31),(3, 59),(25, 31),(11, 59),(26, 31),(19, 59),(27, 31),(27, 59),(28, 31),(35, 59),(29, 31),(43, 59),(30, 31),(51, 59),(32, 33),(4, 12),(32, 34),(4, 20),(33, 34),(12, 20),(32, 35),(4, 28),(33, 35),(12, 28),(34, 35),(20, 28),(32, 36),(4, 36),(33, 36),(12, 36),(34, 36),(20, 36),(35, 36),(28, 36),(32, 37),(4, 44),(33, 37),(12, 44),(34, 37),(20, 44),(35, 37),(28, 44),(36, 37),(36, 44),(32, 38),(4, 52),(33, 38),(12, 52),(34, 38),(20, 52),(35, 38),(28, 52),(36, 38),(36, 52),(37, 38),(44, 52),(32, 39),(4, 60),(33, 39),(12, 60),(34, 39),(20, 60),(35, 39),(28, 60),(36, 39),(36, 60),(37, 39),(44, 60),(38, 39),(52, 60),(40, 41),(5, 13),(40, 42),(5, 21),(41, 42),(13, 21),(40, 43),(5, 29),(41, 43),(13, 29),(42, 43),(21, 29),(40, 44),(5, 37),(41, 44),(13, 37),(42, 44),(21, 37),(43, 44),(29, 37),(40, 45),(5, 45),(41, 45),(13, 45),(42, 45),(21, 45),(43, 45),(29, 45),(44, 45),(37, 45),(40, 46),(5, 53),(41, 46),(13, 53),(42, 46),(21, 53),(43, 46),(29, 53),(44, 46),(37, 53),(45, 46),(45, 53),(40, 47),(5, 61),(41, 47),(13, 61),(42, 47),(21, 61),(43, 47),(29, 61),(44, 47),(37, 61),(45, 47),(45, 61),(46, 47),(53, 61),(48, 49),(6, 14),(48, 50),(6, 22),(49, 50),(14, 22),(48, 51),(6, 30),(49, 51),(14, 30),(50, 51),(22, 30),(48, 52),(6, 38),(49, 52),(14, 38),(50, 52),(22, 38),(51, 52),(30, 38),(48, 53),(6, 46),(49, 53),(14, 46),(50, 53),(22, 46),(51, 53),(30, 46),(52, 53),(38, 46),(48, 54),(6, 54),(49, 54),(14, 54),(50, 54),(22, 54),(51, 54),(30, 54),(52, 54),(38, 54),(53, 54),(46, 54),(48, 55),(6, 62),(49, 55),(14, 62),(50, 55),(22, 62),(51, 55),(30, 62),(52, 55),(38, 62),(53, 55),(46, 62),(54, 55),(54, 62),(56, 57),(7, 15),(56, 58),(7, 23),(57, 58),(15, 23),(56, 59),(7, 31),(57, 59),(15, 31),(58, 59),(23, 31),(56, 60),(7, 39),(57, 60),(15, 39),(58, 60),(23, 39),(59, 60),(31, 39),(56, 61),(7, 47),(57, 61),(15, 47),(58, 61),(23, 47),(59, 61),(31, 47),(60, 61),(39, 47),(56, 62),(7, 55),(57, 62),(15, 55),(58, 62),(23, 55),(59, 62),(31, 55),(60, 62),(39, 55),(61, 62),(47, 55),(56, 63),(7, 63),(57, 63),(15, 63),(58, 63),(23, 63),(59, 63),(31, 63),(60, 63),(39, 63),(61, 63),(47, 63),(62, 63),(55, 63)]

f = [BitVec(f"flag_{i}", 24) for i in range(64)]
s = Solver()

def set_idx(set_to):
    for i in set_to:
        s.add(f[i[0]] == i[1])

def sub2(s_list):
    for i in s_list:
        s.add(f[i[1]] - f[i[0]] == i[2])

def add2(a2_list):
    for i in a2_list:
        s.add(f[i[0]]+f[i[1]] == i[2])

def add3(a3_list):
    for i in a3_list:
        s.add(f[i[0]]+f[i[1]]+f[i[2]] == i[3])

def equate3(e3_list):
    for i in e3_list:
        res = (f[i[2]]*f[i[1]])%0x7fff
        s.add((f[i[0]]*res)%0x7fff == i[3])

def equate4(e4_list):
    for i in e4_list:
        res = (f[i[3]]*f[i[2]])%0x7fff
        res = (f[i[1]]*res)%0x7fff
        s.add((f[i[0]]*res)%0x7fff == i[4])

def mod_equate2(m2_list):
    for i in m2_list:
        s.add((f[i[1]] % f[i[0]]) * (f[i[0]] % f[i[1]]) == 0)
        s.add(f[i[0]] != f[i[1]]) 
        s.add(UDiv((UDiv(f[i[1]], f[i[0]]) + UDiv(f[i[0]], f[i[1]])),1) == i[2])

def distinct_add():
    for i in off:
        s.add(f[i[0]] != f[i[1]])

def set_range():
    for i in range(64):
        s.add(f[i]+0x2f > 0x2f, f[i]+0x2f <= 127)


equations = {'add_2': [[2, 3, 12], [14, 22, 12], [33, 41, 12]],
 'add_3': [[4, 5, 6, 17], [12, 20, 28, 7], [43, 51, 59, 15], [48, 49, 57, 12]],
 'equate_3': [[1, 9, 10, 8], [7, 15, 23, 15], [18, 26, 27, 144]],
 'equate_4': [[35, 36, 37, 45, 30]],
 'mod_equate_2': [[30, 38, 2],[31, 39, 3],[42, 50, 3],[46, 54, 3],[47, 55, 2],[62, 63, 7]],
 'sub_2': [[0, 8, 2], [16, 17, 2], [21, 29, 5], [52, 53, 2], [60, 61, 2]],
 'equal_2': [[11, 7],[13, 8],[19, 1],[24, 5],[25, 3],[32, 1],[34, 4],[40, 7],[44, 3],[56, 2],[58, 5]]}

def main():
    set_range()
    distinct_add()
    set_idx(equations['equal_2'])
    sub2(equations['sub_2'])
    add2(equations['add_2'])
    add3(equations['add_3'])
    equate3(equations['equate_3'])
    equate4(equations['equate_4'])
    mod_equate2(equations['mod_equate_2'])

    print(s.check())
    m = s.model()
    flag = [(int(str(m[f[i]]), 0)+0x2f & 0xff) for i in range(len(m))]
    print(flag)
    print(''.join([chr(i) for i in flag]))  # Pass the output to solve.py


main()