論文の概要: Validating Network Protocol Parsers with Traceable RFC Document Interpretation
- arxiv url: http://arxiv.org/abs/2504.18050v1
- Date: Fri, 25 Apr 2025 03:39:19 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-05-02 19:15:53.633122
- Title: Validating Network Protocol Parsers with Traceable RFC Document Interpretation
- Title（参考訳）: トレース可能なRFC文書解釈によるネットワークプロトコルパーサの検証
- Authors: Mingwei Zheng, Danning Xie, Qingkai Shi, Chengpeng Wang, Xiangyu Zhang,
- Abstract要約: オラクルとトレーサビリティの問題は、プロトコルの実装がいつバグがあると考えられるかを決定する。
この研究はどちらも考慮し、大規模言語モデル(LLM)の最近の進歩を利用した効果的なソリューションを提供する。
我々は、C、Python、Goで書かれた9つのネットワークプロトコルとその実装を使用して、我々のアプローチを広く評価してきた。
- 参考スコア（独自算出の注目度）: 11.081773172066766
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Validating the correctness of network protocol implementations is highly challenging due to the oracle and traceability problems. The former determines when a protocol implementation can be considered buggy, especially when the bugs do not cause any observable symptoms. The latter allows developers to understand how an implementation violates the protocol specification, thereby facilitating bug fixes. Unlike existing works that rarely take both problems into account, this work considers both and provides an effective solution using recent advances in large language models (LLMs). Our key observation is that network protocols are often released with structured specification documents, a.k.a. RFC documents, which can be systematically translated to formal protocol message specifications via LLMs. Such specifications, which may contain errors due to the hallucination of LLMs, are used as a quasi-oracle to validate protocol parsers, while the validation results in return gradually refine the oracle. Since the oracle is derived from the document, any bugs we find in a protocol implementation can be traced back to the document, thus addressing the traceability problem. We have extensively evaluated our approach using nine network protocols and their implementations written in C, Python, and Go. The results show that our approach outperforms the state-of-the-art and has detected 69 bugs, with 36 confirmed. The project also demonstrates the potential for fully automating software validation based on natural language specifications, a process previously considered predominantly manual due to the need to understand specification documents and derive expected outputs for test inputs.
- Abstract（参考訳）: ネットワークプロトコルの実装の正しさを検証することは、オラクルとトレーサビリティの問題のために非常に難しい。
前者は、特にバグが観察可能な症状を起こさない場合、プロトコルの実装がバグと見なせるかどうかを判断する。
後者は、実装がどのようにプロトコル仕様に違反しているのかを開発者が理解できるようにし、バグ修正を容易にする。
両方の問題を考慮に入れない既存の作業とは異なり、この作業はどちらも考慮し、最近の大規模言語モデル(LLM)の進歩を利用して効果的なソリューションを提供する。
我々のキーとなる観察は、ネットワークプロトコルは、しばしば構造化された仕様文書(RFC文書)でリリースされ、LCMを通して形式化されたプロトコルメッセージ仕様に体系的に変換できるということです。
LLMの幻覚によるエラーを含む可能性のあるそのような仕様は、プロトコルパーサを検証するための準オークルとして使用され、検証結果は徐々にオラクルを洗練させる。
オラクルはドキュメントから派生しているので、プロトコル実装で見つかったバグはすべてドキュメントに遡ることができるので、トレーサビリティの問題に対処できます。
我々は、C、Python、Goで書かれた9つのネットワークプロトコルとその実装を使用して、我々のアプローチを広く評価してきた。
その結果,本手法は最先端に優れ,69例のバグが検出され,36例が確認された。
このプロジェクトはまた、自然言語仕様に基づいてソフトウェア検証を完全に自動化する可能性も示している。これは、以前は手動で検討されていたプロセスであり、仕様文書を理解し、テストインプットに対して期待された出力を導出する必要がある。
関連論文リスト
- FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols [2.242458166492809]
オンチップ通信プロトコルの正式な仕様は、システムオンチップ(SoC)の設計と検証に不可欠である。
非公式な文書から正式なプロトコル仕様を構築するための2段階のフレームワークであるFLAGを提案する。
論文 参考訳（メタデータ） (2025-04-24T03:34:37Z) - Large Language Models for Validating Network Protocol Parsers [8.007994733372675]
プロトコル標準は一般的に自然言語で書かれるが、実装はソースコードで書かれている。
大規模言語モデル(LLM)に基づくフレームワークであるPARVALを提案する。
プロトコル標準とそれらの実装の両方を、フォーマット仕様と呼ばれる統一された中間表現に変換する。
実装とRFC標準の矛盾をうまく識別し、偽陽性率は5.6%と低い。
論文 参考訳（メタデータ） (2025-04-18T07:09:56Z) - Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
SCIONルータは、敵の環境でセキュアなパケット転送のための暗号化プロトコルを実行する。
プロトコルのネットワーク全体のセキュリティ特性と,その実装の低レベル特性の両方を検証する。
本稿では,本研究のアプローチを説明し,主な成果を要約し,検証可能なシステムの設計と実装に関する教訓を抽出する。
論文 参考訳（メタデータ） (2024-05-09T19:57:59Z) - DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
プロパティベースのテストはセキュアプロトコルのセキュリティバグの検出に有効である。
セキュアマルチパーティ計算(MPC)を特に対象とする。
MPCプロトコルのビットレベル実装において,様々な欠陥を検出するテストを作成する。
論文 参考訳（メタデータ） (2024-03-08T02:02:24Z) - GenAudit: Fixing Factual Errors in Language Model Outputs with Evidence [64.95492752484171]
GenAudit - 文書基底タスクの事実チェック LLM 応答を支援するためのツール。
GenAuditは、レファレンス文書でサポートされていないクレームを修正したり削除したりすることでLCMレスポンスを編集することを提案し、また、サポートしているように見える事実の参照から証拠を提示する。
GenAuditは、さまざまなドメインから文書を要約する際に、8つの異なるLCM出力でエラーを検出することができる。
論文 参考訳（メタデータ） (2024-02-19T21:45:55Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。
本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。
実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
論文 参考訳（メタデータ） (2024-01-19T14:52:04Z) - Understanding and Mitigating Classification Errors Through Interpretable
Token Patterns [58.91023283103762]
容易に解釈可能な用語でエラーを特徴付けることは、分類器が体系的なエラーを起こす傾向にあるかどうかを洞察する。
正しい予測と誤予測を区別するトークンのパターンを発見することを提案する。
提案手法であるPremiseが実際によく動作することを示す。
論文 参考訳（メタデータ） (2023-11-18T00:24:26Z) - Knowledge-Augmented Language Model Verification [68.6099592486075]
最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。
本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。
その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
論文 参考訳（メタデータ） (2023-10-19T15:40:00Z) - Bicoptor 2.0: Addressing Challenges in Probabilistic Truncation for Enhanced Privacy-Preserving Machine Learning [6.733212399517445]
本稿では,既存のPPML作業における確率的トランケーションプロトコルの問題の解析と解決策の提案に焦点をあてる。
精度の面では、既存の作品のいくつかで推奨される精度の選択が誤りであることを明らかにする。
本稿では,今後の課題に対する解法と精度選択ガイドラインを提案する。
論文 参考訳（メタデータ） (2023-09-10T01:43:40Z) - Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。
まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。
我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
論文 参考訳（メタデータ） (2023-05-22T06:11:15Z) - Data post-processing for the one-way heterodyne protocol under
composable finite-size security [62.997667081978825]
本研究では,実用的連続可変(CV)量子鍵分布プロトコルの性能について検討する。
ヘテロダイン検出を用いたガウス変調コヒーレント状態プロトコルを高信号対雑音比で検討する。
これにより、プロトコルの実践的な実装の性能を調べ、上記のステップに関連付けられたパラメータを最適化することができる。
論文 参考訳（メタデータ） (2022-05-20T12:37:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。