Leapfrog: certified equivalence for protocol parsers
Leapfrog: certified equivalence for protocol parsers
复制标题
DOI：
10.1145/3519939.3523715
复制
发表时间：
2022-05
期刊：
影响因子：
--
通讯作者：
Ryan Doenges;Tobias Kapp'e;J. Sarracino;Nate Foster;Greg Morrisett
中科院分区：
文献类型：
--
作者：
Ryan Doenges;Tobias Kapp'e;J. Sarracino;Nate Foster;Greg Morrisett
我们提出了Leapfrog，一个基于Coq的用于验证网络协议解析器等价性的框架。我们的方法基于P4解析器的自动机模型，以及一种使用“跳跃”来符号化计算双模拟的紧凑表示的算法。证明由一个经过认证的编译链提供支持，该编译链从一阶蕴含式到低级位向量验证条件，这些条件使用现成的SMT求解器来处理。因此，Leapfrog中的解析器等价性证明是完全自动且一键式的。我们机械地证明了支撑我们方法的核心元理论，包括关键的转换和若干优化。我们在一系列实际案例研究中对Leapfrog进行了评估，所有这些案例研究都只需要极少的配置且无需手动证明。我们最大的案例研究使用Leapfrog为一个从自动机到硬件流水线的第三方编译器执行翻译验证。总体而言，Leapfrog代表着朝着一个所有关键网络基础设施的解析器都经过验证的世界迈出了一步。它还为后续工作提出了方向，例如验证涉及安全性的关系属性。
We present Leapfrog, a Coq-based framework for verifying equivalence of network protocol parsers. Our approach is based on an automata model of P4 parsers, and an algorithm for symbolically computing a compact representation of a bisimulation, using "leaps." Proofs are powered by a certified compilation chain from first-order entailments to low-level bitvector verification conditions, which are discharged using off-the-shelf SMT solvers. As a result, parser equivalence proofs in Leapfrog are fully automatic and push-button. We mechanically prove the core metatheory that underpins our approach, including the key transformations and several optimizations. We evaluate Leapfrog on a range of practical case studies, all of which require minimal configuration and no manual proof. Our largest case study uses Leapfrog to perform translation validation for a third-party compiler from automata to hardware pipelines. Overall, Leapfrog represents a step towards a world where all parsers for critical network infrastructure are verified. It also suggests directions for follow-on efforts, such as verifying relational properties involving security.