Hardening Attack Surfaces with Formally Proven Binary Format Parsers
summary
A toolchain converts a descriptive 3D format into F proofs and then to C, yielding memory- and integer-safe parsers with functional correctness and double-fetch freedom. Applied to Hyper-V vSwitch, a 5000-line spec verifies in 82 seconds and emits 23,000 C lines with zero user proof effort; generated validators pass performance regressions with under 2% cycles/byte* overhead, are live in Windows/Azure, and eliminate many legacy parsing bugs.
AI-written summary · about
chapters (5)
- 0:00Start
- 4:043D: A source language of message formats for Dependent Data Descriptions
- 6:13This paper: Verified Secure Parsers for Microsoft Hyper-V Network Virtualization
- 7:24Hyper-V vSwitch: network packet layers
- 9:21Performance
related talks
08mEverparse: A Verifying Compiler from Data Format Specifications to Verified Efficient Parsers
29mVale: Verifying High-Performance Cryptographic Assembly Code
21mDaedalus: Safer Document Parsing
48mThe Proof Must Go On: Formal Methods in the Theater of Secure Software Development(…)
34mFormally verified hardening of C programs against hardware fault injection
12mAutomated Synthesis of Verified Firewalls
42mBuilding Hardened IoT Implementations With LangSec
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice