なにもかも忘れかけている.

はじめに

 z3pyはSMTソルバZ3のPythonバインディング.たとえば

1
2
3
4
5
...
if(x * 2 + 3 * y == 4
&& x * 3 + y == -1){
puts("congrats!");
}

のようなプログラムに対して

1
2
3
4
5
6
7
8
9
10
11
from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add(x * 2 + 3 * y == 4)
s.add(x * 3 + y == -1)
print(s.check())
print(s.model())

としてやれば期待される入力値[x = -1, y = 2]を算出できる.これだけではだからなに? という感じだが.シンボリック実行は各命令とメモリの状態からこの割当を自動生成するものだと思えばよい.これがangrやらTritonやらmiasmやらmanticoreやら,その他いまどきのバイナリ解析ツール群の基盤となっているというわけです.

参考になったサイト

 で,メモっとかないと忘れるので.SAT/SMTソルバのしくみやシンボリック実行全般まで広げると膨大になるということで,z3pyに限っています.前者については高速SATソルバーの原理 - 基盤(S)離散構造処理系プロジェクト[PDF]SAT/SMTソルバの仕組み - SlideShareを読むとよいでしょう.いまどきのSAT/SMTソルバにはVSIDSやらLubyリスタートやらいろいろな工夫が盛り込まれているが,とりあえずユーザとしてはDPLLとCDCLさえ抑えておけば問題ないはず.後者,シンボリック実行全般に関するおすすめの文献は秘密.Pythonバインディング以外の記事,angrやTritonなどサードパーティのツール群に関する記事も省いてある.

ウェブサイト 概要
CTF/Toolkit/z3py - 電気通信大学MMA 日本語で書かれた入門資料.これには書かれてないがBitVecSortも便利.
Theorem prover, symbolic execution and practical reverse-engineering z3pyのチュートリアル.まずはこの通りに手を動かす.
Breaking Kryptonite’s Obfuscation: A Static Analysis Approach Relying on Symbolic Execution シンボリック実行の最小構成の実装.
0vercl0k/z3-playground 上2つの資料で参照されているソースコード群.
Solving a simple crackme using Z3 – Aneesh Dogra’s Blog 簡単なcrackmeのwriteup.
Playing with Z3, hacking the serial check. – rosako’s blog 簡単なcrackmeのwriteup.
Using SAT and SMT to defeat simple hashing algorithms - LSE Blog オレオレハッシュ関数の解析.
Reversing the petya ransomware with constraint solvers ランサムウェアPetyaのSalsa実装の不備を突くdecryptor.
thomasjball/PyExZ3 シンボリック実行の実装例.z3公式からリンクが貼られている.symbolic/以下,z3_wrap.py, loader.pyが参考になる.
Quick introduction into SAT/SMT solvers and symbolic execution (DRAFT) [PDF] いろいろリンク貼ったけどこれだけ読めばいい.SMTソルバの紹介.数独の解き方.マインスイーパの自動化.デコンパイラ.難読化解除.シンボリック実行.ハッシュ関数の解析.全部載っている.Dennis Yurichev氏,Reverse Engineering for Beginnersも書いていて,慈善事業家か?

 はてなブックマークを使っていればよかったのではという気がしてきた.

おわりに

 z3py便利最高ですね.みなさんは便利最高ですか?
 これで次のようなCTFの問題を解くことができます:

問題 大会
Unbreakable Enterprise Product Activation Google CTF 2016
Ropsynth SECCON 2016 Online CTF
baby-re DEF CON CTF Qualifier 2016
amandhj DEF CON CTF Qualifier 2016
Pepperidge Farm DEF CON CTF Qualifier 2017

 まあ明らかにangr使ったほうが楽.とりあえずいくつかやってみただけで,ほかにもたくさんあると思う.
 Bareflank Hypervisorを読むのはいつになるかわかりません.