Fri 17 Jun 2022 16:10 - 16:30 at Kon-Tiki - Verification II Chair(s): Thomas Wahl
Sat 18 Jun 2022 04:10 - 04:30 at Kon-Tiki - Verification II

We present Leapfrog, a Coq-based framework for verifying the equivalence of network protocol parsers. Our approach is based on an automata model of P4 parsers, and an algorithm for symbolically computing bisimulations modulo ``leaps'' that greatly simplifies the symbolic representation. Proofs are powered by a Coq plugin that uses an off-the-shelf SMT solver to decide the validity of first-order entailments, resulting in a fully automatic, push-button tool for verifying equivalence. We mechanically prove the core metatheory that underpins our approach, including the key transformations, along with 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.

Fri 17 Jun

Displayed time zone: Pacific Time (US & Canada) change

15:30 - 16:50
Verification IIPLDI at Kon-Tiki +12h
Chair(s): Thomas Wahl GrammaTech, Inc.
15:30
20m
Talk
Relational Compilation for Performance-Critical Applications
PLDI
Clément Pit-Claudel EPFL, AWS, Jade Philipoom MIT CSAIL, Dustin Jamner MIT CSAIL, Andres Erbsen MIT CSAIL, Adam Chlipala MIT CSAIL
Link to publication DOI Pre-print
15:50
20m
Talk
Formally Verified Lifting of C-compiled x86-64 Binaries
PLDI
Freek Verbeek Open University of The Netherlands & Virginia Tech, Joshua A. Bockenek Virginia Tech, Zhoulai Fu University of California, Davis, Binoy Ravindran Virginia Tech
DOI
16:10
20m
Talk
Leapfrog: Certified Equivalence for Protocol Parsers
PLDI
Ryan Doenges Cornell University, Tobias Kappé ILLC, University of Amsterdam, John Sarracino Cornell University, Nate Foster Cornell University, Greg Morrisett Cornell Tech
DOI Pre-print
16:30
20m
Talk
Computing Correctly with Inductive Relations
PLDI
Zoe Paraskevopoulou Northeastern University, Aaron Eline University of Maryland, Leonidas Lampropoulos University of Maryland
DOI

Sat 18 Jun

Displayed time zone: Pacific Time (US & Canada) change

03:30 - 04:50
Verification IIPLDI at Kon-Tiki
03:30
20m
Talk
Relational Compilation for Performance-Critical Applications
PLDI
Clément Pit-Claudel EPFL, AWS, Jade Philipoom MIT CSAIL, Dustin Jamner MIT CSAIL, Andres Erbsen MIT CSAIL, Adam Chlipala MIT CSAIL
Link to publication DOI Pre-print
03:50
20m
Talk
Formally Verified Lifting of C-compiled x86-64 Binaries
PLDI
Freek Verbeek Open University of The Netherlands & Virginia Tech, Joshua A. Bockenek Virginia Tech, Zhoulai Fu University of California, Davis, Binoy Ravindran Virginia Tech
DOI
04:10
20m
Talk
Leapfrog: Certified Equivalence for Protocol Parsers
PLDI
Ryan Doenges Cornell University, Tobias Kappé ILLC, University of Amsterdam, John Sarracino Cornell University, Nate Foster Cornell University, Greg Morrisett Cornell Tech
DOI Pre-print
04:30
20m
Talk
Computing Correctly with Inductive Relations
PLDI
Zoe Paraskevopoulou Northeastern University, Aaron Eline University of Maryland, Leonidas Lampropoulos University of Maryland
DOI