Last active
June 8, 2024 07:46
-
-
Save AmunRha/169d79eaa31bf9cbbe5642e31e594c67 to your computer and use it in GitHub Desktop.
This gist contains all the files required to solve the challenge 2k from redpwnctf21
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# 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() |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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}") |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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() |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment