シンボリック実行

シンボリック実行エンジンは、プログラム入力を数学的変数として扱い、条件分岐ごとにパスを分けて探索します。各パスは一階論理の制約を蓄積し、Z3 などの SMT ソルバが充足可能性を判定し、可能ならそのパスに到達する具体的な入力を生成します。これにより、オーバーフロー、ゼロ除算、汚染がシンクに到達するなどのバグ条件の到達可能性を形式的に証明できますが、パス爆発と制約の複雑さに悩まされます。KLEE、angr、Manticore などのツールがファザー支援、深い脆弱性の発見、バイナリの安全性検証に用いられます。