前の記事のコメントで、 amaraoから非常に良い質問がありました 。 彼は、どのようなルールを使用して、ソフトウェアの脆弱性をどのように探すかを尋ねました。 この質問の一部を紹介します。

どのアルゴリズムで、どのルールで？ または、それはすべて「気まぐれ」です。 この場合、メソッドはどこかで絶対的なケースとして何かを説明しません-どこかではないと思いました。

この質問により、 アマラオは 、自発的または非自発的に、ソフトウェアの脆弱性を評価する際の客観性の問題、この評価がそれを行う専門家にどの程度依存するか、または依存しないかについて注意を喚起します。 この質問は非常に重要であるため、セキュリティの専門家とクライアントの両方で頻繁に発生します。

実際、提供された製品の安全性を客観的に評価できない場合、どのようにしてニーズに最適な製品を選択できますか？ もちろん、すべてのメーカーは、これまでに作成された中で最も安全なのは自社製品であることを誓います。 さらに、それぞれが、おそらく、それを信じて、正当な理由で信じます。

認証などの独立企業によるソフトウェアの評価は、この問題を解決できるようです。 しかし、客観的な分析手段がない場合、評価自体の品質をどのように検証できますか？ 実際、この場合のソフトウェア製品の評価は、それ自体が製品、サービスです。

これらの質問は非常に頻繁に議論されるという事実にもかかわらず、私はそれらに対する明確な答えを見ませんでした。 しかし、この分野での仕事中に、現代の技術の可能性について特定のアイデアを開発しました。

この記事では、次の考えを説明します。今日、セキュリティの客観的な評価を保証する脆弱性を検索するアルゴリズムはありません。 したがって、製品に対する信頼は、製品を評価した専門家の評判とその操作の経験（実際には、防御を克服しようとしたクラッカーの評判）のみに基づいています。

---

既存のすべての脆弱性検索方法は、フォーマルとエキスパートの2つのカテゴリに分類できます。

ソフトウェアの脆弱性を見つける正式な方法は、正式な開発方法と非常に密接に関連しています。 それらは、設計された製品の仕様に対して明確に定義された意味を持つ言語の使用に基づいています。 受け取ったプロジェクトの正確性をチェックするための数学的方法。 自動化されたプログラムコード生成。 検証プロセス中に、潜在的な脆弱性の評価が行われます。

その名が示すように、エキスパートメソッドは評価者の知識と経験に基づいています。 定義上、これらのメソッドを完全に客観的と呼ぶことはほとんどできないという事実にもかかわらず、私はそれらから始めます。

エキスパートメソッド

エキスパートメソッドは、情報システムが多かれ少なかれよく知られたパターンに従って作成されるという事実に基づいています。 アーキテクチャパターン、デザインパターン、コードがあります。 開発者は、よく知られたセキュリティツールとテクニックを使用します。 プログラムは、よく知られたプログラミング言語で作成され、一般的なオペレーティングシステムの制御下で動作し、アクセス可能なライブラリを使用し、利用可能なサービスにアクセスします。 そして、これらの各パターンを使用すると、特定の脆弱性が出現する可能性が広がります。

そのため、たとえば、プログラムがC、C ++で記述されている場合、「悪用可能な」バッファオーバーフローを見つけることができます。 プログラムのリクエスト言語が非常に複雑な場合、APIの不正使用方法を使用した攻撃に対して脆弱になる可能性があります。 プログラムがパスワードを使用してユーザーを認証する場合、パスワードを取得する可能性があります。 DBMSプログラムは、多くの場合、SQLインジェクションに対して脆弱です。 ご想像のとおり、このリストは膨大です。

より複雑なシステムは、その構成部分に分解されます。 次に、これらの部分とその相互作用を分析します。

したがって、サーバーとクライアントの部分で構成されるシステムでは、サーバー、クライアント、およびそれらの間の相互作用のプロトコルを分析する必要があります。 この場合、個々のパーツをコンポーネントに分割すると便利な場合があります。 たとえば、サーバー部分は多くの場合、DBMSとアプリケーションサーバーで構成されます。 また、アプリケーションサーバーは、オペレーティングシステムのいくつかのプロセスとして実装できます。 各プロセス-1つまたは別のライブラリを使用します。

実際、この手法は、相互作用する部分の形でプログラムまたはシステムの何らかの表現を見つけることになります。 このビューにより、利用可能な履歴情報に基づいて、各部分の脆弱性とそれらの相互作用に関連する脆弱性を分析できます。

エキスパートアプローチの良い例は、Microsoftが開発および使用した方法です。 この方法は、特に「ThreatModeling」[ 1 ]という本で説明されています。 情報フロー図を使用してプログラムのアーキテクチャを分析し、攻撃ツリーを使用して結果を表します。

したがって、エキスパートメソッドは、プログラムを適切に分解するスペシャリストの能力と、さまざまなタイプのプログラムおよびプロトコルの脆弱性に関する知識に基づいています。

正式な方法

私の経験では、「数学の使用」は、ほとんど魔法のアクションのようにa敬の念を抱いて認識されることがあります。 「銀の弾丸」のタイトルの候補となるのは、多くの人が理解している数学的、正式な方法であり、それらを使用して得られた結果は十分に批判的に認識されていません。

もちろん、正式な方法を使用すると、より優れたソフトウェアを作成できます。 彼らは、信頼性および/またはセキュリティのためのプログラムに対する要求が増加している分野で、すでにアプリケーションを見つけています。 それらの使用分野は徐々に拡大しており、おそらくこの記事を読んでいる人は、少なくともそのような方法の要素をすでに使用しているか、将来使用するでしょう。 時間の経過とともに、正式な手段を使用することで、製品の品質が向上し、開発とサポートのコストが削減されると考えています^* 。

一方、正式な方法は優れた結果を提供しますが、それらの制限を理解する必要があります。 数学モデルの構築と研究に携わってきたすべての人は、どのモデルも元々そこに置かれたもの以上のものを与えられないことを教えてくれるでしょう。

例として、非常に単純なプロトコルを実装する非常に単純なプログラムの非常に単純なモデルを取り上げましょう。

簡単な例

プログラムは、開始して初期化した後、ユーザーからの接続が確立されるのを待つ必要があります。 接続が確立されると、プログラムはユーザーからユーザー名とパスワードを受け取ります。 それらが正しいことが判明した場合、プログラムはユーザーに何らかの情報、ドキュメントを転送することができます。 転送が完了すると、プログラムは切断され、新しい接続を待つ必要があります。

このプログラムを使用して、未登録のユーザーが情報にアクセスできないようにします。

これを行う1つの可能な方法は、オートマトンモデルを構築して探索することです。

このプログラムをシミュレートするマシンの回路図を次の図に示します。







このモデルでは、I→II→III→IとI→II→Iの2つのルートのみが可能です。

考えられるすべてのルートを検討した結果、認証を正常に渡すことによってのみドキュメントが読み取られる状態になることができるという結論に達しました。 結果の結論は、プロジェクトの正しさを確認します。 もちろん、単純なシステムの場合、これは明らかでした。より複雑な状況では、「間違った」方法を見つけたかもしれません。

システムが認証なしでドキュメントを読み取る状態に入るルートを見つけることができた場合、これは脆弱性を発見したことを意味します。 さらに、対応する遷移を行うために各状態でどのようなリクエストを行う必要があるかがわかるため、システムを攻撃する方法がすぐにわかります。

ここにあるように見える-脆弱性分析アルゴリズム。 モデルを作成し、研究しました。 攻撃方法またはシステムのセキュリティに関する結論が出力で受信されました。 ただし、各モデルは特定のタイプの脆弱性を見つけるのに役立つことに注意してください。この場合、これらはユーザーとプログラム間で交換されるメッセージのシーケンスのエラーです。 そして、特定のタイプの脆弱性を見つけることが期待されるため、このモデルまたはそのモデルを構築しています。

数学モデルの研究に基づいてプログラムの安全性を主張するとき、シミュレートされたプログラムの特性とそれが動作する環境に関する多くの仮定に依存します。

モデルの仮定

単純なモデルを作成するときに行った仮定のいくつかについて説明しましょう。

おそらく、最も明白な前提は、正しいパスワードを提供したユーザーがログインしていることです。 モデルは、パスワードの傍受、選択、ユーザーからの盗難の問題を考慮しません。 この観点からプログラムを評価するには、追加の調査が必要です。

それほど明白な仮定はありません。 たとえば、ドキュメントを受け取るユーザーは、名前とパスワードを入力したユーザーと同じです。 これは、セッションのインターセプトを含むすべての攻撃を考慮から除外します。

これまで見てきたように、非常に単純なプログラムを調査する場合でも、多くの仮定に頼らざるを得ません。 より複雑なシステムの場合、これはさらに真実です。 特定のソフトウェア製品またはシステムのセキュリティについて結論を出すたびに、攻撃者の限られた能力に関する多くの仮定に頼っています。

いくつかの仮定は検証できます。 たとえば、場合によっては、セッションが傍受されないと主張することができます。 ユーザーがローカルのキーボードとモニターを使用し、オペレーティングシステムが「信頼できるパス」をサポートしている場合、それは非常に妥当なように見えます。 はい、私はほとんど忘れていました。おそらく、ユーザーが椅子から出るとセッションが自動的に中断されると仮定する必要があります...

他の仮定は検証できません。 攻撃者の物理的能力の境界がわからないため、それらのいくつかは検証できません。 たとえば、コンピューターの電磁放射を遮断する能力。 攻撃者が何を持っているのかを推測できますが、この知識に自信を持つ根拠さえあるかもしれません。 しかし、最後まで確信が持てません。 おそらく、明日、状況は大きく変わるでしょう。 攻撃の手段がすでに比較的無料でアクセスされている可能性がありますが、まだわかりません。

一部の論理的な仮定も検証できません。 この仮定の例は、RSAアルゴリズムのセキュリティです。 私の知る限り、その非亀裂の厳密な正式な証拠は存在しません。 これは、ハッキング技術が明日登場する可能性があり、このアルゴリズムの使用に基づくすべてのシステムが安全でなくなることを意味します。 さらに、このアルゴリズムを攻撃する方法を誰もまだ知らないことを完全に確信することはできません。 もちろん、現在RSAが安全であると信じるには十分な理由がありますが、自問してみてください：数十億ドルの価値のあるビジネス（これが興味深いターゲットになる場合）を完全にRSAに依存させますか？

これらの仮定がすべて、私たちが何かを知っているという事実-特定の問題を解決する方法-ではなく、私たちが何かを知らないという事実と関連しているのは興味深いことです 。 いずれかのステートメントを確認する必要があるたびに、問題が発生します。この問題を解決することはできず、誰もこれを行うことができません。または、解決方法はわかっていますが、わかりませんか？

数学の学校のコースを少なくとも覚えている人は誰でも、すべての数学モデルは公理に基づいていることに簡単に気付くでしょう-モデル自体の中の証明不可能な仮定。 そして、「良い」モデルと「悪い」モデルの違いは、行われた仮定の信頼性にのみあります。 「これを実行できない」などのステートメントをテストすることは、「これを実行できる」と言うよりもはるかに複雑です。 これでは、専門家を信頼することを余儀なくされています。

そして、セキュリティの分野における正式なモデルの主観性、専門家の経験への依存性について、一見逆説的な結論に達しました。

結論

脆弱性の欠如は、たとえばプログラムの機能やその速度を実証する方法とは対照的に実証できません。 私たちは専門家の意見を信頼せざるを得ません。

専門家が特定のシステムを攻撃する方法を知らなくても、これが安全であることを意味するわけではありません。 とにかく、専門家がこれを知っていなくても、そのような方法が存在しないことを完全に確信することはできません。

この場合、専門家または専門家コミュニティのみが、どのチェックを行う必要があるか、分析されたプログラムの脆弱性を検索するためにどのような努力が必要かを判断できます。 彼は、そのようなシステムでの攻撃方法に関する知識に基づいてこれを行うことができます。 そして、監査結果の信頼性は、監査を実施した専門家の評判にのみ基づいています。

そして、記事全体のロジックの範囲内で仕上げたいと思います。

明日、ビッグディスカバリーは行われず、その結果、この記事で述べられたことはすべて間違っていると言えますか？ いいえ、できません。

このビッグディスカバリーはまだ誰にも作られていないと思いますか？ これがまだ起こっていないと信じる理由があります。 しかし、私は完全に確信することはできません。

ご注意

*比較的セキュリティのない一般的な形式的なアプローチに興味がある場合は、「形式的な方法を理解する」[ 2 ]の本に興味があるかもしれません。

別の本はコンピューターセキュリティです。 芸術と科学」[ 3 ]には、ソフトウェアセキュリティを分析するための正式な方法に特化した別の章を含む、情報セキュリティの数学モデルに関する多くの情報が含まれています。

文学

1. Frank Swiderski、Window Snyder「Threat Modeling」、Microsoft Press 2004、ISBN 978-0-7356-1991-3

2. Jean Francois Monin、Michal G. Hichey（編集者）「Understanding Formal Methods」、Springer-Verlag 2003、ISBN 1-85233-247-6

3.マット・ビショップ「コンピューターのセキュリティ。 芸術と科学」、Addison-Wesley 2003、ISBN 0-201-44099-7