Search
シンボリック実行エンジン
Last updated
Nov 30, 2022
Edit Source
# 説明
プログラム上で目的の地点に到達したいとき、それに当てはまるような入力値の条件を数学的に解くプログラム。条件分岐ごとに条件式を追加してそれをSMTソルバに解かせる。
Concolic Execution
SSA形式とCFGが対応する
Taint 解析
# 計算量
条件分岐数を $N$ として $O(2^N)$
# 実装
レジスタ, メモリに関する制約とSSA形式のIRを条件式としてSMTソルバで解く。
# 使用例
シンボリック実行エンジンのプロジェクト angr のサンプルコード。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
| import angr
import logging
binary_path = './chall'
target = angr.Project(binary_path, main_opts={'base_addr': 0x10000})
logging.getLogger('angr').setLevel(logging.CRITICAL)
entry_state = target.factory.entry_state()
simulation = target.factory.simulation_manager(entry_state)
simulation.explore(find=0x000115b1, avoid=0x000115c4)
for sf in simulation.found:
print(sf.posix.dumps(0))
solution - simulation.found[0].posix.dumps(0)
print(solution)
|
# 参考