論文の概要: Verification and Attack Synthesis for Network Protocols
- arxiv url: http://arxiv.org/abs/2511.01124v1
- Date: Mon, 03 Nov 2025 00:26:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-05 16:37:27.072059
- Title: Verification and Attack Synthesis for Network Protocols
- Title（参考訳）: ネットワークプロトコルの検証と攻撃合成
- Authors: Max von Hippel,
- Abstract要約: ネットワークプロトコルは、事前に定義された通信パターンに従う入力と出力を持つプログラムである。
この論文は,攻撃対象のネットワークプロトコルの機能と性能を,攻撃対象のネットワークプロトコルの機能と性能を効果的に特徴付けることができることを示している。
- 参考スコア（独自算出の注目度）: 3.8022378790092026
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Network protocols are programs with inputs and outputs that follow predefined communication patterns to synchronize and exchange information. There are many protocols and each serves a different purpose, e.g., routing, transport, secure communication, etc. The functional and performance requirements for a protocol can be expressed using a formal specification, such as, a set of logical predicates over its traces. A protocol could be prevented from achieving its requirements due to a bug in its design or implementation, a component failure (e.g., a crash), or an attack. This dissertation shows that formal methods can feasibly characterize the functionality and performance of network protocols under normal conditions as well as when subjected to attacks.
- Abstract（参考訳）: ネットワークプロトコルは、事前定義された通信パターンに従って情報を同期し交換する入力と出力を持つプログラムである。
多くのプロトコルがあり、それぞれが異なる目的(例えば、ルーティング、トランスポート、セキュアな通信など)を果たす。
プロトコルの機能的および性能的要件は、そのトレース上の論理述語のセットなど、正式な仕様を使って表現することができる。
プロトコルは、その設計や実装のバグ、コンポーネントの障害(例えば、クラッシュ)、あるいはアタックによって、その要件を達成するのを防げる。
この論文は,攻撃対象のネットワークプロトコルの機能と性能を,攻撃対象のネットワークプロトコルの機能と性能を効果的に特徴付けることができることを示している。
関連論文リスト
- Protocol Testing with I/O Grammars [45.68497486907946]
本稿では,単一フレームワークにおける入力生成と出力チェックを組み合わせた新しいプロトコルテスト手法を提案する。
我々は、I/O文法が、テスト中のプログラムの出力検証を可能にするとともに、高度なプロトコルの特徴を正しく、完全に指定できることを実証する。
論文 参考訳（メタデータ） (2025-09-24T16:41:04Z) - LLM-Assisted Model-Based Fuzzing of Protocol Implementations [9.512044399020514]
プロトコル動作の障害は脆弱性やシステム障害につながる可能性がある。
プロトコルテストに対する一般的なアプローチは、プロトコルの状態遷移と期待される振る舞いをキャプチャするマルコフモデルを構築することである。
本稿では,大規模言語モデル(LLM)を利用して,ネットワークプロトコルの実装をテストするためのシーケンスを自動的に生成する手法を提案する。
論文 参考訳（メタデータ） (2025-08-03T13:16:18Z) - ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols [45.66401695351214]
本稿では,広く使用されているSystemVerilogプロトコルを対象とした最初のベンチマークスイートであるProtocolLLMを紹介する。
我々は,ほとんどのモデルがタイミング制約に従う通信プロトコルのSystemVerilogコードを生成するのに失敗したことを観察する。
論文 参考訳（メタデータ） (2025-06-09T17:10:47Z) - Validating Network Protocol Parsers with Traceable RFC Document Interpretation [11.081773172066766]
オラクルとトレーサビリティの問題は、プロトコルの実装がいつバグがあると考えられるかを決定する。
この研究はどちらも考慮し、大規模言語モデル(LLM)の最近の進歩を利用した効果的なソリューションを提供する。
我々は、C、Python、Goで書かれた9つのネットワークプロトコルとその実装を使用して、我々のアプローチを広く評価してきた。
論文 参考訳（メタデータ） (2025-04-25T03:39:19Z) - Games for AI Control: Models of Safety Evaluations of AI Deployment Protocols [52.40622903199512]
本稿では,多目的かつ部分的に観察可能なゲームとして,AI-Control Gamesを紹介した。
我々は、信頼できない言語モデルをプログラミングアシスタントとしてデプロイするためのプロトコルをモデル化、評価、合成するために、フォーマリズムを適用した。
論文 参考訳（メタデータ） (2024-09-12T12:30:07Z) - 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) - Ejafa_protocol: A custom INC secure protocol [0.0]
このプロトコルには、鍵交換用のX25519や暗号化用のChaCha20など、現代の暗号プリミティブが含まれている。
プロトコルの重要な特徴は、セキュリティを犠牲にすることなく、リソース制限された環境への適応性である。
論文 参考訳（メタデータ） (2024-01-05T12:51:19Z) - Towards Semantic Communication Protocols: A Probabilistic Logic
Perspective [69.68769942563812]
我々は,NPMを確率論理型言語ProbLogで記述された解釈可能なシンボルグラフに変換することによって構築された意味プロトコルモデル(SPM)を提案する。
その解釈性とメモリ効率を利用して、衝突回避のためのSPM再構成などのいくつかの応用を実演する。
論文 参考訳（メタデータ） (2022-07-08T14:19:36Z) - Automated Attack Synthesis by Extracting Finite State Machines from
Protocol Specification Documents [25.871916915930996]
RFC文書から有限状態マシン(FSM)を抽出するためのデータ駆動型アプローチを提案する。
市販のNLPツールとは異なり、RFC文書からFSMを抽出するためのデータ駆動型アプローチを提案する。
BGPv4, DCCP, RFCを用いたFSM抽出の一般化可能性を示す。
SCTPとTCP。
論文 参考訳（メタデータ） (2022-02-18T23:27:29Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。