Automated Verification of Network Function Binaries
Talkat 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22) · 2022-04-04..04-06·
summary
Claims an automated verifier, Klint, proves properties of real NF binaries (no source or debug info) by modeling arbitrary data structures as a universal ghost map abstraction, inferring invariants across maps from observed interactions, and using symbolic execution of the binary to enumerate paths. Implementation verifies seven network functions (six C, one Rust) in minutes, checks memory safety and functional specs, and finds counterexamples when paths violate contracts.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:25Context
- 1:03Network Functions
- 1:30Hard part
- 2:38Requirements
- 6:15Translation
- 8:31Source code
- 9:06Exhaustive symbolic execution
- 9:36Binaries
- 10:42Klint
- 11:52Outline
- 12:11Verification performance
- 14:40Summary
related talks
46mVerifying code using automated reasoning
12mAutomated Synthesis of Verified Firewalls- 12mAutomated Synthesis of Verified Firewalls
15mThey're the same picture: a software-verification flow adapted for hardware verification
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
32mVerifying Constant-Time Implementations
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
07mV for Verification