10

私は最近、EJ Schwartz 博士による「Dynamic taint Analysis と Forward Symbolic Execution について知りたいことすべて (ただし、質問することを恐れていた可能性があります)」というタイトルの論文を読みました。論文では、彼は主にバイナリ レベルのセキュリティ コンテキストでのアプリケーションについて話しました。

動的汚染分析と前方シンボリック実行の正確な違いに興味があります。

私が見る限り、汚染分析は、x に格納されている情報がオブジェクト y に転送されるたびに、オブジェクト x(ソース) からオブジェクト y(シンク) への情報の流れを追跡します。したがって、主な関心事は、どのオブジェクトがソースによって推移的に影響を受ける可能性があるかということです。シンボリック実行では、一部の入力をシンボリック値として扱い、他の変数をシンボリック値で表現しようとします。それにより、シンボリック入力が後続のプログラムに影響を与える条件について答えます。

バイナリ レベルでは、リターン アドレスの上書きによって引き起こされる脆弱性とともに、テイント分析が頻繁に言及されていることがわかります。一方、シンボリック実行は、整数オーバーフロー、ランタイム アサーション エラー、リソース リーク(メモリ リーク、ファイルのオープン/クローズなど)、バッファ オーバーフローなど、より多くのタイプの脆弱な問題に対処できます。

しかし、最新の汚染分析にはデータ フロー分析だけが含まれているわけではないようです。それらのほとんどは、制御フローの状態を追跡します。また、いくつかの脆弱性検出シナリオでは、汚染された入力もシンボリック値として表され、シンボリック実行と同様に伝播されます。一方、シンボリック実行エンジンは、基礎となる制約ソルバーと実行/解釈ランタイムの制限により、異なるパス条件で区切られたシンボリック値を完全に使用することはできません。そのため、期待どおりの高い分岐またはパスカバレッジを実現できません。

では、一般的なケースでは、汚染分析は一種の粗いシンボリック実行であると言えますか、それともシンボリック実行は一種の正確な汚染分析であると言えますか?

4

4 に答える 4

2

興味深い質問です！ここに私の 2 セントがあります:シンボリック実行は一種の汚染分析を使用してパス制約を構築します。シンボリック実行では、SMT/SAT ソルバーも使用して、特定のパス制約が満たされるように、変数や入力の具体的な値を生成します。

テイント分析は SMT/SAT ソルバーを使用しないため、一種のシンボリック実行ではないと言えます。テイント分析はシンボリック実行の一部であると言えるかもしれません。

これは単なる意見です。気軽にチャレンジしてください。

于 2015-12-16T16:58:36.310 に答える
0

私は@Bennyに同意します。それは本当に興味深い質問です。この種の質問を定式化することでおそらく多くのことを学び、それらに答えようとするとさらに多くのことを学びます.

ベニーの答えに追加したいと思います：

汚染追跡とシンボリック実行を実装するには、言語のセマンティクスを定義する必要があります (バイナリの場合の x86 アセンブリなど)。たとえば、次のことを説明する必要があります。

add eax, ebx

「手段」、つまり、状態に対して行います。汚染追跡セマンティクスの定義は、シンボリック実行セマンティクスの一種のサブセットと見なすことができます。汚染追跡セマンティクスは、シンボリック実行セマンティクスでエンコードされます。共通部分は

  • 汚染されている場合ebxは、汚染eaxされています。
  • ebxシンボリック (iow に 1 つ以上のシンボリック変数を含む SMT 式が含まれる) の場合、シンボリックeaxです

それでも、シンボリック実行のセマンティクスには、さらに詳しい情報 (正確な算術演算など) が含まれている必要がeaxありeaxますebx。

コメントするか、私を修正してください！

于 2016-02-26T17:56:00.823 に答える
0

私の意見では、あなたの質問に答えるには、次の質問に答える必要があります。ii) テイント分析は、シンボリック実行が可能なすべての実行パスを見つける可能性を秘めていますか? iii) どちらも同じ実行パスを見つける可能性が同じですか? iv) 両者は、他方が計算できない実行パスを計算できますか。

私の意見では、iv) は正しいです。つまり、サブセットではないということです。ただし、実際には大きな重複があることに同意します。

オプション i) と iii) を削除できます。これは、シンボリック実行では実行可能な実行パスのみが検出されるのに対して、テイント分析では実行不可能な実行パスが検出される可能性があるため、制約解決に頼らないためです。

オプション ii) を排除するために、シンボリック実行では公開でき、テイント分析では公開できない実行パスがあると思います (間違っていれば訂正してください)。例えば：

for(int i=0;i<3;i++) {
   if(someString.charAt(i)=='4')
       //do something
   else
       //do something else
}

このような場合、シンボリック実行は 8 つの可能な実行パスすべてを公開しますが、テイント分析 (私が間違っていなければ) は公開しません。

于 2016-11-24T19:35:47.697 に答える