Try   HackMD

SMTソルバ入門(z3)

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

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

のみでインストール出来ます.

challenge

今回は過去に解いた問題からn00bzCTF2024のリバーシング,flagcheckerをz3で解いていきたいと思います.
アドカレを書くには時間がないので簡単な問題ですが制約を見つける問題としてふと頭をよぎりました.
n00bzCTF2024で私が他に解いた問題のwriteupはこちらですN00bzCTF Writeups

summary

問題の概要としてはexelファイルのマクロを解析し,合致する入力を解析するとイメージしてください.

Image Not Showing Possible Reasons
  • The image was uploaded to a note which you don't have access to
  • The note which the image was originally uploaded to has been deleted
Learn More →

マクロ全体

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)
image
ちゃんとフラグは出るのでCTFとしては成功してるのですがz3できれいに解きたいと思います.
ソルバの美容はモテの秘訣です.

solution

  • z3ソルバの作成
    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('}'))
  • VBマクロの制約
    VBマクロで実装されている条件式についてz3に制約を追加していきます
    全てのコードに対して共通しますがVBで実装されている変数名とpythonソルバ内の変数名のインデクスが1つずれています.

この度,フラグの配列は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
  • ASCII範囲
    ASCII範囲は32~127ですからこの制約も追加していきます
for c in chars: s.add(c >= 32, c <= 126)

  • z3に解かせます
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")

result

image
素晴らしいですね😆

Conclusion

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}