Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust
summary
Vest generates Rust zero-copy parsers and in-place serializers from an RFC-like DSL, proves memory safety plus soundness, completeness, non-malleability and non-ambiguity, and for the first time claims resistance to basic digital side-channel attacks. It implements a verified combinator library (10 primitive, 9 higher-order combinators), uses the Varys verifier, and automatically produces code for Bitcoin blocks, TLS 1.3 handshakes and WebAssembly. Performance matches or beats hand-written parsers and verification is orders of magnitude faster.
AI-written summary · about
chapters (9)
- 0:00Vest introduction
- 1:15Parsing and serialization importance
- 2:18Parser security challenges
- 3:01Vest secure approach
- 4:05Programmer interaction with Vest
- 6:31Vest combinators and formats
- 8:21Rust traits for Vest
- 9:45Case studies and benchmarks
- 11:32Future development and conclusion
related talks
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
19mA Hybrid Approach to Semi-automated Rust Verification
18mVerus: Verifying Rust Programs using Linear Ghost Types
09mFormally Secure Hardware with Rust
20mRust for Safer Protocol Development
15mModular Specification and Verification of Closures in Rust
30mA RustFest Carol
20mVerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…)