シンボリック実行とは？
しんぼりっくじっこう
プログラムの変数に具体的な値ではなくシンボル（記号）を割り当て、すべての実行パスを網羅的に解析する技術です。
シンボリック実行（Symbolic Execution）とは、プログラムのテスト・検証技術のひとつで、変数に具体的な数値や文字列の代わりにシンボル（記号）を代入し、プログラムの全実行パスを数学的に解析する手法です。
通常のプログラム実行では、特定の入力値に対してひとつのパスしかたどりませんが、シンボリック実行では入力を「任意の値」として扱い、条件分岐ごとに「この条件が真の場合」「偽の場合」という制約を積み重ねていきます。この制約の集合（パス条件）をSMTソルバーなどの定理証明器に渡すことで、バグを引き起こす入力値を自動的に発見できます。
代表的な活用場面は以下のとおりです。
- セキュリティ検査：バッファオーバーフローや整数オーバーフローを引き起こす入力の探索
- 自動テストケース生成：コードカバレッジを最大化するテスト入力の自動生成
- プログラム検証：仕様に反するパスが存在しないことの証明
- マルウェア解析：難読化されたコードの振る舞いを理解
代表的なツールとしてKLEE（LLVMベース）やAngr（バイナリ解析）があります。パス爆発問題（条件分岐が増えると解析すべきパスが指数的に増加する問題）という課題があるものの、ファジングとの組み合わせなど研究が進んでいます。ソフトウェアの信頼性を高める重要な静的解析技術として、学術・産業の両分野で活用されています。
使い方・例文
セキュリティ研究者がバイナリプログラムに対してシンボリック実行ツールを走らせ、「どんな入力値を与えたときにクラッシュするか」を自動的に探索するといった場面で登場します。
この用語をシェア
最終更新: