結腸検査

コンコリックテスト（concreteとsymbolicを組み合わせた造語で、動的シンボリック実行とも呼ばれる）は、プログラム変数をシンボリック変数として扱う古典的な手法であるシンボリック実行を、具体的な実行（特定の入力に対するテスト）パスに沿って実行するハイブリッドソフトウェア検証手法です。シンボリック実行は、コードカバレッジを最大化することを目的として、制約論理プログラミングに基づく自動定理証明器または制約ソルバーと組み合わせて、新しい具体的な入力（テストケース）を生成するために使用されます。その主な目的は、プログラムの正しさを証明することではなく、実際のソフトウェアにおけるバグを見つけることです。

この概念の説明と議論は、Patrice Godefroid、Nils Klarlund、Koushik Sen による「DART: Directed Automated Random Testing」で紹介されました。^{[ 1 ]} Koushik Sen、Darko Marinov、Gul Aghaによる論文「CUTE: A concolic unit testing engine for C」^{[ 2 ]}では、このアイデアをデータ構造にさらに拡張し、 concolic testingという用語を初めて作り出しました。同様のアイデアに基づいた別のツール、EGT (後に EXE に改名され、さらに改良されて KLEE に改名) は、2005 年に Cristian Cadar とDawson Englerによって独自に開発され、2005 年と 2006 年に公開されました。^{[ 3 ]} PathCrawler ^{[ 4 ] [ 5 ]}は、具体的な実行パスに沿ってシンボリック実行を実行することを最初に提案しましたが、コンコリックテストとは異なり、PathCrawler は具体的な値を使用して複雑なシンボリック制約を単純化しません。これらのツール（DART、CUTE、EXE）は^、 Cプログラムの単体テストにコンコリック テストを適用し、コンコリック テストは、確立されたランダム テスト手法に対するホワイト ボックス改善として最初に考案されました。この手法は後に、 jCUTE [ ^{6 ]}を使用したマルチスレッドJavaプログラムのテストや、実行可能コードからの単体テスト (ツール OSMOSE ^{[ 7 ]}に一般化されました。また、 Microsoft Researchの SAGEにより、ファジング テストと組み合わせて、大規模なx86バイナリの悪用可能なセキュリティ問題を検出するように拡張されました。 ^{[ 8 ] [ 9 ]}

コンコリックアプローチはモデル検査にも適用できます。コンコリックモデルチェッカーでは、モデルチェッカーは検査対象のソフトウェアを表すモデルの状態をたどりながら、具体的な状態と記号的な状態の両方を保存します。記号的な状態はソフトウェアのプロパティをチェックするために使用され、具体的な状態は到達不可能な状態に到達しないようにするために使用されます。そのようなツールの1つが、Sharon Barner、Cindy Eisner、Ziv Glazberg、Daniel Kroening、Ishai RabinovitzによるExpliSATです^{[ 10 ]。}

従来の記号実行に基づくテストを実装するには、プログラミング言語用の本格的な記号インタプリタを実装する必要があります。コンコリックテストの実装者は、記号実行を計測によってプログラムの通常の実行に組み込むことができれば、本格的な記号実行の実装を回避できることに気づきました。この記号実行の実装を簡素化するというアイデアが、コンコリックテストの誕生につながりました。

C言語で書かれた以下の簡単な例を考えてみましょう。

void f ( int x , int y ) {int z = 2 * y ;if ( x == 100000 ) {if ( x < z ) {assert ( 0 ); /* エラー */}}}

xとyにランダムな値を試すような単純なランダムテストでは、不具合を再現するために非現実的なほど多くのテストが必要になるだろう。

まず、 xとyを任意に選択し、例えばx  = y = 1とします。具体的な実行では、2行目でzを2に設定し、3行目のテストは1≠100000であるため失敗します。同時に、記号的な実行では同じパスをたどりますが、xとyを記号変数として扱います。zを式2yに設定し、3行目のテストが失敗したためx ≠100000であることを確認します。この不等式はパス条件と呼ばれ、現在の実行と同じ実行パスをたどるすべての実行で真でなければなりません。   

次回の実行時にプログラムが異なる実行パスをたどるようにしたいので、最後に遭遇したパス条件x ≠ 100000 を否定して、x = 100000 とします。次に、自動定理証明器を呼び出し、記号実行中に構築された記号変数の値とパス条件の完全なセットに基づいて、入力変数xとy の値を求めます。この場合、定理証明器からの有効な応答は、x = 100000、y = 0 となる可能性があります。

この入力でプログラムを実行すると、4行目の内部分岐に到達しますが、100000 ( x ) が 0 ( z = 2 y )より小さくないため、この分岐は実行されません。パス条件はx = 100000 およびx ≥ zです。後者は否定され、x < zとなります。次に、定理証明器は、x = 100000、x < z、およびz = 2 yを満たすx、yを探します。たとえば、x = 100000、y = 50001 です。この入力でエラーが発生します。

基本的に、コンコリック検定アルゴリズムは次のように動作します。

1. 特定の変数群を入力変数として分類します。これらの変数は、記号実行時に記号変数として扱われます。その他の変数はすべて具体的な値として扱われます。
2. シンボル変数の値やパス条件に影響を与える可能性のあるすべての操作、および発生したエラーがトレースファイルに記録されるように、プログラムを計測してください。
3. まず、任意の入力値を選択してください。
4. プログラムを実行してください。
5. トレース上でプログラムを記号的に再実行し、一連の記号制約（パス条件を含む）を生成する。
6. まだ否定されていない最後のパス条件を否定して、新しい実行パスを探索する。そのようなパス条件が存在しない場合、アルゴリズムは終了する。
7. 新しいパス条件セットに対して自動充足可能性ソルバーを呼び出し、新しい入力を生成します。制約を満たす入力がない場合は、ステップ6に戻り、次の実行パスを試みます。
8. ステップ4に戻ってください。

上記の手順にはいくつかの問題点があります。

• このアルゴリズムは、実行可能なパスの暗黙的なツリーに対して深さ優先探索を実行します。実際には、プログラムは非常に大きな、あるいは無限のパスツリーを持つ場合があります。よくある例としては、サイズや長さが無制限のデータ構造をテストする場合が挙げられます。プログラムのごく一部に時間をかけすぎないように、探索の深さを制限する（境界を設ける）ことがあります。
• 記号実行と自動定理証明器には、表現および解決できる制約の種類に制限があります。たとえば、線形算術に基づく定理証明器は、非線形パス条件xy = 6 に対応できません。このような制約が発生するたびに、記号実行は問題を単純化するために、いずれかの変数の現在の具体的な値を代入することがあります。コンコリックテストシステムの設計において重要なのは、対象となる制約を表現するのに十分な精度を持つ記号表現を選択することです。

シンボリック実行に基づく分析とテストは、一般的に業界から大きな関心を集めています。動的シンボリック実行（別名コンコリックテスト）を使用する最も有名な商用ツールは、おそらくマイクロソフトのSAGEツールでしょう。KLEEとS2Eツール（どちらもオープンソースツールで、STP制約ソルバーを使用）は、Micro Focus Fortify、NVIDIA、IBMなど、多くの企業で広く使用されています。これらの技術は、セキュリティ脆弱性を発見するために、多くのセキュリティ企業やハッカーによってますます活用されています。

コンコリックテストにはいくつかの限界がある。

• プログラムが非決定的な動作を示す場合、意図した経路とは異なる経路をたどる可能性があります。これにより、検索が終了せず、カバレッジが低下する可能性があります。
• 決定論的なプログラムであっても、不正確な記号表現、不完全な定理証明、大規模または無限のパスツリーの中で最も有益な部分を探索できないことなど、多くの要因によってカバレッジが低下する可能性がある。
• 暗号プリミティブのように、変数の状態を徹底的に混合するプログラムは、実際には解くことのできない非常に大きな記号表現を生成します。例えば、この条件では、定理証明器がSHA-256if (sha256_hash(input) == 0x12345678) { ... }を逆算する必要がありますが、これは未解決問題です。

• pathcrawler-online.comは、評価および教育目的でオンラインテストケースサーバーとして一般公開されている、現在のPathCrawlerツールの制限付きバージョンです。
• jCUTEは、アーバナ・シャンペーン大学によりJava版として研究用途限定ライセンスの下でバイナリ形式で提供されています。
• CRESTはC言語用のオープンソースソリューションで、^{[ 11 ]} CUTE（修正BSDライセンス）に取って代わったものです。
• KLEEは、 LLVMインフラストラクチャ（UIUCライセンス）上に構築されたオープンソースソリューションです。
• CATGはJava向けのオープンソースソリューションです（BSDライセンス）。
• Jalangiは、JavaScript用のオープンソースのコンコリックテストおよびシンボリック実行ツールです。Jalangiは整数と文字列をサポートしています。
• Microsoft Riseで開発されたMicrosoft Pexは、.NET Framework用のMicrosoft Visual Studio 2010 Power Toolとして一般公開されています。
• Tritonは、バイナリコード用のオープンソースのコンコリック実行ライブラリです。
• CutErは、Erlang関数型プログラミング言語向けのオープンソースのコンコリックテストツールです。
• Owi ^{[ 12 ]}は、 C、C++、Rust、WebAssembly、Zig用のオープンソースのコンコリックエンジンです。

DARTやSAGEをはじめとする多くのツールは一般には公開されていません。ただし、例えばSAGEはマイクロソフト社内でセキュリティテストに「日常的に」使用されていることに注意してください。^{[ 13 ]}