Leapfrog: Certified Equivalence for Protocol Parsers

TL;DR

Leapfrog is a Coq-based framework that automatically verifies the equivalence of network protocol parsers using automata models, symbolic bisimulation, and certified proofs, enhancing parser reliability in critical infrastructure.

Contribution

It introduces a fully automatic, certified method for proving parser equivalence based on automata and bisimulation, with a formal proof chain and practical case studies.

Findings

Successfully verified parser equivalence in multiple case studies

Automated proofs require minimal configuration and no manual intervention

Demonstrated translation validation for hardware pipeline compilation

Abstract

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.