Symbolic Execution
シンボリック実行は具体的な値の代わりにシンボル変数でプログラムを実行し、実行可能なすべてのパスを解析して、各パスを引き起こす入力を自動生成する。
目的
プログラムの振る舞いを精密に解析し、高カバレジのテストや脆弱性を誘発する入力を自動的に生成する。
メカニズム
変数はシンボルとして表現され、パス条件は制約として蓄積される。分岐ではパスを fork し、SMT ソルバで実行可能性を判定する。パス爆発が主なボトルネックである。KLEE や angr が C やバイナリのシンボリック実行を実現する。
ユースケース
- テストの自動生成
- セキュリティ脆弱性の調査
- パスカバレジの測定