論文の概要: Automated Channel Fault Analysis with Tofu

• arxiv url: http://arxiv.org/abs/2605.01721v1
• Date: Sun, 03 May 2026 05:27:25 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-05 20:33:49.904122
• Title: Automated Channel Fault Analysis with Tofu
• Title（参考訳）: 豆腐を用いた流路障害の自動解析
• Authors: Jacob Ginesin, Max von Hippel, Cristina Nita-Rotaru,
• Abstract要約: 本研究では,分散プロトコル上でチャネル障害解析を自動的に行うための厳密な手法を開発した。 Tofuは、任意の線形時間論理(LTL)プロトコル仕様に基づいて、音質、完全解析、チャネル障害に基づく攻撃トレースの合成を提供する。 TCP 研究に利用することで,豆腐の適用性を実証する。
• 参考スコア（独自算出の注目度）: 10.517508846742682
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Distributed protocols are the linchpin of the modern internet, underpinning every internet service. This has in turn motivated a massive body of research ensuring the security, reliability, and performance of distributed protocols. In these works, a wide-ranging assumption is that distributed protocols operate over faulty or attacker-controlled channels, where messages can be arbitrarily inserted, dropped, replayed, or reordered. Formal verification work targeting distributed protocols typically defines its own notion of faulty or malicious channels, then constructively proves their protocol is correct with respect to it. In this work we take a fundamentally different approach: we develop a rigorous methodology for automatically conducting channel fault analysis on distributed protocols, and we introduce Tofu, a generalizable tool that implements our methodology. Tofu provides sound, complete analysis, synthesizing channel fault-based attack traces on arbitrary linear temporal logic (LTL) protocol specifications or proving the absence of such through an exhaustive state-space search. We demonstrate the applicability of Tofu by employing it to study TCP.
• Abstract（参考訳）: 分散プロトコルは現代のインターネットの根幹であり、すべてのインターネットサービスを支える。 これにより、分散プロトコルのセキュリティ、信頼性、パフォーマンスを保証する大規模な研究の動機となった。 これらの作業では、分散プロトコルが障害やアタッカーが制御するチャネル上で動作し、メッセージは任意に挿入、ドロップ、リプレイ、リオーダーされる。 分散プロトコルをターゲットとする形式的検証作業は、一般的に、障害や悪意のあるチャネルという独自の概念を定義し、そのプロトコルがそれに関して正しいことを建設的に証明する。 本研究では,分散プロトコル上でチャネル障害を自動的に解析する厳密な方法論を開発し,その方法論を実装した一般化可能なツールであるTofuを紹介する。 Tofuは、音質、完全解析、任意の線形時間論理(LTL)プロトコル仕様に基づくチャネル障害ベースの攻撃トレースの合成、あるいは、徹底的な状態空間探索によってそれらが存在しないことを証明する。 TCP 研究に利用することで,豆腐の適用性を実証する。

関連論文リスト

• Conformal Prediction for Multi-Source Detection on a Network [59.17729745907474]
  マルチソース検出問題について検討する。 グラフ上のノード感染状況のスナップショットが与えられた場合、伝播を開始するソースノードのセットを推定する。 本稿では,ソースセット検出のための統計的に有効なリコール保証を提供する新しいコンフォメーション予測フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-11-12T01:09:56Z)
• Uncovering Gaps Between RFC Updates and TCP/IP Implementations: LLM-Facilitated Differential Checks on Intermediate Representations [21.889716987837428]
  プロトコルスタックコードの実装とRFC標準の間にはしばしば矛盾があります。 この矛盾はプロトコル機能の違いを引き起こすだけでなく、深刻なセキュリティ上の脆弱性を引き起こす可能性がある。 大規模言語モデルの台頭により、RFC文書からプロトコル仕様を抽出する方法が研究され始めている。
  論文  参考訳（メタデータ） (2025-10-28T13:19:46Z)
• Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
  プロトコルとモニタモデルを知っている信頼できないモデルによるアダプティブアタックについて検討する。 我々は、攻撃者がモデル出力に公知またはゼロショットプロンプトインジェクションを埋め込む単純な適応攻撃ベクトルをインスタンス化する。
  論文  参考訳（メタデータ） (2025-10-10T15:12:44Z)
• Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version) [1.5997757408973357]
  音響アニメーションを生成するIsabelle形式を用いたNeedham-Schroederプロトコルをモデル化する。 以上の結果から,すべてのシナリオにおいて信頼性が保たれていることが示唆された。 我々は、透かしとジャミングを統合したPLSベースのDiffie-Hellmanプロトコルを提案している。
  論文  参考訳（メタデータ） (2025-08-26T20:59:16Z)
• LLM-Assisted Model-Based Fuzzing of Protocol Implementations [9.512044399020514]
  プロトコル動作の障害は脆弱性やシステム障害につながる可能性がある。 プロトコルテストに対する一般的なアプローチは、プロトコルの状態遷移と期待される振る舞いをキャプチャするマルコフモデルを構築することである。 本稿では,大規模言語モデル(LLM)を利用して,ネットワークプロトコルの実装をテストするためのシーケンスを自動的に生成する手法を提案する。
  論文  参考訳（メタデータ） (2025-08-03T13:16:18Z)
• Universal quantum computation via scalable measurement-free error correction [45.29832252085144]
  本研究では,中間回路計測を行なわずに誤り訂正を行うシナリオにおいて,普遍的な量子計算をフォールトトレラントにすることができることを示す。 論理的な$mathitCCZ$ゲートを実現するため,Bacon-Shor符号の無測定変形プロトコルを導入する。 特に,回路レベルのエラーレートが10～3ドル以下であれば,破れない論理性能が達成可能であることを示す。
  論文  参考訳（メタデータ） (2024-12-19T18:55:44Z)
• Lazy Layers to Make Fine-Tuned Diffusion Models More Traceable [70.77600345240867]
  新たな任意の任意配置(AIAO)戦略は、微調整による除去に耐性を持たせる。 拡散モデルの入力/出力空間のバックドアを設計する既存の手法とは異なり,本手法では,サンプルサブパスの特徴空間にバックドアを埋め込む方法を提案する。 MS-COCO,AFHQ,LSUN,CUB-200,DreamBoothの各データセットに関する実証研究により,AIAOの堅牢性が確認された。
  論文  参考訳（メタデータ） (2024-05-01T12:03:39Z)
• Robustness of implemented device-independent protocols against constrained leakage [0.0]
  デバイス非依存(DI)プロトコルは近年大きな進歩を遂げている。 これらのデモのセキュリティ証明は、DI暗号の典型的な前提に依存しており、デバイスは互いに望ましくない情報を漏らさないし、敵にも漏らさない。
  論文  参考訳（メタデータ） (2023-02-27T16:28:23Z)
• Round-robin differential phase-time-shifting protocol for quantum key distribution: theory and experiment [58.03659958248968]
  量子鍵分布(QKD)は、遠隔者間で共通の暗号鍵の確立を可能にする。 近年,信号の乱れの監視を回避できるQKDプロトコルが提案され,初期の実験で実証されている。 我々は,ラウンドロビン差動位相シフトプロトコルのセキュリティ証明を,集団攻撃シナリオにおいて導出する。 その結果,RRDPTSプロトコルは高い量子ビット誤り率の条件下で,RDPSと比較して高い秘密鍵レートが得られることがわかった。
  論文  参考訳（メタデータ） (2021-03-15T15:20:09Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。