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

はじめに

 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を読むのはいつになるかわかりません.

 わざわざブログに書くほどでもないことから書いていかないとなまるので書く.

はじめに

 寿司 虚空編[1]第2話で登場したアッカーマン関数というかS変換を実装する.

定義

 $x, y$を非負整数として,

$$Ack(x,y)= \begin{cases} y+1 & \text{if}\ x=0, \\ Ack(x-1,1) & \text{if}\ x>0, y=0, \\ Ack(x-1,Ack(x,y-1)) & \text{otherwise}. \end{cases}$$

 恥ずかしながら「Union-Find木のならし計算量はアッカーマン関数の逆関数となる」といった説明でしか見たことがない.

実験

 何も考えずに$Ack(3, 3)$を実装.なお記号は寿司 虚空編に準拠.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
def f(x):
return x + 1
def b(m, n):
if m == 0 and n > 0:
return f(n)
elif m > 0 and n == 0:
return b(m - 1, 1)
else:
return b(m - 1, b(m, n - 1))
def g(x):
return b(x, x)
def main():
print g(3) # Ack(3, 3)
if __name__ == "__main__":
main()

 実行してみる.ついでにプロファイリング.

1
2
3
4
5
6
7
8
9
10
11
12
13
# python -m cProfile -s time ./sushi.py
61
3624 function calls (1193 primitive calls) in 0.006 seconds
Ordered by: internal time
ncalls tottime percall cumtime percall filename:lineno(function)
2432/1 0.005 0.000 0.006 0.006 sushi.py:4(b)
1188 0.001 0.000 0.001 0.000 sushi.py:1(f)
1 0.000 0.000 0.006 0.006 sushi.py:15(main)
1 0.000 0.000 0.006 0.006 sushi.py:1(<module>)
1 0.000 0.000 0.006 0.006 sushi.py:12(g)
1 0.000 0.000 0.000 0.000 {method 'disable' of '_lsprof.Profiler' objects}

 このプログラムで$Ack(x, y)$を計算しようとするとRuntimeError: maximum recursion depth exceededとなって死ぬ.
 そこで次の手法を導入する:

  • スタック制限の緩和
  • 再帰深度制限の緩和
  • メモ化再帰
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
import sys, threading, thread
memo = {}
def f(x):
return x + 1
def b(m, n):
if (m, n) not in memo:
memo[(m, n)] = (
f(n) if m == 0 and n > 0 else
b(m - 1, 1) if m > 0 and n == 0 else
b(m - 1, b(m, n - 1))
)
return memo[(m,n)]
def g(x):
return b(x, x)
def main():
print g(3) # 61
if __name__ == "__main__":
sys.setrecursionlimit(1024*1024)
thread.stack_size(128*1024*1024)
threading.Thread(target=main).start()

 やる.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
# python -m cProfile -s time ./sushi.py
61
415 function calls in 0.002 seconds
Ordered by: internal time
ncalls tottime percall cumtime percall filename:lineno(function)
1 0.000 0.000 0.002 0.002 threading.py:1(<module>)
1 0.000 0.000 0.000 0.000 collections.py:1(<module>)
1 0.000 0.000 0.002 0.002 sushi.py:1(<module>)
7 0.000 0.000 0.000 0.000 {method 'acquire' of 'thread.lock' objects}
1 0.000 0.000 0.000 0.000 heapq.py:31(<module>)
91 0.000 0.000 0.000 0.000 {method 'append' of 'list' objects}
2 0.000 0.000 0.000 0.000 sre_parse.py:379(_parse)
28 0.000 0.000 0.000 0.000 sre_parse.py:182(__next)
2 0.000 0.000 0.000 0.000 sre_compile.py:359(_compile_info)
73 0.000 0.000 0.000 0.000 {len}
2 0.000 0.000 0.000 0.000 sre_compile.py:32(_compile)
26 0.000 0.000 0.000 0.000 sre_parse.py:201(get)
22 0.000 0.000 0.000 0.000 sre_parse.py:138(append)
1 0.000 0.000 0.000 0.000 {thread.start_new_thread}
4 0.000 0.000 0.000 0.000 threading.py:259(__init__)
2 0.000 0.000 0.000 0.000 threading.py:656(__init__)
2 0.000 0.000 0.001 0.000 re.py:226(_compile)
21 0.000 0.000 0.000 0.000 {ord}
2 0.000 0.000 0.001 0.000 sre_compile.py:493(compile)
1 0.000 0.000 0.001 0.001 warnings.py:45(filterwarnings)
1 0.000 0.000 0.000 0.000 threading.py:308(wait)
8 0.000 0.000 0.000 0.000 threading.py:58(__init__)
2 0.000 0.000 0.000 0.000 sre_parse.py:675(parse)
2 0.000 0.000 0.000 0.000 threading.py:560(__init__)
1 0.000 0.000 0.000 0.000 threading.py:640(Thread)
4 0.000 0.000 0.000 0.000 threading.py:241(Condition)
2 0.000 0.000 0.000 0.000 sre_parse.py:140(getwidth)
2 0.000 0.000 0.000 0.000 sre_parse.py:301(_parse_sub)
12 0.000 0.000 0.000 0.000 {_sre.getlower}
10 0.000 0.000 0.000 0.000 {isinstance}
1 0.000 0.000 0.000 0.000 threading.py:726(start)
2 0.000 0.000 0.000 0.000 sre_compile.py:478(_code)
4 0.000 0.000 0.000 0.000 sre_compile.py:472(isstring)
1 0.000 0.000 0.000 0.000 threading.py:1090(__init__)
2 0.000 0.000 0.000 0.000 {method 'setter' of 'property' objects}
1 0.000 0.000 0.000 0.000 collections.py:26(OrderedDict)
6 0.000 0.000 0.000 0.000 {thread.allocate_lock}
1 0.000 0.000 0.000 0.000 threading.py:602(wait)
1 0.000 0.000 0.000 0.000 threading.py:124(_RLock)
2 0.000 0.000 0.000 0.000 sre_parse.py:178(__init__)
1 0.000 0.000 0.000 0.000 threading.py:627(_newname)
1 0.000 0.000 0.000 0.000 threading.py:575(set)
4 0.000 0.000 0.000 0.000 {min}
2 0.000 0.000 0.001 0.000 re.py:188(compile)
3 0.000 0.000 0.000 0.000 {thread.get_ident}
1 0.000 0.000 0.000 0.000 keyword.py:11(<module>)
1 0.000 0.000 0.000 0.000 threading.py:372(notify)
1 0.000 0.000 0.000 0.000 {thread.stack_size}
1 0.000 0.000 0.000 0.000 threading.py:709(_set_daemon)
2 0.000 0.000 0.000 0.000 threading.py:541(Event)
2 0.000 0.000 0.000 0.000 threading.py:299(_is_owned)
2 0.000 0.000 0.000 0.000 {_sre.compile}
3 0.000 0.000 0.000 0.000 {method 'release' of 'thread.lock' objects}
1 0.000 0.000 0.000 0.000 threading.py:296(_acquire_restore)
1 0.000 0.000 0.000 0.000 {sys.setrecursionlimit}
2 0.000 0.000 0.000 0.000 {method 'extend' of 'list' objects}
2 0.000 0.000 0.000 0.000 sre_parse.py:67(__init__)
1 0.000 0.000 0.000 0.000 threading.py:399(notifyAll)
1 0.000 0.000 0.000 0.000 collections.py:387(Counter)
2 0.000 0.000 0.000 0.000 {method 'get' of 'dict' objects}
2 0.000 0.000 0.000 0.000 sre_parse.py:90(__init__)
1 0.000 0.000 0.000 0.000 threading.py:293(_release_save)
1 0.000 0.000 0.000 0.000 threading.py:551(_Event)
2 0.000 0.000 0.000 0.000 sre_parse.py:195(match)
3 0.000 0.000 0.000 0.000 threading.py:63(_note)
1 0.000 0.000 0.000 0.000 threading.py:1152(currentThread)
1 0.000 0.000 0.000 0.000 threading.py:254(_Condition)
2 0.000 0.000 0.000 0.000 {method 'items' of 'dict' objects}
1 0.000 0.000 0.000 0.000 threading.py:789(_set_ident)
1 0.000 0.000 0.000 0.000 threading.py:1058(_Timer)
1 0.000 0.000 0.000 0.000 threading.py:1088(_MainThread)
1 0.000 0.000 0.000 0.000 {method 'insert' of 'list' objects}
1 0.000 0.000 0.000 0.000 threading.py:422(_Semaphore)
1 0.000 0.000 0.000 0.000 threading.py:1097(_set_daemon)
1 0.000 0.000 0.000 0.000 threading.py:569(isSet)
1 0.000 0.000 0.000 0.000 threading.py:56(_Verbose)
1 0.000 0.000 0.000 0.000 threading.py:1128(_DummyThread)
1 0.000 0.000 0.000 0.000 threading.py:1008(daemon)
1 0.000 0.000 0.000 0.000 {issubclass}
1 0.000 0.000 0.000 0.000 {method 'disable' of '_lsprof.Profiler' objects}
1 0.000 0.000 0.000 0.000 threading.py:514(_BoundedSemaphore)

 関数呼び出し回数が3624回から415回まで減り,4msec高速化.

おわりに

 それでも$Ack(4, 2)$でSEGVするのでこのお話はなかったことに.$2^{65536}-3$は遠い.

参考文献