論文の概要: From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
- arxiv url: http://arxiv.org/abs/2609.11882v2
- Date: Sat, 12 Sep 2026 16:14:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-16 07:15:04.988893
- Title: From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
- Title（参考訳）: スペックからアプリへ:SignalとWhatsAppのモデルの検証とモニタリング
- Abstract要約: 我々はWhatsApp WebによるSignalプロトコルの実装のモデルを開発する。
Signalプロトコルの中核となるコンポーネントについては、認証と機密性を検証する。
監視によって、元のlibsignalライブラリとWhatsAppのフォークの間に、これまで文書化されていなかった違いが明らかになった。
- 参考スコア（独自算出の注目度）: 8.86750495352076
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The Signal protocol is a prominent messaging protocol that secures communication for billions of users. It powers WhatsApp, the most widely used messaging application worldwide, and the Signal app, popular among privacy-conscious users. Extensive research in the computational and Dolev-Yao settings provides strong formal security guarantees for the protocol itself. However, a gap remains between the guarantees of the protocol specification and the implementation's actual behavior at runtime. In this work, we bridge this gap by applying SpecMon, a recently proposed runtime monitor, to check whether observed executions conform to formal protocol models. To this end, we instrument two applications (WhatsApp Web and Signal Desktop) to capture their interactions with the network and the cryptographic components. Using this instrumentation, we develop two multiset-rewrite models that are compatible with Tamarin, thus enabling verification. We derive the first model of WhatsApp Web's implementation of the Signal protocol and the most detailed model to date of Signal's original protocol. Monitoring establishes that observed executions conform to these models, relative to the trusted event extraction and the symbolic abstraction. For the core components of the Signal protocol, we verify authentication and secrecy properties. Finally, monitoring reveals previously undocumented differences between the original libsignal library and WhatsApp's fork. We evaluate our methodology and demonstrate its reproducibility. Developing the WhatsApp Web model, instrumenting the app, adding fuzzing, and running the experiments took three person-weeks. We also demonstrate efficient monitoring of real-world applications and detection of deliberately injected security faults, with low overhead in our measured setting.
- Abstract（参考訳）: Signalプロトコルは、数十億のユーザのための通信をセキュアにするための、卓越したメッセージングプロトコルである。
それは世界でもっとも広く使われているメッセージングアプリWhatsAppと、プライバシーを意識したユーザーの間で人気があるSignalアプリを動かしている。
計算とDolev-Yao設定に関する広範な研究は、プロトコル自体に対して強力な正式なセキュリティ保証を提供する。
しかしながら、プロトコル仕様の保証と実行時の実装の実際の動作との間には、ギャップが残っている。
本研究では、最近提案されたランタイムモニタであるSpecMonを用いて、観測された実行が正式なプロトコルモデルに準拠しているかどうかを確認する。
この目的のために、ネットワークと暗号化コンポーネントとのインタラクションをキャプチャする2つのアプリケーション(WhatsApp WebとSignal Desktop)を実装します。
この装置を用いて,タマリンと互換性のある2つのマルチセット書き換えモデルを構築し,検証を可能にする。
我々はWhatsApp WebによるSignalプロトコルの実装の最初のモデルと、Signalのオリジナルプロトコルの最も詳細なモデルを導出する。
監視は、観測された実行が信頼されたイベント抽出と象徴的な抽象化に対して、これらのモデルに適合していることを確立する。
Signalプロトコルの中核となるコンポーネントについては、認証と機密性を検証する。
最後に、監視によって、元のlibsignalライブラリとWhatsAppのフォークの間に、これまで文書化されていなかった違いが明らかになる。
我々は方法論を評価し、再現性を実証する。
WhatsApp Webモデルの開発、アプリのインスツルメンテーション、ファジングの追加、実験の実行には3週間を要した。
また、実世界のアプリケーションの効率的なモニタリングや、故意に注入されたセキュリティ障害の検出も、測定した設定のオーバーヘッドを低くして実施する。
関連論文リスト
- PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
我々は、スケジューリング、検証、メモリ、ベンチマーク、安全性をシステムレベルのサービスとして提供するPhyAgentOSを紹介します。
セッション中心のセッションは、スケジューリング、互換性、監督された実行、エビデンス収集、受け入れの最小単位として、アクションではなくセッションを扱う。
SessionVerifierは、実行終了とセマンティックタスク完了を、成功、失敗、または再計画のエビデンスに基づいて判断する。
ベンチマークはデプロイメントセッションと検証パスを再利用するので、結果は実際の実行に遡る。
論文 参考訳（メタデータ） (2026-07-18T04:46:53Z) - AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation [0.0]
本稿では,プロトコル実装のためのドメイン固有言語を用いて,トレース特性の検証を行う新しい言語ファースト手法を提案する。
検証のためのタマリン証明器を目標とし、検証された普遍的トレース特性が実装に戻すことを証明する。
我々は、署名されたDiffie-HellmanプロトコルとWireGuard VPNプロトコルの正確なモデルの実装と生成にツールを使用します。
論文 参考訳（メタデータ） (2026-06-18T08:34:17Z) - A Technical Taxonomy of LLM Agent Communication Protocols [60.76747983053368]
本研究では,大規模言語モデル(LLM)エージェント通信プロトコルの分類と解析を行う技術的分類法を開発する。
このフレームワークはプロトコルの選択をガイドし、プライバシーやポリシー執行といったオープンな研究ギャップを強調する。
論文 参考訳（メタデータ） (2026-06-17T14:45:20Z) - Autogenesis: A Self-Evolving Agent Protocol [60.15939127351914]
本稿では,自己進化プロトコルであるAutogenesis Protocol(AGP)を紹介する。
本稿では,実行中のプロトコル登録リソースを動的にインスタンス化し,検索し,精錬する自己進化型マルチエージェントシステムAGSを提案する。
論文 参考訳（メタデータ） (2026-04-16T14:04:06Z) - Automated Side-Channel Analysis of Cryptographic Protocol Implementations [9.38081874899831]
WhatsAppの最初の形式モデルを実装から抽出する。
コンパイル後セキュリティに対する既知のクローンアタックを特定します。
本稿では,暗号プロトコルの実装をサイドチャネル攻撃に対するレジリエンスとして解析する手法を提案する。
論文 参考訳（メタデータ） (2025-11-14T15:13:49Z) - Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
プロトコルとモニタモデルを知っている信頼できないモデルによるアダプティブアタックについて検討する。
我々は、攻撃者がモデル出力に公知またはゼロショットプロンプトインジェクションを埋め込む単純な適応攻撃ベクトルをインスタンス化する。
論文 参考訳（メタデータ） (2025-10-10T15:12:44Z) - LLM-Assisted Model-Based Fuzzing of Protocol Implementations [9.512044399020514]
プロトコル動作の障害は脆弱性やシステム障害につながる可能性がある。
プロトコルテストに対する一般的なアプローチは、プロトコルの状態遷移と期待される振る舞いをキャプチャするマルコフモデルを構築することである。
本稿では,大規模言語モデル(LLM)を利用して,ネットワークプロトコルの実装をテストするためのシーケンスを自動的に生成する手法を提案する。
論文 参考訳（メタデータ） (2025-08-03T13:16:18Z) - What If We Had Used a Different App? Reliable Counterfactual KPI Analysis in Wireless Systems [52.499838151272016]
本稿では、RANによって異なるアプリが実装された場合のトラフィックの値を推定する問題に対処する。
本稿では,無線システムに対する共形予測に基づく対実解析手法を提案する。
論文 参考訳（メタデータ） (2024-09-30T18:47:26Z) - SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols [5.202524136984542]
我々は、アプリケーションがイベントストリームを取得するのに使用するネットワークと暗号化ライブラリを実装します。
次に、これらの観測結果を仕様モデルで有効なトレースにマッチングするために、効率的なアルゴリズムを使用します。
論文 参考訳（メタデータ） (2024-09-04T17:54:29Z) - Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
SCIONルータは、敵の環境でセキュアなパケット転送のための暗号化プロトコルを実行する。
プロトコルのネットワーク全体のセキュリティ特性と,その実装の低レベル特性の両方を検証する。
本稿では,本研究のアプローチを説明し,主な成果を要約し,検証可能なシステムの設計と実装に関する教訓を抽出する。
論文 参考訳（メタデータ） (2024-05-09T19:57:59Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。
本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。
実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
論文 参考訳（メタデータ） (2024-01-19T14:52:04Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。