CTFのリバーシングを解いていると,条件に当てはまる入力を探索することが有ります.
フラグに関する条件を入れて探索してくれるのがSMTソルバ(z3)です.
z3はリバーシングの分野で頻出で,パターンの解を見つけるのにもz3,数式を解くにもz3などかなり便利ですが今まで真面目に触れてこなかったので一通り触ってみたいと思いました.
https://gmo-cybersecurity.com/blog/flare-on-11-write-up-ja/
https://gmo-cybersecurity.com/blog/flare-on-11-write-up/
GMOサイバーセキュリティbyイエラエの記事,"The Flare-On Challengeとは?Flare-On 11の問題紹介とFlare-On 12への誘い"ではz3を使ってリバーシングの有名なCTFであるThe Flare-On Challengeの問題を解いています.
Yaraルールに関する制約を満たす解をz3で見つけています.
https://apemik.hatenablog.com/entry/2024/10/05/215345
こちらの記事ではAlpacaHack Round4で出題されたself-modifyバイナリについてz3でフラグを得ているwriteupになります.
https://www.youtube.com/watch?v=xvFZjo5PgG0
そしてこちらは有名な動画になります.youtubeの動画ですので見やすいと思います.
このように(?)z3はかなり便利そうですので私としてもマスターしつつ弊校の学生にもその利便性を伝えたいと思います
z3は複雑な数理論理式,命題論理に加えて、整数、浮動小数点数、配列、文字列などに対する充足可能性を効率的に決定できます。
整数算術(Linear Integer Arithmetic)
実数算術(Linear Real Arithmetic)
ビットベクトル(Bit-vectors)
配列やリスト(Arrays and Lists)
論理式の量化(Quantifiers)
等の理論に対応しており複数の言語でOSSとして公開されています.
私はlinux環境ですのでreadmeの通りgccでmakeしインストールしました
https://github.com/Z3Prover/z3?tab=readme-ov-file#building-z3-using-make-and-gccclang
python環境のみでの利用の場合
pip install z3-solver
のみでインストール出来ます.
今回は過去に解いた問題からn00bzCTF2024のリバーシング,flagcheckerをz3で解いていきたいと思います.
アドカレを書くには時間がないので簡単な問題ですが制約を見つける問題としてふと頭をよぎりました.
n00bzCTF2024で私が他に解いた問題のwriteupはこちらですN00bzCTF Writeups
問題の概要としてはexelファイルのマクロを解析し,合致する入力を解析するとイメージしてください.
Rem Attribute VBA_ModuleType=VBAModule
Option VBASupport 1
Sub FlagChecker()
Dim chars(1 To 24) As String
guess = InputBox("Enter the flag:")
If Len(guess) <> 24 Then
MsgBox "Nope"
End If
char_1 = Mid(guess, 1, 1)
char_2 = Mid(guess, 2, 1)
char_3 = Mid(guess, 3, 1)
char_4 = Mid(guess, 4, 1)
char_5 = Mid(guess, 5, 1)
char_6 = Mid(guess, 6, 1)
char_7 = Mid(guess, 7, 1)
char_8 = Mid(guess, 8, 1)
char_9 = Mid(guess, 9, 1)
char_10 = Mid(guess, 10, 1)
char_11 = Mid(guess, 11, 1)
char_12 = Mid(guess, 12, 1)
char_13 = Mid(guess, 13, 1)
char_14 = Mid(guess, 14, 1)
char_15 = Mid(guess, 15, 1)
char_16 = Mid(guess, 16, 1)
char_17 = Mid(guess, 17, 1)
char_18 = Mid(guess, 18, 1)
char_19 = Mid(guess, 19, 1)
char_20 = Mid(guess, 20, 1)
char_21 = Mid(guess, 21, 1)
char_22 = Mid(guess, 22, 1)
char_23 = Mid(guess, 23, 1)
char_24 = Mid(guess, 24, 1)
If Asc(char_1) Xor Asc(char_8) = 22 Then
If Asc(char_10) + Asc(char_24) = 176 Then
If Asc(char_9) - Asc(char_22) = -9 Then
If Asc(char_22) Xor Asc(char_6) = 23 Then
If (Asc(char_12) / 5) ^ (Asc(char_3) / 12) = 130321 Then
If char_22 = char_11 Then
If Asc(char_15) * Asc(char_8) = 14040 Then
If Asc(char_12) Xor (Asc(char_17) + 5) = 5 Then
If Asc(char_18) = Asc(char_23) Then
If Asc(char_13) Xor Asc(char_14) Xor Asc(char_2) = 73 Then
If Asc(char_14) Xor Asc(char_24) = 77 Then
If 1365 = Asc(char_22) Xor 1337 Then
If Asc(char_10) = Asc(char_7) Then
If Asc(char_23) + Asc(char_8) = 235 Then
If Asc(char_16) = Asc(char_17) + 19 Then
If Asc(char_19) = 107 Then
If Asc(char_20) + 501 = (Asc(char_1) * 5) Then
If Asc(char_21) = Asc(char_22) Then
MsgBox "you got the flag!"
End If
End If
End If
End If
End If
End If
End If
End If
End If
End If
End If
End If
End If
End If
End If
End If
End If
End If
End Sub
さて,ここで私が開催中に書いたソルバを見てみましょう.
x1 = ord("n")
x2 = ord("0")
x3 = ord("0")
print(x3)
x4 = ord("b")
x5 = ord("z")
x6 = ord("{")
x24 = ord("}")
# If (Asc(char_1) Xor Asc(char_8)) = 22 Then
x8 = x1^22 # x1 ^ x8 = 22
# If (Asc(char_10) + Asc(char_24)) = 176 Then
x10 = 176-x24 # x10 + x24 = 176
# If (Asc(char_22) Xor Asc(char_6)) = 23 Then
x22 = x6^23 # x22 ^ x6 = 23
# If (Asc(char_9) - Asc(char_22)) = -9 Then
x9 = x22-9 # x9 - x22 = -9
# If ((Asc(char_12) / 5) ^ (Asc(char_3) / 12)) = 130321 Then
# (x12 / 5) ^ (x3 / 12) = 130321
for i in range(1000):
if i**4 == 130321:
x12 = i*5
# If (char_22 = char_11) Then
x11=x22 # x22 = x11
# If (Asc(char_15) * Asc(char_8)) = 14040 Then
x15 = 14040/x8 # x15 * x8 = 14040
# If (Asc(char_12) Xor (Asc(char_17) - 5)) = 5 Then
x17 = (5^x12)+5 # x12 ^ (x17 + 5) = 5
# If (Asc(char_14) Xor Asc(char_24)) = 77 Then
x14=77^x24 # x14 ^ x24 = 77
# If (Asc(char_13) Xor Asc(char_14) Xor Asc(char_2)) = 121 Then
x13=121^x2^x14 # x13 ^ x14 ^ x2 = 73
#If 1365 = (Asc(char_22) Xor 1337) Then
x22 = 1337^1365 # 1365 = x22 ^ 1337
# If (Asc(char_10) = Asc(char_7)) Then
x7 = x10 # x10 = x7
# If (Asc(char_23) + Asc(char_8)) = 235 Then
x23 = 235-x8 # x23 + x8 = 235
x18 = x23 # x18 = x23
x16 = x17+19 # x16 = x17 + 19
x19=107 # x19 = 107
x20 = (x1*5)-501 # x20 + 501 = x1 * 5
x21 = x22 # x21 = x22
print(chr(int(x1)),end="")
print(chr(int(x2)),end="")
print(chr(int(x3)),end="")
print(chr(int(x4)),end="")
print(chr(int(x5)),end="")
print(chr(int(x6)),end="")
print(chr(int(x7)),end="")
print(chr(int(x8)),end="")
print(chr(int(x9)),end="")
print(chr(int(x10)),end="")
print(chr(int(x11)),end="")
print(chr(int(x12)),end="")
print(chr(int(x13)),end="")
print(chr(int(x14)),end="")
print(chr(int(x15)),end="")
print(chr(int(x16)),end="")
print(chr(int(x17)),end="")
print(chr(int(x18)),end="")
print(chr(int(x19)),end="")
print(chr(int(x20)),end="")
print(chr(int(x21)),end="")
print(chr(int(x22)),end="")
print(chr(int(x23)),end="")
print(chr(int(x24)),end="")
print("")
はい,正直終わってますね(T_T)
ちゃんとフラグは出るのでCTFとしては成功してるのですがz3できれいに解きたいと思います.
ソルバの美容はモテの秘訣です.
from z3 import *
s = Solver()
Dim chars(1 To 24) As String
より24文字とわかります.
よってz3に対し24文字のascii文字列を作りました.
chars = [BitVec(f'char_{i}', 32) for i in range(24)]
n00bzCTF{}
ですからこのフラグフォーマットに合わせてz3の制約を追加します
s.add(chars[0] == ord('n'))
s.add(chars[1] == ord('0'))
s.add(chars[2] == ord('0'))
s.add(chars[3] == ord('b'))
s.add(chars[4] == ord('z'))
s.add(chars[5] == ord('{'))
s.add(chars[23] == ord('}'))
この度,フラグの配列はBitVecで宣言していますからべき乗の成約に関してはInt()に変換,BV2Int()をしています.
s.add(chars[0] == ord('n'))
s.add(chars[1] == ord('0'))
s.add(chars[2] == ord('0'))
s.add(chars[3] == ord('b'))
s.add(chars[4] == ord('z'))
s.add(chars[5] == ord('{'))
s.add(chars[23] == ord('}'))
s.add(chars[0] ^ chars[7] == 22) # char_1 XOR char_8
s.add(chars[9] + chars[23] == 176) # char_10 + char_24
s.add(chars[8] - chars[21] == -9) # char_9 - char_22
s.add(chars[21] ^ chars[5] == 23) # char_22 XOR char_6
x = BV2Int(chars[11] / 5)
y = BV2Int(chars[2] / 12)
s.add(x ** y == 130321) # (char_12/5)^(char_3/12)
s.add(chars[21] == chars[10]) # char_22 = char_11
s.add(chars[14] * chars[7] == 14040) # char_15 * char_8
s.add(chars[11] ^ (chars[16] - 5) == 5) # char_12 XOR (char_17 + 5)
s.add(chars[17] == chars[22]) # char_18 = char_23
s.add(chars[12] ^ chars[13] ^ chars[1] == 121) # char_13 XOR char_14 XOR char_2
s.add(chars[13] ^ chars[23] == 77) # char_14 XOR char_24
s.add(chars[21] ^ 1337 == 1365) # char_22 XOR 1337
s.add(chars[9] == chars[6]) # char_10 = char_7
s.add(chars[22] + chars[7] == 235) # char_23 + char_8
s.add(chars[15] == chars[16] + 19) # char_16 = char_17 + 19
s.add(chars[18] == 107) # char_19
s.add(chars[19] + 501 == (chars[0] * 5)) # char_20 + 501 = char_1 * 5
s.add(chars[20] == chars[21]) # char_21 = char_22
for c in chars:
s.add(c >= 32, c <= 126)
if s.check() == sat:
m = s.model()
flag = ''.join([chr(m[c].as_long()) for c in chars])
print(f"Flag: {flag}")
else:
print("No solution found")
素晴らしいですね😆
z3,SMTソルバは使いこなせればリバーシングの条件探索でかなり役に立ちそうです.
ただz3内部の型についてはかなり悩まされてしまった(特にべき乗計算はかなり壁だった)ので使いこなしていきたいところです.
今回も突発的に書いた記事になりますがz3についてお役に立てたら嬉しいです.
z3の内部アルゴリズム等触れていませんが機会があれば内部アルゴリズムについても触れてみてSMTソルバを自作してみたいと思います.
最後に最終的なソルバだけ載せて記事を締めます
from z3 import *
s = Solver()
chars = [BitVec(f'char_{i}', 32) for i in range(24)]
s.add(chars[0] == ord('n'))
s.add(chars[1] == ord('0'))
s.add(chars[2] == ord('0'))
s.add(chars[3] == ord('b'))
s.add(chars[4] == ord('z'))
s.add(chars[5] == ord('{'))
s.add(chars[23] == ord('}'))
s.add(chars[0] ^ chars[7] == 22) # char_1 XOR char_8
s.add(chars[9] + chars[23] == 176) # char_10 + char_24
s.add(chars[8] - chars[21] == -9) # char_9 - char_22
s.add(chars[21] ^ chars[5] == 23) # char_22 XOR char_6
x = BV2Int(chars[11] / 5)
y = BV2Int(chars[2] / 12)
s.add(x ** y == 130321) # (char_12/5)^(char_3/12)
s.add(chars[21] == chars[10]) # char_22 = char_11
s.add(chars[14] * chars[7] == 14040) # char_15 * char_8
s.add(chars[11] ^ (chars[16] - 5) == 5) # char_12 XOR (char_17 + 5)
s.add(chars[17] == chars[22]) # char_18 = char_23
s.add(chars[12] ^ chars[13] ^ chars[1] == 121) # char_13 XOR char_14 XOR char_2
s.add(chars[13] ^ chars[23] == 77) # char_14 XOR char_24
s.add(chars[21] ^ 1337 == 1365) # char_22 XOR 1337
s.add(chars[9] == chars[6]) # char_10 = char_7
s.add(chars[22] + chars[7] == 235) # char_23 + char_8
s.add(chars[15] == chars[16] + 19) # char_16 = char_17 + 19
s.add(chars[18] == 107) # char_19
s.add(chars[19] + 501 == (chars[0] * 5)) # char_20 + 501 = char_1 * 5
s.add(chars[20] == chars[21]) # char_21 = char_22
for c in chars:
s.add(c >= 32, c <= 126)
if s.check() == sat:
m = s.model()
flag = ''.join([chr(m[c].as_long()) for c in chars])
print(f"Flag: {flag}")
else:
print("No solution found")
[~/dc/ctf/noobz/rev/flagchecker] >>>python3 z.py
Flag: n00bz{3xc3l_y0ur_sk1lls}