Disclaimer
- This is a copy of my direct message in discord, to someone who asked me about the solution of vvvmmm
- I'm not a native English speaker. I'm trying my best but maybe there's something that is not explained well. Sorry!
- Updated: Added full code of
chal.pyandstackvm.py
Long version (Japanese):
Content
There are 2 files in this challenge.
IDA can't analyze either of them so I quickly searched up about .tbc extension
After seaching for a while, I found this writeup
This writeup explains what tbc files are, how to decompile them, and how to read tcl bytecodes.
As in this writeup, tbc files are obfuscated program in tcl, a scripting language.
They can be disassembled by a tool called 'tbcload'.
I followed the same steps as him, using tbcload-windows-amd64.exe decompile --detail chal.tbc to generate disassembly of chal.tbc
Now its time to read tcl bytecode instructions.
For bytecode information, I referenced this webpage.
I don't know if I should explain every single bytecode used in this program here,
because I want this to be simplified version of my upcoming writeup.
After analyzing bytecodes, I created same VM in python as 'chal.py'
I also implemented a function to disassemble the entire 'code.bin' file.
chal.py
INPUT = "fwectf{789012345678901234567890123456789012345678901234567890123456789012345}\n"
#-----Start VM Code---------------------------------------------------
input_pointer = 0 #Not in the original code
data = b""
with open("code.bin", "rb") as f:
data = f.read()
length = len(data)
code = []
for i in range(0, length, 5):
end = i + 5
if end >= length: end = length - 1
chunk = data[i:end]
code.append(chunk)
memory = []
for i in range(0, 0x1000):
memory.append(0)
ip = 0x1000 - 1
sp = 0x1000 - 2
call_stack = []
terminate = False
def get_mem(idx:int):
return memory[idx]
def set_mem(idx:int, val:object):
memory[idx] = val
def split_inst(line: bytes):
res = []
if len(line) < 2: return
opbyte = chr(line[0])
a = to_short_int_big(line[1:3])
b = to_short_int_big(line[3:5])
res.append(opbyte)
res.append(a)
res.append(b)
return res
def to_short_int_big(bytes_array:bytes):
return int("0x" + bytes_array.hex(), base=0)
def arg_int(inst: list, idx: int, line: str):
if len(inst) <= idx:
print("Error: not enough args for instruction:" + line)
exit(1)
return inst[idx]
def run_opcode(opcode: str, args:list, line_str:str):
global call_stack
global terminate
global input_pointer
if opcode == 'a':
#Receive 1 char(Modified)
#I modified this oparation so that I don't have to send a character one by one manually
ch = INPUT[input_pointer]
input_pointer += 1
if (len(ch) == 0):
set_mem(0, 10) #\n
else:
set_mem(0, ord(ch[0]))
elif opcode == 'b':
#Print 1 char
print(chr(get_mem(0)), end="")
elif opcode == 'c':
#Assign
reg = arg_int(args, 1, line_str)
val = arg_int(args, 2, line_str)
set_mem(reg, val)
elif opcode == 'd':
#push
val = arg_int(args, 1, line_str)
sp_val = get_mem(sp)
set_mem(sp_val, val)
set_mem(sp, sp_val+1)
elif opcode == 'e':
#pushReg
reg = arg_int(args, 1, line_str)
sp_val = get_mem(sp)
val = get_mem(reg)
set_mem(sp_val, val)
set_mem(sp, sp_val+1)
elif opcode == 'f':
#poptoReg
reg = arg_int(args, 1, line_str)
sp_val = get_mem(sp)
sp_val -= 1
set_mem(sp, sp_val)
val = get_mem(sp_val)
set_mem(reg, val)
elif opcode == 'g':
#AssignReg
reg1 = arg_int(args, 1, line_str)
reg2 = arg_int(args, 2, line_str)
val = get_mem(reg2)
set_mem(reg1, val)
elif opcode == 'h':
#Addition
reg = arg_int(args, 1, line_str)
val = arg_int(args, 2, line_str)
old = get_mem(reg)
set_mem(reg, old + val)
elif opcode == 'i':
#Substraction
reg = arg_int(args, 1, line_str)
val = arg_int(args, 2, line_str)
old = get_mem(reg)
set_mem(reg, old - val)
elif opcode == 'j':
#Divition
reg = arg_int(args, 1, line_str)
val = arg_int(args, 2, line_str)
if val == 0: print("Division by zero")
old = get_mem(reg)
set_mem(reg, int(old / val))
elif opcode == 'k':
#Multiply
reg = arg_int(args, 1, line_str)
val = arg_int(args, 2, line_str)
old = get_mem(reg)
set_mem(reg, old * val)
elif opcode == 'l':
#Modulo
reg = arg_int(args, 1, line_str)
val = arg_int(args, 2, line_str)
if val == 0: print("Modulo by zero")
old = get_mem(reg)
set_mem(reg, old % val)
elif opcode == 'm':
#Addition(Refs)
r1 = arg_int(args, 1, line_str)
r2 = arg_int(args, 2, line_str)
v1 = get_mem(r1)
v2 = get_mem(r2)
set_mem(r1, v1+v2)
elif opcode == 'n':
#Substraction(Refs)
r1 = arg_int(args, 1, line_str)
r2 = arg_int(args, 2, line_str)
v1 = get_mem(r1)
v2 = get_mem(r2)
set_mem(r1, v1-v2)
elif opcode == 'o':
#Divition(Refs)
r1 = arg_int(args, 1, line_str)
r2 = arg_int(args, 2, line_str)
v1 = get_mem(r1)
v2 = get_mem(r2)
if v2 == 0: print("Division by zero")
set_mem(r1, int(v1/v2))
elif opcode == 'p':
#Multiply(Refs)
r1 = arg_int(args, 1, line_str)
r2 = arg_int(args, 2, line_str)
v1 = get_mem(r1)
v2 = get_mem(r2)
set_mem(r1, v1*v2)
elif opcode == 'q':
#Modulo(Refs)
r1 = arg_int(args, 1, line_str)
r2 = arg_int(args, 2, line_str)
v1 = get_mem(r1)
v2 = get_mem(r2)
if v2 == 0: print("Modulo by zero")
set_mem(r1, v1%v2)
elif opcode == 'r':
#load
addr = arg_int(args, 1, line_str)
val = get_mem(addr)
val2 = get_mem(val)
set_mem(addr, val2)
elif opcode == 's':
#loadinto
addr = arg_int(args, 1, line_str)
reg = arg_int(args, 2, line_str)
val = get_mem(reg)
addr_val = get_mem(addr)
set_mem(addr_val, val)
elif opcode == 't':
#return
if len(call_stack) == 0: terminate = True; return
ret = call_stack[-1]
call_stack = call_stack[0:-1]
set_mem(ip, ret)
elif opcode == 'u':
#call
call_stack.append(get_mem(ip))
target = arg_int(args, 1, line_str)
set_mem(ip, target)
elif opcode == 'v':
#jump if 0
reg = arg_int(args, 1, line_str)
target = arg_int(args, 2, line_str)
if (get_mem(reg) == 0):
set_mem(ip, target)
elif opcode == 'w':
#jump
target = arg_int(args, 1, line_str)
set_mem(ip, target)
else:
print("Invalid Instruction: " + opcode)
def run_VM():
while(not terminate):
cur_ip = get_mem(ip)
if (cur_ip >= len(code)):
break
line = code[cur_ip]
inst = split_inst(line)
if len(inst) == 0:
set_mem(ip, cur_ip+1)
continue
set_mem(ip, cur_ip+1)
op = inst[0]
# Get data from memory (doesn't trigger if length of flag is not 77)
# if cur_ip == 2230:
# with open("matrix_data.txt", "w") as g:
# stack_vm_cmd = memory[256:256+1233]
# stack_vm_data = memory[2816:3072]
# matrix = memory[1792:2417]
# g.write(str(matrix))
run_opcode(op, inst, line)
#-----End VM Code----------------------------------------------------------
#Create opcode info used in logging
#[name, arg_amount]
opcode_info = dict()
opcode_info['a'] = ["RecieveChar", 0]
opcode_info['b'] = ["PrintChar", 0]
opcode_info['c'] = ["Assign", 2]
opcode_info['d'] = ["Push", 1]
opcode_info['e'] = ["PushReg", 1]
opcode_info['f'] = ["PopToReg", 1]
opcode_info['g'] = ["AssignReg", 2]
opcode_info['h'] = ["Add", 2]
opcode_info['i'] = ["Sub", 2]
opcode_info['j'] = ["Div", 2]
opcode_info['k'] = ["Mul", 2]
opcode_info['l'] = ["Modulo", 2]
opcode_info['m'] = ["AddReg", 2]
opcode_info['n'] = ["SubReg", 2]
opcode_info['o'] = ["DivReg", 2]
opcode_info['p'] = ["MulReg", 2]
opcode_info['q'] = ["ModuloReg", 2]
opcode_info['r'] = ["Load", 1]
opcode_info['s'] = ["LoadInto", 2]
opcode_info['t'] = ["Return", 0]
opcode_info['u'] = ["Call", 1]
opcode_info['v'] = ["JumpIfZero", 2]
opcode_info['w'] = ["JumpTo", 1]
def disassemble_bin():
with open("assembly_list.txt", "w") as f:
i = 0
for opcode in code:
res = split_inst(opcode)
info = opcode_info.get(res[0])
if info:
if info[1] == 2:
f.write(f"Inst {i}: {info[0]}, {res[1]}, {res[2]}\n")
elif info[1] == 1:
f.write(f"Inst {i}: {info[0]}, {res[1]}\n")
else:
f.write(f"Inst {i}: {info[0]}\n")
else:
f.write(f"{res[0]}, {res[1]}, {res[2]}\n")
i += 1
if __name__ == '__main__':
#disassemble_bin()
run_VM()
disassembled result
Inst 0: Assign, 0, 102 #print "flag:"
Inst 1: PrintChar
Inst 2: Add, 0, 6
Inst 3: PrintChar
Inst 4: Sub, 0, 11
Inst 5: PrintChar
Inst 6: Add, 0, 6
Inst 7: PrintChar
Inst 8: Sub, 0, 45
Inst 9: PrintChar
Inst 10: Assign, 2816, 962
Inst 11: Assign, 2817, 962
Inst 12: Assign, 2818, 962
.....
Inst 2654: PrintChar
Now I can analyze what this code.bin executes in VM, its time to begin round 2, reading VM codes.
- Assign:
memory[arg[0]] = arg[1] - AssignReg:
memory[arg[0]] = memory[arg[1]] - Add:
memory[arg[0]] += arg[1] - Sub:
memory[arg[0]] -= arg[1] - Div:
memory[arg[0]] = int(memory[arg[0]] / arg[1]) - Mul:
memory[arg[0]] *= arg[1] - Modulo:
memory[arg[0]] %= arg[1] - AddReg:
memory[arg[0]] += memory[arg[1]] - SubReg:
memory[arg[0]] -= memory[arg[1]] - Div:
memory[arg[0]] = int(memory[arg[0]] / memory[arg[1]]) - MulReg:
memory[arg[0]] *= memory[arg[1]] - ModuloReg:
memory[arg[0]] %= memory[arg[1]] - Push:
memory[memory[sp]] = arg[0],memory[sp] += 1 - PushReg:
memory[memory[sp]] = memory[arg[0]],memory[sp] += 1 - PopToReg:
memory[sp] -= 1,memory[arg[0]] = memory[memory[sp]] - Load:
memory[arg[0]] = memory[memory[arg[0]]] - LoadInto:
memory[memory[arg[0]]] = memory[arg[1]] - Call:
call_stack.append(memory[ip])),memory[ip] = arg[0] - Return:
ret = call_stack.pop(),memory[ip] = ret. But if call stack is empty, terminate the program - JumpTo:
memory[ip] = arg[0] - JumpIfZero: If
memory[arg[1]]is0,memory[ip] = arg[0] - PrintChar:
print(chr(memory[0]), end="") - RecieveChar:
memory[0] = input()[0]. But if length of the input is 0,memory[0] = 10(\n, a newline character)
I will try to explain more in my upcoming write up
The funny thing is, there's another VM inside this.
Although this one is much simpler than the previous one, I was imtimidated when I saw this first time.
Now I know why this challenge is called "vvvmmm"
stackvm.py
loaded_addr = 0
calc_info = []
#array of [flag_index, modulo_by, matrix_index]
mod_seq = []
#----------------Start VM------------------------------------------
#from memory[256:256+1233]
cmds = [101, 119, 43, 538, 1920, 37, 120, 140, 151, 119, ...]
#from memory[2816:3072]
data = [962, 962, 962, 962, 962, 962, 962, ...]
def get_cmd():
global cmds
cmd = cmds[-1]
cmds = cmds[0:-1]
return cmd
def get_stack():
global stack
val = stack[-1]
stack = stack[0:-1]
return val
def exec_code(id, cmd):
global loaded_addr
global calc_info
global mod_seq
if id == 921:
#add
val1 = get_stack()
val2 = get_stack()
print(f"Add {val1}, {val2}, result={val1+val2}")
stack.append(val1+val2)
elif id == 926:
#sub
val1 = get_stack()
val2 = get_stack()
print(f"Sub {val1}, {val2}, result={val1-val2}")
stack.append(val1-val2)
elif id == 931:
#mul
val1 = get_stack()
val2 = get_stack()
print(f"Mul {val1}, {val2}, result={val1*val2}")
stack.append(val1*val2)
elif id == 936:
#div
val1 = get_stack()
val2 = get_stack()
if val2 == 0: print("Division by zero")
print(f"Div {val1}, {val2}, result={int(val1/val2)}")
stack.append(int(val1/val2))
elif id == 941:
#mod
val1 = get_stack()
val2 = get_stack()
if val2 == 0: print("Modulo by zero")
print(f"Mod {val1}, {val2}, result={val1%val2}")
stack.append(val1%val2)
#Log
calc_info.append(val2)
elif id == 952:
val1 = get_stack()
val2 = get_stack()
print(f"PopReg {val1}, {val2}")
#memory[val1] = val2
#Log
calc_info.append(val1-1792)
mod_seq.append(calc_info)
elif id == 956:
val1 = get_stack()
print(f"Load {val1}")
#stack.append(memory[val1])
stack.append(0)
#Log
loaded_addr = val1 - 12
calc_info = []
calc_info.append(loaded_addr)
elif id == 962:
#push
stack.append(cmd - 128)
print(f"Push {cmd - 128}")
else:
print(f"Invalid Code: {id}")
def run_VM():
while(len(cmds)):
cmd = get_cmd()
if cmd >= 256: exec_code(962, cmd) #push opcode
else: exec_code(data[cmd], cmd)
#-----------------------------------------------------------------------------------
if __name__ == '__main__':
run_VM()
with open("calc_infos.txt", "w") as f:
f.write(str(mod_seq))
After going through all of these, I finally reversed an entire program.
I uploaded equivalent program made in python as chal_no_vm.py
The goal is to modify matrix so that can pass verify function.
Each make_big_arr function will make 25x25 array from matrix in a certain way, and each value in an 25 integer array should be distinct to be verified.
chal_no_vm.py
#calc_infos.txt generated from stack.py
mod_seq = [[76, 25, 542], [76, 23, 536], [75, 25, 540], [75, 23, 133], [74, 25, 498], [74, 23, 29], [73, 25, 448], [73, 23, 355], [72, 25, 333], [72, 23, 550], [71, 25, 610], [71, 23, 173], [70, 25, 61], [70, 23, 432], [69, 25, 9], [69, 23, 166], [68, 25, 459], [68, 23, 100], [67, 25, 525], [67, 23, 226], [66, 25, 389], [66, 23, 95], [65, 25, 619], [65, 23, 132], [64, 25, 64], [64, 23, 262], [63, 25, 222], [63, 23, 203], [62, 25, 37], [62, 23, 593], [61, 25, 580], [61, 23, 433], [60, 25, 393], [60, 23, 124], [59, 25, 578], [59, 23, 307], [58, 25, 567], [58, 23, 595], [57, 25, 620], [57, 23, 40], [56, 25, 402], [56, 23, 179], [55, 25, 373], [55, 23, 605], [54, 25, 318], [54, 23, 352], [53, 25, 93], [53, 23, 289], [52, 25, 108], [52, 23, 92], [51, 25, 121], [51, 23, 181], [50, 25, 184], [50, 23, 251], [49, 25, 130], [49, 23, 544], [48, 25, 1], [48, 23, 576], [47, 25, 255], [47, 23, 477], [46, 25, 413], [46, 23, 446], [45, 25, 372], [45, 23, 84], [44, 25, 240], [44, 23, 10], [43, 25, 379], [43, 23, 243], [42, 25, 172], [42, 23, 73], [41, 25, 315], [41, 23, 41], [40, 25, 452], [40, 23, 418], [39, 25, 500], [39, 23, 47], [38, 25, 177], [38, 23, 269], [37, 25, 466], [37, 23, 57], [36, 25, 624], [36, 23, 568], [35, 25, 79], [35, 23, 478], [34, 25, 316], [34, 23, 592], [33, 25, 468], [33, 23, 537], [32, 25, 440], [32, 23, 309], [31, 25, 200], [31, 23, 388], [30, 25, 221], [30, 23, 288], [29, 25, 565], [29, 23, 136], [28, 25, 219], [28, 23, 97], [27, 25, 187], [27, 23, 517], [26, 25, 499], [26, 23, 343], [25, 25, 382], [25, 23, 514], [24, 25, 612], [24, 23, 489], [23, 25, 404], [23, 23, 292], [22, 25, 528], [22, 23, 411], [21, 25, 207], [21, 23, 535], [20, 25, 137], [20, 23, 559], [19, 25, 340], [19, 23, 359], [18, 25, 53], [18, 23, 324], [17, 25, 444], [17, 23, 604], [16, 25, 239], [16, 23, 114], [15, 25, 326], [15, 23, 55], [14, 25, 237], [14, 23, 329], [13, 25, 381], [13, 23, 518], [12, 25, 342], [12, 23, 38], [11, 25, 176], [11, 23, 69], [10, 25, 256], [10, 23, 599], [9, 25, 555], [9, 23, 490], [8, 25, 313], [8, 23, 391], [7, 25, 441], [7, 23, 182], [6, 25, 252], [6, 23, 180], [5, 25, 320], [5, 23, 344], [4, 25, 68], [4, 23, 56], [3, 25, 26], [3, 23, 232], [2, 25, 293], [2, 23, 589], [1, 25, 312], [1, 23, 505], [0, 25, 234], [0, 23, 410]]
#data from memory[1792:2417]
long_array = [23, -1, 6, 0, 8, 19, 4, 5, 14, -1, -1, 24, 21, 16, 17, 9, 13, 15, 12, 22, 11, 7, 10, 2, 18, 11, -1, 21, 16, -1, 9, 13, 15, 12, 22, 23, 7, -1, -1, 18, -1, -1, 6, 0, 8, 19, 4, -1, 14, 20, 9, 7, 10, -1, 18, -1, -1, -1, 0, 8, 19, -1, 5, 14, -1, 11, 24, 21, -1, -1, 23, 13, 15, -1, 22, 19, 4, 5, 14, -1, 11, 24, 21, 16, -1, 9, 13, 15, 12, 22, 23, 7, -1, -1, 18, -1, 1, -1, 0, 8, -1, 13, 15, 12, 22, 23, 7, 10, -1, 18, 11, 1, 6, 0, -1, 19, 4, 5, 14, 20, 9, -1, 21, 16, -1, 8, 23, 1, 6, 0, -1, 19, -1, -1, 14, 17, -1, -1, 21, 16, 22, 9, 13, 15, 12, 18, 11, 7, 10, 2, 17, 11, 24, 21, 16, 22, 9, 13, 15, 12, 18, 23, 7, 10, 2, 8, -1, 1, 6, 0, 20, 19, -1, -1, 14, 18, -1, -1, 10, -1, -1, -1, -1, 6, -1, 20, 19, -1, 5, 14, 17, 11, 24, 21, 16, 22, 23, 13, 15, 12, -1, 19, 4, -1, 14, 17, 11, -1, 21, 16, 22, 9, 13, 15, 12, 18, 23, 7, 10, -1, 8, -1, -1, 6, 0, 22, -1, 13, 15, 12, 18, 23, -1, 10, -1, 8, 11, -1, 6, -1, -1, 19, 4, -1, 14, 17, 9, 24, 21, 16, 2, -1, -1, 1, 10, -1, -1, 19, 4, 5, 0, 17, -1, 24, 6, 12, 22, 9, 13, -1, 16, 18, 11, 7, 21, 16, 17, 11, 24, 21, 12, 22, 9, 13, 15, 2, 18, 23, -1, -1, 0, 8, -1, -1, 6, 14, 20, 19, 4, 5, 12, 18, 9, 7, 15, 0, 8, -1, 1, -1, 14, 20, -1, -1, 5, -1, -1, 11, -1, 21, -1, 22, 23, 13, -1, 14, -1, 19, 4, -1, 16, 17, 11, -1, 21, 12, 22, 9, 13, 15, -1, 18, -1, -1, -1, 0, 8, 3, 1, 6, 0, 22, -1, 13, 6, -1, 18, 23, 7, -1, 16, 8, 11, 1, 21, 14, 20, 19, 4, 5, 12, 17, -1, -1, 15, 6, 2, 8, 23, -1, 5, -1, -1, 19, 4, 21, 0, 17, -1, -1, 15, -1, 22, -1, 13, 10, 16, 18, 11, 7, 21, 16, -1, 11, -1, 15, 12, 22, 9, 13, -1, -1, 18, -1, 7, 6, 0, 8, -1, 1, 5, 14, 20, 19, 4, 10, 12, 18, 9, 7, 6, 0, -1, -1, 1, 5, 14, 20, 19, 4, -1, -1, 17, 11, -1, 15, -1, 22, -1, 13, 5, 14, -1, 19, 4, 21, 16, 17, 11, -1, 15, 12, 22, 9, 13, 10, -1, 18, -1, 7, 6, 0, 8, 3, 1, 15, 0, -1, -1, 13, 10, 2, 18, 23, 7, 6, 16, 8, 11, -1, -1, 14, 20, 19, 4, 21, 12, 17, -1, -1, -1, 6, 2, 8, 23, -1, 5, 14, 20, 19, 24, 21, 0, 17, -1, 13, 15, -1, -1, 9, 7, 10, 16, 18, 11, -1, 21, 16, -1, 11, 13, 15, 12, 22, 9, -1, -1, -1, 18, 23, -1, 6, -1, 8, -1, 4, 5, 14, 20, 19, -1, 10, 12, 18, 9, -1, 6, 0, 8, -1, 4, 5, 14, 20, 19, -1, 21, -1, -1, 11, 13, 15, 2, 22, 23, 4, -1, 14, -1, 19, -1, 21, 16, 17, 11, 13, 15, 12, 22, -1, 7, 10, -1, -1, 23, -1, 6, 0, 8, -1, 13, 15, 0, 22, -1, -1, 10, 2, 18, 23, -1, 6, -1, 8, 11, 4, 5, 14, 20, -1, -1, 21, 12, 17, -1]
def make_matrix(array: list):
big_arr = []
for i in range(25):
arr = []
for j in range(25):
arr.append(array[i*25 + j])
big_arr.append(arr)
return big_arr
def make_matrix2(array: list):
big_arr = []
for i in range(25):
arr = []
for j in range(25):
arr.append(array[i + j*25])
big_arr.append(arr)
return big_arr
def make_matrix3(array: list):
big_arr = []
for i in range(5):
for j in range(5):
arr = []
val = 0
for k in range(25):
if k != 0 and k % 5 == 0:
val += 20
arr.append(array[i*5 + j*125 + k + val])
big_arr.append(arr)
return big_arr
def verify_arr(i: list):
for arr in i:
verify_arr = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
for index in arr:
verify_arr[index] = 1
for value in verify_arr:
if value == 0:
return False
return True
def fill_array_based_on_flag(flag: str):
for mods in mod_seq:
long_array[mods[2]] = ord(flag[mods[0]]) % mods[1]
if __name__ == '__main__':
flag = input("flag: ")
if len(flag) != 77:
print("Incorrect")
exit(1)
fill_array_based_on_flag(flag)
v1 = make_matrix(long_array)
v2 = make_matrix2(long_array)
v3 = make_matrix3(long_array)
if verify_arr(v1) and verify_arr(v2) and verify_arr(v3):
print("Correct")
else:
print("Incorrect")
solve_z3.py
from z3 import *
import hashlib
#list of [flag_index、modulo_by、array_index]
#question_array[array_index] = flag[flag_index] % modulo_by
mod_seq = [[76, 25, 542], [76, 23, 536], [75, 25, 540], [75, 23, 133], [74, 25, 498], [74, 23, 29], [73, 25, 448], [73, 23, 355], [72, 25, 333], [72, 23, 550], [71, 25, 610], [71, 23, 173], [70, 25, 61], [70, 23, 432], [69, 25, 9], [69, 23, 166], [68, 25, 459], [68, 23, 100], [67, 25, 525], [67, 23, 226], [66, 25, 389], [66, 23, 95], [65, 25, 619], [65, 23, 132], [64, 25, 64], [64, 23, 262], [63, 25, 222], [63, 23, 203], [62, 25, 37], [62, 23, 593], [61, 25, 580], [61, 23, 433], [60, 25, 393], [60, 23, 124], [59, 25, 578], [59, 23, 307], [58, 25, 567], [58, 23, 595], [57, 25, 620], [57, 23, 40], [56, 25, 402], [56, 23, 179], [55, 25, 373], [55, 23, 605], [54, 25, 318], [54, 23, 352], [53, 25, 93], [53, 23, 289], [52, 25, 108], [52, 23, 92], [51, 25, 121], [51, 23, 181], [50, 25, 184], [50, 23, 251], [49, 25, 130], [49, 23, 544], [48, 25, 1], [48, 23, 576], [47, 25, 255], [47, 23, 477], [46, 25, 413], [46, 23, 446], [45, 25, 372], [45, 23, 84], [44, 25, 240], [44, 23, 10], [43, 25, 379], [43, 23, 243], [42, 25, 172], [42, 23, 73], [41, 25, 315], [41, 23, 41], [40, 25, 452], [40, 23, 418], [39, 25, 500], [39, 23, 47], [38, 25, 177], [38, 23, 269], [37, 25, 466], [37, 23, 57], [36, 25, 624], [36, 23, 568], [35, 25, 79], [35, 23, 478], [34, 25, 316], [34, 23, 592], [33, 25, 468], [33, 23, 537], [32, 25, 440], [32, 23, 309], [31, 25, 200], [31, 23, 388], [30, 25, 221], [30, 23, 288], [29, 25, 565], [29, 23, 136], [28, 25, 219], [28, 23, 97], [27, 25, 187], [27, 23, 517], [26, 25, 499], [26, 23, 343], [25, 25, 382], [25, 23, 514], [24, 25, 612], [24, 23, 489], [23, 25, 404], [23, 23, 292], [22, 25, 528], [22, 23, 411], [21, 25, 207], [21, 23, 535], [20, 25, 137], [20, 23, 559], [19, 25, 340], [19, 23, 359], [18, 25, 53], [18, 23, 324], [17, 25, 444], [17, 23, 604], [16, 25, 239], [16, 23, 114], [15, 25, 326], [15, 23, 55], [14, 25, 237], [14, 23, 329], [13, 25, 381], [13, 23, 518], [12, 25, 342], [12, 23, 38], [11, 25, 176], [11, 23, 69], [10, 25, 256], [10, 23, 599], [9, 25, 555], [9, 23, 490], [8, 25, 313], [8, 23, 391], [7, 25, 441], [7, 23, 182], [6, 25, 252], [6, 23, 180], [5, 25, 320], [5, 23, 344], [4, 25, 68], [4, 23, 56], [3, 25, 26], [3, 23, 232], [2, 25, 293], [2, 23, 589], [1, 25, 312], [1, 23, 505], [0, 25, 234], [0, 23, 410]]
question_array = [23, -1, 6, 0, 8, 19, 4, 5, 14, -1, -1, 24, 21, 16, 17, 9, 13, 15, 12, 22, 11, 7, 10, 2, 18, 11, -1, 21, 16, -1, 9, 13, 15, 12, 22, 23, 7, -1, -1, 18, -1, -1, 6, 0, 8, 19, 4, -1, 14, 20, 9, 7, 10, -1, 18, -1, -1, -1, 0, 8, 19, -1, 5, 14, -1, 11, 24, 21, -1, -1, 23, 13, 15, -1, 22, 19, 4, 5, 14, -1, 11, 24, 21, 16, -1, 9, 13, 15, 12, 22, 23, 7, -1, -1, 18, -1, 1, -1, 0, 8, -1, 13, 15, 12, 22, 23, 7, 10, -1, 18, 11, 1, 6, 0, -1, 19, 4, 5, 14, 20, 9, -1, 21, 16, -1, 8, 23, 1, 6, 0, -1, 19, -1, -1, 14, 17, -1, -1, 21, 16, 22, 9, 13, 15, 12, 18, 11, 7, 10, 2, 17, 11, 24, 21, 16, 22, 9, 13, 15, 12, 18, 23, 7, 10, 2, 8, -1, 1, 6, 0, 20, 19, -1, -1, 14, 18, -1, -1, 10, -1, -1, -1, -1, 6, -1, 20, 19, -1, 5, 14, 17, 11, 24, 21, 16, 22, 23, 13, 15, 12, -1, 19, 4, -1, 14, 17, 11, -1, 21, 16, 22, 9, 13, 15, 12, 18, 23, 7, 10, -1, 8, -1, -1, 6, 0, 22, -1, 13, 15, 12, 18, 23, -1, 10, -1, 8, 11, -1, 6, -1, -1, 19, 4, -1, 14, 17, 9, 24, 21, 16, 2, -1, -1, 1, 10, -1, -1, 19, 4, 5, 0, 17, -1, 24, 6, 12, 22, 9, 13, -1, 16, 18, 11, 7, 21, 16, 17, 11, 24, 21, 12, 22, 9, 13, 15, 2, 18, 23, -1, -1, 0, 8, -1, -1, 6, 14, 20, 19, 4, 5, 12, 18, 9, 7, 15, 0, 8, -1, 1, -1, 14, 20, -1, -1, 5, -1, -1, 11, -1, 21, -1, 22, 23, 13, -1, 14, -1, 19, 4, -1, 16, 17, 11, -1, 21, 12, 22, 9, 13, 15, -1, 18, -1, -1, -1, 0, 8, 3, 1, 6, 0, 22, -1, 13, 6, -1, 18, 23, 7, -1, 16, 8, 11, 1, 21, 14, 20, 19, 4, 5, 12, 17, -1, -1, 15, 6, 2, 8, 23, -1, 5, -1, -1, 19, 4, 21, 0, 17, -1, -1, 15, -1, 22, -1, 13, 10, 16, 18, 11, 7, 21, 16, -1, 11, -1, 15, 12, 22, 9, 13, -1, -1, 18, -1, 7, 6, 0, 8, -1, 1, 5, 14, 20, 19, 4, 10, 12, 18, 9, 7, 6, 0, -1, -1, 1, 5, 14, 20, 19, 4, -1, -1, 17, 11, -1, 15, -1, 22, -1, 13, 5, 14, -1, 19, 4, 21, 16, 17, 11, -1, 15, 12, 22, 9, 13, 10, -1, 18, -1, 7, 6, 0, 8, 3, 1, 15, 0, -1, -1, 13, 10, 2, 18, 23, 7, 6, 16, 8, 11, -1, -1, 14, 20, 19, 4, 21, 12, 17, -1, -1, -1, 6, 2, 8, 23, -1, 5, 14, 20, 19, 24, 21, 0, 17, -1, 13, 15, -1, -1, 9, 7, 10, 16, 18, 11, -1, 21, 16, -1, 11, 13, 15, 12, 22, 9, -1, -1, -1, 18, 23, -1, 6, -1, 8, -1, 4, 5, 14, 20, 19, -1, 10, 12, 18, 9, -1, 6, 0, 8, -1, 4, 5, 14, 20, 19, -1, 21, -1, -1, 11, 13, 15, 2, 22, 23, 4, -1, 14, -1, 19, -1, 21, 16, 17, 11, 13, 15, 12, 22, -1, 7, 10, -1, -1, 23, -1, 6, 0, 8, -1, 13, 15, 0, 22, -1, -1, 10, 2, 18, 23, -1, 6, -1, 8, 11, 4, 5, 14, 20, -1, -1, 21, 12, 17, -1]
def make_matrix(array: list):
big_arr = []
for i in range(25):
arr = []
for j in range(25):
arr.append(array[i*25 + j])
big_arr.append(arr)
return big_arr
def make_matrix2(array: list):
big_arr = []
for i in range(25):
arr = []
for j in range(25):
arr.append(array[i + j*25])
big_arr.append(arr)
return big_arr
def make_matrix3(array: list):
big_arr = []
for i in range(5):
for j in range(5):
arr = []
val = 0
for k in range(25):
if k != 0 and k % 5 == 0:
val += 20
arr.append(array[i*5 + j*125 + k + val])
big_arr.append(arr)
return big_arr
#Make Flag Ints array
n = 77
flag_int = [Int("flag[%d]" % i) for i in range(n)]
#Make Question Ints
question_array_ints = []
i = 0
for val in question_array:
if val == -1:
question_array_ints.append(-1)
else:
question_array_ints.append(Int(f"matrix{i}"))
i += 1
for sequence in mod_seq:
question_array_ints[sequence[2]] = flag_int[sequence[0]] % sequence[1]
s = Solver()
#Add char restriction
for integer in flag_int:
s.add(32 < integer, integer < 126)
#Set array values
question_array_ints: list[ArithRef]
for i in range(len(question_array)):
if question_array[i] == -1: continue
else:
s.add(question_array_ints[i] == question_array[i])
#Set Distinction
big_arr = make_matrix(question_array_ints)
for arr in big_arr:
s.add(Distinct(arr))
big_arr = make_matrix2(question_array_ints)
for arr in big_arr:
s.add(Distinct(arr))
big_arr = make_matrix3(question_array_ints)
for arr in big_arr:
s.add(Distinct(arr))
if s.check() == sat:
m = s.model()
flag_str = ""
for integer in flag_int:
flag_str += chr(int(str(m[integer])))
print(f"Flag: {flag_str}")
print(f"Hash: {hashlib.sha256(flag_str.encode()).hexdigest()}")
else:
print("No solution found")
Output
Flag: fwectf{th3_m0r3_d1ff1cu1t_ch415_y0u_m4k3_th3_m0r3_d1ff1cu1t_m1n3_w111_63c0m3}
Hash: 8d5f1becd60f19181c89d6563677b941cc7ceec6298d80ffea7d17f537fb5c11