問題タブ [symbolic-execution]

angrを使用して IoT ファームウェア ファイルを分析したいと考えています。angrのドキュメントを読みましたが、ファームウェア ファイルを分析する解決策が見つかりませんでした。では、 angrはどのようにしてファームウェアの CFG ファイルを生成するのでしょうか? または、シンボリック実行としてangrを使用してファームウェアファイルを分析するにはどうすればよいですか?

アサーションチェックにシンボリック実行を使用できないのはどのような状況ですか? 説明のために、次の例を取り上げます。

ここで、シンボリック実行を使用して、それ¬A ^ (B < 5) ^ Cが私たちの主張に違反していることを見つけることができます。ここで、最初の条件を次のように変更するとします。

この変更により、x と b の新しい値はわかりません。では、アサーション チェックにシンボリック実行を引き続き使用できますか?

一般的に、シンボリック実行を使用できない状況はありますか? つまり、プログラムの可能なすべての実行を分析しなければならない状況です。