From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
本論文は、SpecMonランタイムモニターを用いて、WhatsApp WebおよびSignal Desktopの観測された実行が新たに開発されたTamarin互換モデルに適合していることを検証することにより、形式的なプロトコル仕様と実世界の実際の実装との間の溝を埋め、それによってセキュリティ特性を裏付けるとともに、アプリケーション間の文書化されていない相違を明らかにしている。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
デジタル時代において、数十億の人々が最もプライベートな思考を共有し、金融データを保護し、日常生活を調整するために、メッセージングアプリに依存しています。これらのアプリケーションの舞台裏には、「プロトコル」として知られる複雑な一連のルールが存在しており、それがメッセージをどのようにロックし、送信し、解除するかという設計図としての役割を果たしています。これらの設計図の中で最も有名なのが「Signalプロトコル」です。これは、たとえハッカーがメッセージを傍受したとしても、内容を読み取ることができないように設計されたシステムです。長年、セキュリティの専門家たちは強力なコンピュータツールを用いて、この設計図が数学的に健全であることを証明してきました。彼らは、もしルールが完璧に従われるならば、このシステムは破ることのできないものであることを示してきました。しかし、設計図は建物そのものではありません。紙の上で完璧に見える設計であっても、建設作業員がすべての指示に従ったか、適切な材料を使用したか、あるいは壁を築く際に偶発的なミスを避けたかどうかは別問題です。ソフトウェアの世界では、理論的な設計と、ユーザーのスマートフォン上で実際に動作しているコードとの間の「隙間」に、脆弱性が隠れていることがよくあります。
CISPAヘルムホルツ情報セキュリティ研究センターの研究チームは、この隙間を埋めることに着手しました。彼らは、Signalプロトコルの実世界のバージョン（WhatsAppやSignalアプリ内で実行されているもの）が、設計された厳格なルールを実際に遵守しているのかを知りたいと考えました。これらの大規模なアプリケーションのコードベース全体を読み解こうとする代わりに（一部が隠されていたり、非公開であったりするため、それは困難な作業です）、研究者たちは特化した「監視役（ウォッチドッグ）」を構築しました。SpecMonと呼ばれるこの監視役は、アプリケーションが実行されている間、その動きを見守り、ネットワークとのあらゆる会話や、セキュリティキーを用いたあらゆる計算を傍受します。そして、これらのライブな動作を、完璧な理論モデルとリアルタイムで比較します。もしアプリケーションが近道を取ろうとしたり、ステップを飛ばしたり、あるいは設計図が許可しているものとは異なる方法を使用しようとしたりすれば、監視役はアラームを鳴らします。
研究者たちはこの手法を、誰でも検査可能なSignal Desktopと、巨大企業が所有する閉鎖的でプロプライエタリなシステムであるWhatsApp Webという、2つの主要なアプリケーションに適用しました。Signal Desktopアプリケーションに対しては、既存の非常に詳細なプロトコルの数学的モデルから出発し、そこに将来の量子コンピュータに耐えられるよう設計された新しいタイプの暗号化の扱い方など、実際のソフトウェアに見られる具体的で複雑な詳細を加えました。一方、WhatsAppについては、逆算して作業を行う必要がありました。事前のモデルがない状態から出発し、アプリケーションの挙動を観察してその動作を記録し、ソフトウェアが行っていることと正確に一致する新しいカスタム設計図をゼロから構築しました。これは、WhatsApp版のプロトコルの実装から直接、形式的なモデルが導き出された初めての事例であり、大きな成果となりました。
これらのモデルの準備が整うと、研究者たちはそれらをテストにかけました。メッセージが遅延したり、順序が入れ替わって送られたり、あるいはネットワーク接続が中断されたりするシナリオを含む、数千回のシミュレーション会話を実行しました。あらゆるケースにおいて、アプリケーションはモデルが予測した通りに動作し、コアとなるセキュリティメカニズムが正しく機能していることが確認されました。また、研究者たちは、監視役がそれらを検知できるかどうかを確認するために、意図的にソフトウェアにエラーを注入しました。アプリに古い暗号化キーを再利用させたり、署名のチェックをスキップさせたり、あるいは予期せぬ方法で秘密のデータを漏洩させたりしました。システムはこれらすべてのセキュリティ上の欠陥を検知し、監視ツールがルールの逸脱を察知するのに十分な感度を持っていることを証明しました。
しかし、このモニタリングは、すぐには判明しない、2つのアプリケーション間の微妙な違いをも明らかにしました。研究者たちは、WhatsAppが「既読通知（メッセージが閲覧されたことを送信者に知らせる通知）」の扱いを、Signalとは異なって行っていることを発見しました。Signalでは、これらの通知はメッセージ自体と同じ強力な暗号化の中に包み込まれており、セキュリティキーの継続的な更新に参加しています。一方、WhatsAppでは、これらの通知は暗号化レイヤーの外側で送信されており、そのためセキュリティの更新をトリガーしません。研究者たちは、この違いに基づいてWhatsAppのセキュリティを打破する方法は見つけませんでしたが、これは、もし秘密のキーが盗まれた場合に、アプリケーションがセキュリティを回復するのに時間がかかる可能性があることを意味すると指摘しました。また、WhatsAppには、Signalアプリに備わっている「サーバーから送信者の身元を隠す」といった高度なプライバシー機能がまだ含まれていないことも確認されました。
この研究は、すべてのソースコードを見る必要がなくとも、複雑な実世界のソフトウェアが動作している様子を観察し、それがセキュリティの約束を遵守しているかどうかを検証することが可能であることを示しています。プロセスは効率的で、セットアップと実行にわずか数週間しかかからず、アプリケーションの速度への遅延もほとんどありませんでした。理論的モデルとライブモニタリングが同じ言語を共有するシステムを構築することで、研究者たちは、開発者やセキュリティ専門家が、アプリケーションの進化に合わせてそれらが安全であり続けているかを継続的にチェックする方法を提供しました。このアプローチは、私たちが日常的に使用しているデジタルツールに対する信頼を築くための新しい道を提示しており、私たちが住む建物が、その設計図と同じくらい安全であることを保証するものなのです。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。