Validating Network Protocol Parsers with Traceable RFC Document Interpretation

• URL: http://arxiv.org/abs/2504.18050v1
• Date: Fri, 25 Apr 2025 03:39:19 GMT
• Title: Validating Network Protocol Parsers with Traceable RFC Document Interpretation
• Authors: Mingwei Zheng, Danning Xie, Qingkai Shi, Chengpeng Wang, Xiangyu Zhang,
• Abstract summary: oracle and traceability problems determine when a protocol implementation can be considered buggy.<n>This work considers both and provides an effective solution using recent advances in large language models (LLMs)<n>We have extensively evaluated our approach using nine network protocols and their implementations written in C, Python, and Go.
• Score: 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.

Related papers

• FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols [2.242458166492809]
  Formal specifications of on-chip communication protocols are crucial for system-on-chip (SoC) design and verification.<n>We propose FLAG, a two-stage framework to help construct formal protocol specifications from informal documents.
  arXiv  Detail & Related papers  (2025-04-24T03:34:37Z)
• Large Language Models for Validating Network Protocol Parsers [8.007994733372675]
  Protocol standards are typically written in natural language, whereas implementations are in source code.<n>We propose PARVAL, a framework built on large language models (LLMs)<n>It transforms both protocol standards and their implementations into a unified intermediate representation, referred to as format specifications.<n>It successfully identifies inconsistencies between the implementation and its RFC standard, achieving a low false positive rate of 5.6%.
  arXiv  Detail & Related papers  (2025-04-18T07:09:56Z)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems.
  arXiv  Detail & Related papers  (2024-05-09T19:57:59Z)
• DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
  Property-based testing is effective for detecting security bugs in secure protocols. We specifically target Secure Multi-Party Computation (MPC) We devise a test that can detect various flaws in a bit-level implementation of an MPC protocol.
  arXiv  Detail & Related papers  (2024-03-08T02:02:24Z)
• GenAudit: Fixing Factual Errors in Language Model Outputs with Evidence [64.95492752484171]
  We present GenAudit -- a tool intended to assist fact-checking LLM responses for document-grounded tasks.<n>GenAudit suggests edits to the LLM response by revising or removing claims that are not supported by the reference document, and also presents evidence from the reference for facts that do appear to have support.<n> Comprehensive evaluation by human raters shows that GenAudit can detect errors in 8 different LLM outputs when summarizing documents from diverse domains.
  arXiv  Detail & Related papers  (2024-02-19T21:45:55Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• Understanding and Mitigating Classification Errors Through Interpretable Token Patterns [58.91023283103762]
  Characterizing errors in easily interpretable terms gives insight into whether a classifier is prone to making systematic errors. We propose to discover those patterns of tokens that distinguish correct and erroneous predictions. We show that our method, Premise, performs well in practice.
  arXiv  Detail & Related papers  (2023-11-18T00:24:26Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  Recent Language Models (LMs) have shown impressive capabilities in generating texts with the knowledge internalized in parameters. We propose to verify the output and the knowledge of the knowledge-augmented LMs with a separate verifier. Our results show that the proposed verifier effectively identifies retrieval and generation errors, allowing LMs to provide more factually correct outputs.
  arXiv  Detail & Related papers  (2023-10-19T15:40:00Z)
• Bicoptor 2.0: Addressing Challenges in Probabilistic Truncation for Enhanced Privacy-Preserving Machine Learning [6.733212399517445]
  This paper focuses on analyzing the problems and proposing solutions for the probabilistic truncation protocol in existing PPML works. In terms of accuracy, we reveal that precision selections recommended in some of the existing works are incorrect. We propose a solution and a precision selection guideline for future works.
  arXiv  Detail & Related papers  (2023-09-10T01:43:40Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC) is a novel fact-checking model that decomposes complex claims into simpler sub-tasks. We first leverage the in-context learning ability of large language models to generate reasoning programs. We execute the program by delegating each sub-task to the corresponding sub-task handler.
  arXiv  Detail & Related papers  (2023-05-22T06:11:15Z)
• Data post-processing for the one-way heterodyne protocol under composable finite-size security [62.997667081978825]
  We study the performance of a practical continuous-variable (CV) quantum key distribution protocol. We focus on the Gaussian-modulated coherent-state protocol with heterodyne detection in a high signal-to-noise ratio regime. This allows us to study the performance for practical implementations of the protocol and optimize the parameters connected to the steps above.
  arXiv  Detail & Related papers  (2022-05-20T12:37:09Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.