Automated Verification of Network Function Binaries

Explore an automated technique for verifying network function binaries in this NSDI '22 conference talk. Delve into the challenges of bridging abstraction levels between implementations and specifications without relying on specific data structures. Learn about the innovative use of "ghost maps" to model data structures and specify network functions. Discover how Klint, a new verification tool, can analyze network function binaries without source code or debug symbols, enabling operators to verify proprietary code. Examine the process of inferring control flow and types through NF-environment interactions, and understand how this approach allows for verification of entire NF binary stacks down to the NIC driver level. Gain insights into the performance and practical applications of this verification technique across multiple network function binaries.

Intro
Context
Network Functions
Hard part
Requirements
Translation
Source code
Exhaustive symbolic execution
Binaries
Klint
Outline
Verification performance
Summary