セキュリティの脆弱性がソフトウェア システムに存在しないことを示すために、自動化された定理証明機能を使用するという話を少し聞いたことがあります。一般に、これを行うのは非常に困難です。
私の質問は、既存または提案されたシステムの脆弱性を見つけるために、同様のツールを使用する作業を行った人はいますか?
Eidt:ソフトウェア システムが安全であることを証明することについて質問しているわけではありません。私は、(理想的には以前は知られていない) 脆弱性 (またはそれらのクラス) を見つけることについて質問しています。ここではブラック ハットのように (しかしそうではありません) 考えています。システムの正式なセマンティクスを説明し、攻撃したいものを説明してから、システムを乗っ取るために使用する必要がある一連のアクションをコンピューターに判断させます。
はい、この分野で多くの作業が行われました。充足可能性 (SAT および SMT) ソルバーは、セキュリティの脆弱性を見つけるために定期的に使用されます。たとえば、Microsoft では、Windows からバッファ オーバーランのバグを根絶するためにSAGEと呼ばれるツールが使用されています。SAGE はZ3 定理証明を使用します充足可能性チェッカーとして。「スマート ファジング」や「ホワイト ボックス ファジング」などのキーワードを使用してインターネットを検索すると、セキュリティの脆弱性を見つけるために充足可能性チェッカーを使用しているプロジェクトが他にもいくつか見つかります。大まかな考え方は次のとおりです。プログラム内の実行パスを収集し (実行できなかった、つまり、プログラムを実行させる入力が見つからなかった)、これらのパスを数式に変換します。これらの式を充足可能性ソルバーに入力します。アイデアは、プログラムに特定のパスを実行させる入力がある場合にのみ、満足/実行可能な式を作成することです。生成された式が充足可能 (つまり、実行可能) である場合、充足可能性ソルバーは割り当てと目的の入力値を生成します。ホワイトボックス ファザーは、実行パスの選択にさまざまな戦略を使用します。主な目標は、クラッシュにつながるパスをプログラムに実行させる入力を見つけることです。
したがって、少なくとも意味のある意味では、何かが安全であることを証明することの反対は、安全でないコード パスを見つけることです。
Byron Cook の TERMINATOR プロジェクトを試してみてください。
そして、Channel9 で少なくとも 2 つのビデオ。 ここにそれらの1つがあります
彼の研究は、この非常に興味深い研究分野について学ぶ良い出発点になるでしょう。
Spec# や Typed-Assembly-Language などのプロジェクトも関連しています。安全性チェックの可能性を実行時からコンパイル時に戻すという彼らの探求の中で、コンパイラは多くの悪いコード パスをコンパイル エラーとして検出できます。厳密には、それらはあなたが述べた意図を助けるものではありませんが、彼らが利用する理論はあなたにとって役立つかもしれません.
私は現在、他の誰かと一緒に Coq で PDF パーサーを書いています。この場合の目標は安全なコードを生成することですが、このようなことを行うことは、致命的なロジック バグの発見に確実に役立ちます。
ツールに慣れれば、ほとんどの証明は簡単になります。より難しい証明は興味深いテストケースをもたらし、実際の既存のプログラムでバグを引き起こすことがあります。(そして、バグを見つけるためには、見つけるべきバグがなく、深刻な証明が必要ないことを確認したら、単純に定理を公理として仮定することができます。)
約 1 か月前に、複数の / 古い XREF テーブルを含む PDF の解析で問題が発生しました。解析が終了したことを証明できませんでした。これについて考えて、予告編で /Prev ポインターをループさせて PDF を作成しました (誰がそれを考えるでしょうか? :-P)。(最も注目すべきは、Ubuntu のほぼすべての poppler ベースのビューアーです。私の CPU をすべて消費したことで、私を笑わせ、Gnome/evince-thumbnailer を呪いました。彼らは今、それを修正したと思います。)
Coq を使用して低レベルのバグを見つけるのは困難です。何かを証明するには、プログラムの動作のモデルが必要です。スタック/ヒープの問題については、おそらく CPU レベルまたは少なくとも C レベルの実行をモデル化する必要があります。技術的には可能ですが、これは努力する価値がないと思います。
C に SPLint を使用するか、選択した言語でカスタム チェッカーを作成すると、より効率的になります。
まさにそれを行おうとしている L4 検証済みカーネルがあります。しかし、エクスプロイトの歴史を見ると、まったく新しい攻撃パターンが発見され、それまでに作成された多くのソフトウェアは攻撃に対して非常に脆弱です。たとえば、フォーマット文字列の脆弱性は 1999 年まで発見されませんでした。約 1 か月前に HD Moore がDLL ハイジャックをリリースし、文字通り Windows の下のすべてが脆弱です.
ソフトウェアが未知の攻撃に対して安全であることを証明することは不可能だと思います。少なくとも定理がそのような攻撃を発見できるようになるまではそうではありません.私の知る限り、これは起こっていません.
定理の証明とはあまり関係ありませんが、ファズ テストは脆弱性を自動的に発見するための一般的な手法です。
はい。多くの定理証明プロジェクトは、ソフトウェアの穴や欠陥を実証することで、ソフトウェアの品質を示しています。セキュリティ関連にするために、セキュリティ プロトコルの穴を見つけることを想像してみてください。カルロス オラルテ博士 ウーゴ・モンタナリの論文には、そのような例が 1 つあります。
それはアプリケーションにあります。セキュリティやその特別な知識と関係がある定理証明自体ではありません。
免責事項：自動定理証明器の経験はほとんどありません
いくつかの観察