初投稿です。今回、Full Weak Engineer CTFに参加させていただき、vvvmmm唯一のクリア者になれたので、この問題だけササっとWriteupを書いてみました。
大会自体は個人参加でしたが、4367ポイント稼いで26位だったので大分健闘した方なのではないでしょうか。
（本来の初投稿はpicoCTF 2025 Writeupになる予定でしたが、解いた問題をすべてカバーしようと記事を書いていくうちにやる気がどこかへ消えました。）
問題
vvvmmm.zipにはchal.tbcとcode.binの二つのファイルが入っている。
ファイルの正体の特定
入っている二つのファイルを両方ともIDA Freeで特定しようとしてみたが、バイナリファイルとしてしか認識せず。
どうやらアセンブリコードが含まれているわけではないらしい。
tbc拡張子のファイルが一体何なのかをインターネットで調べてみる。
すると、tbcファイルが使用された他のCTF問題のWriteupが見つかった。
このWriteupによると、tbcファイルとはTCLという言語で書かれたソースコードをコンパイルしたものであることが分かった。
corbamico氏が公開している「tbcload」というツールを使用すると逆アセンブリしてくれるとのこと。
Writeupにはバイトコードの解説も記されており、非常に丁寧。
Writeupを書いてくださったfsharp氏とツールの開発者であるcorbamico氏に大いに感謝したい。
さっそく、Githubからtbcload-windows-amd64.exeを入手し、tbcload-windows-amd64.exe decompile --detail chal.tbcを実行する。
すると以下の内容がコンソールに出力された。
(16進数の文字列)
...
Command 0,pc= 0-11
(0)push1 0
Command 1,pc= 2-9
(2)push1 1
(4)push1 2
(6)push1 3
(8)invokeStk1 3
(10)storeScalarStk
(11)pop
Command 2,pc= 12-27
(12)push1 4
...
（省略）
...
default {
puts stderr "Invalid Instruction: $op"
break
}
[lit-0051]tbcload::bcproc
これをテキストファイルにコピーして、1つずつ命令を上から見ていく。
TCLバイトコードを読む
括弧書きでその横にpush1 0等の文字列があるもの、これが一つのバイトコード命令となっている。
[lit-0051]等はlitとあるように文字列リテラルであり、それぞれ番号が割り振られている。
また、push1とpop命令があることから、スタックの概念も存在することが分かる。
この言語の特殊なところはスタックにプッシュされるのが、対応する番号の文字列リテラルであるという点だ。
例えば、push1 1は[lit-0001]openより、スタックに文字列openがプッシュされる。
これを踏まえて0と1番のコマンドを流れを見ていく。
Command 0,pc= 0-11
(0)push1 0 #Stack = [f]
Command 1,pc= 2-9
(2)push1 1
(4)push1 2
(6)push1 3 #Stack = [f, open, code.bin, r]
(8)invokeStk1 3 #Stack = [f, channelID]
(10)storeScalarStk #Stack = [f]
(11)pop #Stack = []
...（省略）
[lit-0000]f
[lit-0001]open
[lit-0002]code.bin
[lit-0003]r
(0)から(6)では、f, open, code.bin, rをスタックにプッシュしている。
(8)でスタックから3つ文字列をpopしてそれをコマンドとして実行。この場合、open code.bin rというコマンドを実行しており、code.binをオープンしている。結果としてチャンネルIDがpushされる。
(10)でスタックから2つpopして、最初の文字列の変数に二番目の文字列を代入。この場合、fという変数にチャンネルIDが代入される。最初の文字列がpushされる。
(11)で残ったfの文字列をpopする。
invokeStk1で実行されるTCLコマンドの詳細は、このブログを参考にさせていただいた。
また、バイトコードの詳細については氏と同じくこのサイトを参考にさせていただいた。
最初のVM
なんとかバイトコードを読み終わり同じVMをPythonで作成した。
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()
VMの仕組み自体については以下の通り：
- メモリは長さが4096あるint配列
- そのうち、
ipを0x1000 - 1（一番後ろ）、spを0x1000 - 2（後ろから2番目）として使用する - "code.bin"から5バイトずつ取り出し、それを一つの命令として扱う
1バイト目が命令識別子、2-3バイト目が最初の引数(short)、4-5バイト目が二番目の引数(short) - 単純なジャンプ命令以外にコールスタックも存在する
完成したVMでさっそくcode.binを実行してみる。
なお、本来はフラグを1文字ずつ手動で入力しないといけないのだが、少しVMをいじってINPUT定数を送信するようにした。
- 実行結果：
flag:Incorrect
入力したフラグが正解かどうかを判定するプログラムのようだ。
disassemble_bin関数でcode.binを逆アセンブリできるようにしたので、逆アセンブリする。
- 逆アセンブリ結果：
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 #Making Data
Inst 11: Assign, 2817, 962
Inst 12: Assign, 2818, 962
Inst 13: Assign, 2819, 962
Inst 14: Assign, 2820, 962
...
Inst 2654: PrintChar
ここに記されている命令名は、私が独自に名付けたものなので、わかりにくいものがあるかもしれない。
命令名と命令の挙動を表したPythonコードの対応表をここに記しておく。
- 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。ただし、もしコールスタックが空ならプログラム終了 - JumpTo:
memory[ip] = arg[0] - JumpIfZero: もし
memory[arg[1]]が0なら、memory[ip] = arg[0] - PrintChar:
print(chr(memory[0]), end="") - RecieveChar:
memory[0] = input()[0]。ただし、input()の長さが0ならmemory[0] = 10(改行コード)
これらの情報を駆使して逆アセンブリ結果を読み解いていく。
Inst 0-9はprint("flag: ")の部分。
Inst 965-973あたりがフラグ入力受付部分。
改行が送信されるまで入力を受け付ける。
Inst 977-995はprint("Incorrect")の部分。
認証部分で失敗するとここに飛ばされる。
Inst 2234-2654がフラグ認証部分。
メモリ中にある長さ625の配列を3通りでチェックしている。
詳細は後述。
さて、Inst 996-2229の大量pushの後、Inst 2232でCall, 900が実行されている。
何らかの関数を実行しているが、このInst 900-966の部分は実に奇妙なことになっている。
特にInst 921-959の部分がReturnに挟まれまくっており、一見到達不可能なコードに見える。
関数について調べてみると、あることが分かる。
この部分は私のメモを抜粋して説明する。
なお、引数が文字列になっている箇所があるが、変数名として名前付けしている。
Inst 2230: AssignReg, 0, SP
Inst 2231: Assign, SP, 3072
Inst 2232: Call, run_stack_vm
run_stack_vm:
0 = SP
SP = 3072
SP - 256 = length of stack VM Commands
Inst 900: AssignReg, 128, 0 //128 = pushed count
enc_loop:
Inst 901: Sub, 128, 256
Inst 902: JumpIfZero, 128, ret //if (no more stack cmd) goto ret
Inst 903: Add, 128, 256
Inst 904: AssignReg, 0, 128
Inst 905: Sub, 128, 1 //128 -= 1
Inst 906: Load, 0 //0 = pushed_num
Inst 907: Call, run_stackcmd
Inst 908: Sub, 10, 28
Inst 909: JumpIfZero, 10, ret
Inst 910: Add, 10, 28
Inst 911: JumpTo, enc_loop
ret:
Inst 912: Return
run_stackcmd:
Inst 913: AssignReg, 1, 0
Inst 914: AssignReg, 99, 0
Inst 915: Div, 99, 256
Inst 916: JumpIfZero, 99, switch_cmd //if pushed_num < 256: jump switch_cmd
Inst 917: JumpTo, 962
switch_cmd:
Inst 918: Add, 0, 2816
Inst 919: Load, 0
Inst 920: AssignReg, 4095, 0 //4095番はIP, switch by Commands
Inst 920がAssignReg, 4095, 0とあるが、メモリの4095番はIPとして使用されている。
つまりここでIPを直接制御して到達不可能に見えたコードへジャンプしているということである。
ではジャンプ先はどこから取得しているのかというとInst 918にAdd, 0, 2816とある。
直前の挙動からみるに、メモリの[2816+オフセット値(0-255)]番の中身をジャンプ先として取得している。
Inst 10-265が2816から3071まで定数を代入していることから、この部分がジャンプテーブルのセットアップということになる。
ではオフセット値はどこからくるのか。enc_loop部分の挙動からInst 996-2229の大量プッシュして用意した配列を1つずつpopしていることがわかる。
値を取得してそれに基づいて特定の部分へジャンプし、命令を実行する・・・
あれ？これもVM？
第二のVM
というわけでまたVMをPythonで作成。
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))
二つ目のVMの仕組みについて：
-
cmdsが大量プッシュされていた数字の配列 -
dataはジャンプテーブル -
data[cmd]が実際に実行する命令 - スタックも存在する
両方とも最初のVMのメモリから抜き取った。
抜き取りには最初のVMの下記の箇所を、コメントアウトを外して使用。
# 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))
二つ目のVMのLoadとPopReg命令に関しては本来、最初のVM中のメモリの情報が必要だが、Loadは0をスタックにプッシュ、PopRegは何もしないという処理に置き換えた。
逆アセンブリ結果を出力してみると大体以下の繰り返し。
Push 23 #Moduloする数字
Push 14 #入力した文字列があるメモリ番号。[12-88]
Load 14 #memory[メモリ番号](flagの文字)をスタックにプッシュ
Mod 0, 23, result=0
Push 1792 #1792で固定
Push 589 #オフセット [0-624]
Add 589, 1792, result=2381
PopReg 2381, 0 #memory[1792+オフセット] = modulo結果
最初のVMがRecieveCharの結果を、メモリの12-88番に保存していたので、それをある数字でModuloした結果を1792+オフセットの位置に保存していることが分かる。
メモリの1792-2416番はInst 266-890で初期化されており、認証にも使用されていることから、入力した文字列によって、長さ625の配列の要素が変化し、それを認証でチェックして正解か不正解を判断しているということがわかった。
ということで、[入力した文字列のインデックス、moduloする数字、長さ625の配列のインデックス]の組み合わせをcalc_infos.txtに記録するようにstackvm.pyに追記した。
実際のプログラムの流れ
というわけで実際のプログラムはどのような挙動をしているのかを、説明用にPythonで作成。
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")
-
mod_seqは[入力した文字列のインデックス、moduloする数字、長さ625の配列のインデックス]の配列 -
long_arrayは長さ625の配列（Inst 10-265で初期化されているもの）
まず最初にプログラムは、文字列の入力を受け取り、文字列の長さが77であるかをチェックする。77でなければ不正解としてプログラムを終了する。
77であった場合、文字列に応じてlong_arrayを改変する。その際、mod_seqを参照し、入力した文字のインデックスに応じて、特定の数字でmoduloして、long_arrayの特定のインデックスにセットする。
その後、3通りの方法でlong_arrayから25x25の二次元配列を作成する。
最後に、作成した3つの二次元配列を認証する。認証方法としては、二次元配列から配列を一つずつ取り出し、すべての配列中に0から24の数字が揃っていれば、認証成功、そうでなければ失敗というもの。
あとはz3ソルバーを作成してフラグを入手するだけ。
solve_z3.py
from z3 import *
import hashlib
#[入力した文字列のインデックス、moduloする数字、長さ625の配列のインデックス]
#question_array[matrix_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")
Flag: fwectf{th3_m0r3_d1ff1cu1t_ch415_y0u_m4k3_th3_m0r3_d1ff1cu1t_m1n3_w111_63c0m3}
Hash: 8d5f1becd60f19181c89d6563677b941cc7ceec6298d80ffea7d17f537fb5c11