State-inferer: LLM-Driven State Machine Extraction and Formal Verification for Secure Protocol Implementations
本論文は、プログラムスライシング、大規模言語モデル、および形式的なモデル検査を統合することで、ソースコードからプロトコルの状態マシンを正確に抽出し検証するホワイトボックスフレームワークであるState-infererを紹介するものであり、遷移レベルでの優れた精度を実現し、TLS、IKEv2、およびSSHの実装における4つの未知のセキュリティ脆弱性を発見した。
原論文は CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
デジタル世界のセキュリティは、コンピュータ同士がどのように通信するかを支配する目に見えないルールに大きく依存しています。ネットワークプロトコルとして知られるこれらのルールは、データが送信者から受信者へと安全に移動し、身元を検証し、秘密を守るように設計されています。その核心において、これらのプロトコルは厳格な台本（スクリプト）のように機能します。つまり、コンピュータはある特定の状態にある必要があり、特定のメッセージを受け取り、その後、次に進む前に新しい状態へと移行しなければならないのです。もしコンピュータがステップを飛ばしたり、誤った状態の時にメッセージを受け入れてしまったりすると、システム全体が侵害され、攻撃者がセキュリティチェックを回避したり、機密情報を盗み出したりすることが可能になります。数十年にわたり、セキュリティの専門家たちは、サーバー上で実際に動作しているコードが、この台本通りに完璧に従っているかどうかを検証しようと試みてきました。しかし、実際のコードは乱雑で、隠れた変数や複雑なロジックに満ちており、標準的なテストツールではマッピングが困難です。プログラムの実際の挙動が書かれた設計から逸脱したとき、危険な欠陥が目の前に潜み、悪用されるのを待っていることになるのです。
PLA情報工学大学の研究チームは、この問題を解決するための新しい手法を開発しました。「State-inferer」と呼ばれるこのツールは、複雑なコンピュータコードと、それが従うべき論理的ルールの間の「翻訳者」として機能します。このツールは、コード全体を一度に読み取ろうとしたり、ランダムなメッセージを送信してプログラムの挙動を推測したりするのではなく、コードを小さく扱いやすい断片へと分解します。それは「プログラム・スライシング」と呼ばれる技術を用い、特定のデータがソフトウェア内を移動する際にどのように変化するかを正確に追跡し、コンピュータが状態を切り替える原因となる正確なロジックを分離します。このプロセスは、絡まった毛糸玉の中から一本の糸を辿り、他の部分は無視して、その糸がどこへ繋がっているのかを正確に見極める作業に似ています。これらの特定の糸に焦点を当てることで、システムはプログラムが辿る正確なイベントのシーケンスを再構築できます。これには、標準的なツールが見落としがちな隠れた内部条件も含まれます。
研究者たちはその後、再構築されたこれらのシーケンスを、コードを理解し推論するように訓練された人工知能の一種である大規模言語モデルに投入しました。大量のテキストを単にAIに読ませようとする従来の試みとは異なり、このシステムは、プロトコルの各遷移（トランジション）ごとに、一つの小さく集中したコードの断片をAIに提供しました。これにより、AIは無関係な情報に圧倒されることなく、状態変化の完全なコンテキスト（文脈）を把握することができました。そしてAIは、プログラムの挙グの完全なマップを構築しました。どのメッセージが変化をトリガーしたかだけでなく、その変化が起こるためにどのような内部変数が真（true）である必要があるのかまでも記録しました。最後に、研究者たちは形式検証エンジンを使用して、このマップを公式のセキュリティルールと照らし合わせ、検証を行いました。このエンジンは厳格な監査役のように機能し、プログラムが取り得るあらゆる経路を体系的にテストし、例えば、安全な接続が完全に確立される前にデータを送信してしまうといった、ルールへの違反がないかをチェックします。
TLS、IKEv2、SSHを含む主要なセキュリティプロトコルの7つの異なるオープンソース実装を用いてテストを行った際、この新手法は驚くほど高い精度を証明しました。この手法は95.2パーセントの精度でコードの挙動を正しく特定し、約78.9パーセントの精度しか出せなかった既存の最高水準のツールを大幅に上回りました。この差は単なる軽微なエラーの問題ではありませんでした。この新しいツールは、外部からのメッセージではなく、内部タイマーやリソースチェックによって駆動される遷移など、他の手法が完全に見落としていた複雑な内部ロジックを捉えることに成功したのです。実際、研究者たちは、古い手法がプログラムの簡略化された視点に依存していたため、内部の詳細を無視してしまい、クリティカルな遷移の半分近くを見逃していたことが多いことを発見しました。全体像を捉えることで、この新ツールはソフトウェア内に存在していた4つの未知の脆弱性を発見することができました。これらの欠陥は、これまで発見されていなかったものであり、公式のセキュリティ識別子が割り当てられるほど深刻なものであり、修正のためにソフトウェアのメンテナーに報告されました。
最も重要な発見の一つは、これらの欠陥が単なる理論上の可能性ではなく、実際に悪用可能な弱点であったことです。ある事例では、サーバーが、必要な鍵交換を完了する前に重要なセキュリティメッセージを受け入れるように騙され、実質的に認証をバイパスできてしまうことが判明しました。別のケースでは、チェックの欠落により、サーバーがエンドレスなメッセージのストリームを処理できてしまい、リソースを枯渇させる可能性があることが分かりました。これらの発見は、ソフトウェアを分析する現在の手法における決定的なギャップを浮き彫りにしています。つまり、入力と出力を見るだけでは、プログラムが真にどのように機能するかを理解するには不十分だということです。研究者たちは、精密なコード分析と人工知能の推論能力を組み合わせることで、プログラムの内部ロジックの完全かつ正確なモデルを構築できることを証明しました。このアプローチは、ソフトウェアを修正する必要もなく、また研究者がコードの全行を手動で追跡する必要もありません。そのため、私たちのデジタルインフラを保護している複雑なシステムを監査するための、拡張性のある方法となります。
この研究はまた、テキストの類似性に基づいてコードを検索するという、従来のアプローチの限界にも対処しました。それらの手法は、プログラムの状態を変化させるために連携して働く異なる関数同士のつながりを結びつけることができなかったため、失敗することがよくありました。対照的に、この新システムは、データの流れと制御の流れを実際に追跡するため、人工知能に提供されるコンテキストが完全かつ連結されたものになります。これにより、システムは汎用的なテンプレートを適用して的外れな結果を出すのではなく、それぞれのユニークな実装の変数とロジックに特化したセキュリティチェックを生成することができました。その結果、異なるコーディングスタイルの癖に適応しながら、システムの挙動に関する信頼できるモデルを生成できるフレームワークが得られました。
結局のところ、この研究はソフトウェアセキュリティへのアプローチにおけるパラダイムシフトを象徴しています。それは、すべてのコード行を手動で検査するか、表面的なことしか見ることができないブラックボックス・テストに頼るかという二択から脱却するものです。代わりに、機械の内部を見通し、それがどのように考え、反応するかを正確に理解する方法を提示しています。研究者たちは、コードを「スライス（切り出し）」、分析し、検証可能な一連の論理的ステップとして扱うことで、長年隠れていたエラーを見つけ出せることを明らかにしました。このツールはオープンソースプロジェクトに対してテストされましたが、この手法は、インターネットを支える膨大な数のプロプライエタリな（独占的な）システムを保護するための道筋を示唆しています。複雑なプロトコルのステートマシンを自動的に抽出し、検証する能力は、セキュリティをかつてないほど徹底的かつ迅速にチェックすることを可能にし、数十年にわたってデジタル世界を悩ませてきた種類の侵害を未然に防ぐ可能性を秘めています。今回の知見は、プロトコルが「すべきこと」と、それが「実際にしていること」の間のギャップにこそ危険が潜んでおり、そのギャップを埋めるには、コードそのものをより深く、より精密に見つめる必要があることを裏付けています。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。