AI 中文总结
针对 P4 报文解析器，提出 Octopus 工具将其转成自动机并符号化检查等价性，可在消费级硬件上数分钟内完成非平凡解析器的等价性检查，还评估了其网络场景可用性。
AI 中文摘要
P4 是一种用于编程协议无关报文处理器的领域特定语言，其中报文解析器描述如何将输入比特流构造成首部和字段。基于 Doenges 等人（2022）的工作，我们提出 Octopus 工具，它将 P4 报文解析器转换为自动机，随后尝试（符号化地）检查它们的等价性。Octopus 会生成证据，要么是证明等价性的互模拟，要么是见证两个解析器之间行为差异的反例比特流。与早期工作不同，我们的工具能在消费级硬件上于数分钟内检查非平凡解析器之间的等价性。我们报告该工具的实现，并评估其在网络场景中的可用性。
英文摘要
P4 is a domain-specific language for programming protocol-independent packet processors, where packet parsers describe how incoming bit-streams are structured into headers and fields. Building on work by Doenges et al. (2022), we present Octopus, a tool that translates P4 packet parsers into automata and then attempts to (symbolically) check their equivalence. Octopus produces evidence, either in the form of a bisimulation demonstrating equivalence, or a counterexample bit-stream witnessing a behavioral difference between the two parsers. In contrast with earlier work, our tool can check equivalence between non-trivial parsers within minutes, on consumer hardware. We report on the tool's implementation and evaluate its usability in networking contexts.
Journal refIn proceedings of CAV 2026 (1), pp 198-211
DOI：10.1007/978-3-032-32519-8_11
