私の質問はこの質問に関連しており、@ RollfRollesの優れた回答があります。 M.D. Preda et alの論文はかなり技術的であるため、彼らの考えを理解しているかどうか疑問に思います。次のフレーズは、この論文から引用されています。
基本的な考え方は、攻撃者を具体的なプログラムの動作、つまり具体的なプログラムのセマンティクスの抽象的な解釈としてモデル化することです。このフレームワークでは、攻撃者は、不透明な述語の抽象的な検出が具体的な検出と同等である場合に、不透明な述語を破ることができます。
私が理解しているように、攻撃者は正式な抽象解釈(AI)としての健全な近似を使用してプログラムのプロパティを取得しようとしている誰かとしての攻撃者のモデル。 AI手順が完了すると、攻撃者は成功します(非公式に言えば、抽象ドメインで取得された固定小数点は、具体的なドメインの固定小数点にも「マップ」されます)。
具体的には、攻撃者はモデルは、不透明な述語を解決するAIベースのアルゴリズムと見なすことができます。実際、このアイデアはいたるところに広がっています(たとえば、この論文で、著者はSMTソルバーで使用されるDPLLアルゴリズムも一種の抽象解釈であることを証明しています)。
明らかに、抽象解釈が完了していない最悪の場合、攻撃者は必要なプロパティを回復できない可能性があります(たとえば、近似することはできますが、適切に設計された不透明な述語の正確なソリューションを回復することはありません)。すべての攻撃をAIでモデル化できるかどうかはまだわからないため、抽象ドメインとしての攻撃者のモデルにはいくつかの制限があるのではないかと思います。次に、簡単な質問が私に届きます。「攻撃者が他の方法を使用して不透明な述語を解決するとどうなりますか?」
簡単な例として、攻撃者は動的分析を使用して不透明な述語をバイパスできます(彼はいくつかの誤りを受け入れますが、最終的には必要なプロパティを取得できる可能性があります)。
いくつか提案をお願いします?