MASTG-KNOW-0116 シンボリック実行 (Symbolic Execution)

ほとんどのプロフェッショナルな GUI ベースの逆アセンブラはスクリプト機能と拡張性を備えていますが、特定の問題を解決するにはあまり適していないことがあります。リバースエンジニアリングフレームワークは重量のある GUI に依存することなくある種のリバースエンジニアリングタスクを実行および自動化できます。特に、ほとんどのリバーシングフレームワークはオープンソースであるか、フリーで利用可能です。モバイルアーキテクチャをサポートする一般的なフレームワークには radare2 (iOS) と Angr があります。

例：シンボリック実行やコンコリック実行を使用したプログラム解析

2000年代後半には、シンボリック実行ベースのテストがセキュリティ脆弱性を特定する手段として普及しました。シンボリック「実行」とは実際にプログラムを通る可能性のあるパスを一次論理の式として表現するプロセスを指します。充足可能性モジュロ理論 (SMT) ソルバーを使用してこれらの式の充足可能性をチェックし、解決された式に対するパス上の特定の実行点に到達するために必要な変数の具体的な値などのソリューションを提供します。

簡単に言えば、シンボリック実行とはプログラムを実行せずに数学的に解析することです。解析の中で、それぞれの未知の入力は数学的変数 (シンボリック値) として表されるため、これらの変数に対して実行されるすべての操作は操作のツリー (別名、AST (抽象構文木)、コンパイラ理論より) として記録されます。これらの AST は SMT ソルバーにより解釈されるいわゆる 制約 に変換できます。この解析の最後に、変数は値が不明な入力となる最終数学方程式が得られます。SMT ソルバーは最終状態を与えられた入力変数に可能な値を与えるためにこれらの方程式を解く特別なプログラムです。

これを説明するために、一つの入力 (x) を取り、二つ目の入力 (y) の値で乗算する関数を想像してください。最後に、if 条件があります。計算された値が外部変数 (z) の値よりも大きいかどうかをチェックし、true の場合は "success" を返し、そうでなければ "fail" を返します。この操作の方程式は (x * y) > z になるでしょう。

関数が常に "success" (最終状態) を返すようにしたい場合、対応する方程式を満たす x と y (入力変数) の値を計算するように SMT ソルバーに伝えることができます。グローバル変数の場合と同様に、それらの値はこの関数の外部から変更でき、この関数が実行されるたびに異なる出力となる可能性があります。これにより正しいソリューションを決定する際の複雑さが増します。

内部的な SMT ソルバーはさまざまな方程式解法を使用して、そのような方程式の解を生成します。いくつかの技法は非常に高度であり、それらの議論は本書の範疇を超えています。

現実世界の状況では、関数は上記の例よりもはるかに複雑です。関数の複雑さが増すと従来のシンボリック実行に大きな課題が生じる可能性があります。課題のいくつかを以下に要約します。

• プログラム内のループと再帰は 無限実行ツリー につながる可能性があります。

• 複数の条件分岐やネストされた条件は パス爆発 につながる可能性があります。

• シンボリック実行により生成された複雑な方程式は SMT ソルバーの制限により解決できない可能性があります。

• プログラムはシンボリック実行では処理できないシステムコール、ライブラリコール、またはネットワークイベントを使用しています。

これらの課題を克服するには、通常、シンボリック実行を 動的実行 (具象的実行 とも呼ばれる) などの他の技法と組み合わせて、従来のシンボリック実行に特有のパス爆発を軽減します。この具象的な (実際の) 実行とシンボリック実行の組み合わせは コンコリック実行 (concolic という名前は concrete と symbolic に由来します) と呼ばれ、 動的シンボリック実行 と呼ばれることもあります。

これを視覚化するために、上記の例では、さらにリバースエンジニアリングを実行するかプログラムを動的に実行してこの情報をシンボリック実行解析に渡すことにより、外部変数の値を取得できます。この追加情報により方程式の複雑さを軽減し、より正確な解析結果を生み出すこともあります。改善された SMT ソルバーと現在のハードウェアスピードを併せることで、コンコリック実行は中規模のソフトウェアモジュール (10 KLOC 程度) のパスを探索できます。

さらに、シンボリック実行はコントロールフローグラフの簡素化など逆難読化タスクのサポートにも役立ちます。例えば、Jonathan Salwan と Romain Thomas は 動的シンボリック実行を使用して VM ベースのソフトウェア保護をリバースエンジニアリングする方法を示しました [#salwan] (つまり、実際の実行トレース、シミュレーション、シンボリック実行を組み合わせて使用します) 。

シンボリック実行 (Symbolic Execution) では、シンボリック実行を使用して Android アプリケーションの簡単なライセンスチェックをクラックするためのウォークスルーを説明します。