Automated Formal Verification of Software Network Functions

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiability at the expense of other goals such as run-time performance. Exhaustive symbolic execution (ESE), a technique that automatically explores all paths in a piece of code, is a promising direction for automating formal verification. However, ESE faces the path explosion problem: a large number of different program paths with equivalent behavior prevent ESE from completing in reasonable time, since ESE enumerates each path individually.

This thesis addresses some of the challenges ESE currently faces, in the context of software network functions (NFs). These are real-world programs that the Internet relies on and are amenable to verification, because they are typically self-contained and have a clear specification.

In the first part of this thesis, we propose abstractions that enable ESE to analyze more code in reasonable time. We propose ghost maps to abstract over complex data structure code by executing equivalent simpler code written in terms of maps. We also propose imperative loop summaries to abstract over loops by executing equivalent loop-free code also written in terms of maps. Instead of exploring a large number of equivalent paths, an ESE engine can use our techniques to explore only paths that have different high-level behavior. As a result, our techniques can automatically verify the correctness of a set of NFs using only hand-written contracts for data structures, as opposed to the step-by-step proof annotations necessary in previous work.

In the second part of this thesis, we propose abstractions that make code amenable to ESE while also improving performance and safety. We present a new network card driver template specifically designed for NFs. Drivers following this template are not only easier to automatically verify, as they don't use complex data structures, but also provide better performance for the NFs that can use them compared to more general drivers. We additionally show that drivers written in safe languages can reach the same performance as their unsafe counterparts, as long as safe languages expose to developers a handful of specific type invariants that enable compilers to automatically prove the safety of potentially unsafe operations and thus avoid emitting run-time checks.