BPF and formal verification

CRANK

I spent the spring of 2015 researching the Berkeley packet filter (BPF) and its formal verification with my programming languages professor, Joe Gibbs Politz. The project took some unexpected turns and we learned a lot about Coq and applied formal verification in the process.Other than a little experience with the proof assistant Isabelle, this was my first foray into formal verification. If you consider yourself a Coq guru, this reflection might seem facile. If you’re interested in formal verification or are starting your first real-world Coq project, though, I think you’ll find it worthwhile.The main goal of our work was to create a translation validator for BPF programs. This idea was based on the Jitk project from MIT.A translation validator proves some definition of correctness for an individual BPF program. This distinction is critical to understand when validating programs or compilers. Formally verifying a compiler proves that all outputs of that compiler are correct. Transl…