~/talk

Leapfrog: Certified Equivalence for Protocol Parsers

on YouTube 17m
Talkat PLDI 2022 · 2022-06-13..06-17· [security, networking]

speakers

name:Boyi Xie
links:none on file
name:Rafael Rojas
links:none on file
name:Toby Murray
links:none on file

resources

video:https://youtu.be/Qnd_VjMCAwk
slides:none on file

summary

Leapfrog proves that a high-level P4 parser and its optimized target automaton recognize the same packet language by modeling parsers as finite automata, using a symbolic bisimulation with a weakest-precondition transformer and a new bypass optimization called bisimulation up to closure (leaps) to skip long buffering steps. Implementation is mechanized in Coq and uses the mirrorSolve SAT/SMT plugin. The tool translation-validates ParserGen outputs and emits Coq proof certificates for the examples attempted.

AI-written summary · about

chapters (11)

  1. 0:00Intro
  2. 0:11Parsing Matters for Security
  3. 0:59Programmable Parsing
  4. 2:00Parsing MPLS with a P4 Automaton
  5. 3:06Loop Unrolling Optimization
  6. 3:54Leapfrog Contributions
  7. 5:25Automata Semantics: Configurations
  8. 7:05Language Equivalence
  9. 7:58Concrete Algorithm
  10. 9:51Symbolic Algorithm
  11. 12:21Implementation

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.