Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust

Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust

Speakers: Yi Cai, Second Year PhD Student, University of Maryland

Conference: USENIX Security

YouTube: https://www.youtube.com/watch?v=78Y-KJIpOPA

Overview

Binary formats are the backbone of modern computing, underpinning everything from common document types like PDF and ZIP to executable formats like Linux ELF and WebAssembly, and critically, security-sensitive protocols such as cryptographic handshakes, X.509 certificates, and VPN configurations. Interacting with these diverse formats necessitates the use of parsers and serializers. A serializer translates high-level data structures within an application into a sequence of bytes for external communication or storage, while a parser performs the inverse operation, converting external byte sequences back into structured data for the application. This talk introduces Vest, a novel framework designed to generate verified, secure, and high-performance parsers and serializers specifically for the Rust programming language.

The development of Vest directly addresses a long-standing challenge in software engineering: the inherent tension between achieving high performance and ensuring robust security in binary data processing. Historically, optimizing parsers for speed often involves intricate low-level manipulations that can inadvertently introduce subtle bugs or deviations from format specifications, leading to severe security vulnerabilities. Vest aims to resolve this dilemma by providing a system that not only generates highly optimized, zero-copy parsers and in-place serializers but also formally proves their correctness and security properties, making them resilient against various parsing attacks.

Presented by Yi Cai, a second-year PhD student at the University of Maryland, Vest represents a collaborative effort with researchers from Carnegie Mellon University, Microsoft Research, and Northeastern University. By leveraging Rust's inherent memory safety guarantees alongside the power of formal verification tools like Verus, Vest empowers developers to build critical parsing infrastructure with unprecedented levels of assurance. It democratizes access to formal methods, allowing regular programmers to specify complex binary formats using a high-level description language and automatically obtain mechanically verified, production-ready code.

Background

▶ Watch: Introduction and the challenge of secure parsing (0:00)

The pervasive nature of binary formats means that nearly every application interacts with them at its boundaries. The integrity and security of these interactions are paramount, yet secure parsing and input validation remain exceptionally difficult tasks. Indeed, input validation errors are consistently ranked among the top five most dangerous software errors, highlighting their critical impact on system security. The primary reason for this difficulty stems from the conflicting objectives developers face: the desire for maximum performance often clashes with the meticulous attention to detail required for security. Aggressive optimizations, while improving speed, can easily cause an implementation to diverge from the complex formal specifications of a binary format, opening doors for attackers.

A significant class of vulnerabilities arises when parsers and their corresponding serializers are not perfect inverses of each other. This mismatch can lead to parsing ambiguities or malleability, where a single high-level data structure can be encoded into multiple valid byte sequences, or conversely, where a single byte sequence can be interpreted in multiple ways by different parsers or even by the same parser under different conditions. The talk specifically references an award-winning paper presented at the same USENIX Security conference, which identified and exploited numerous novel attacks based on such "dubious parser implementations." These findings underscore the urgent need for robust solutions that can guarantee the precise and unambiguous handling of binary data.

Traditional approaches to parsing often involve manual implementation in low-level languages, or the use of parser generators that prioritize speed over formal correctness. While these tools can deliver high performance, they typically offer no formal guarantees regarding memory safety, soundness, completeness, or critical security properties like non-malleability and non-ambiguity. This leaves a significant gap, as security-critical applications dealing with sensitive data (e.g., cryptographic protocols, financial transactions) require absolute assurance that their parsers correctly interpret and validate all inputs without introducing exploitable flaws. Vest enters this landscape to bridge this gap, offering a verified approach to secure and performant parsing in Rust.

Key Findings

▶ Watch: Developer workflow and Vest's code generation process (4:05)

Vest's core contribution is its ability to generate verified, secure, high-performance parsers and serializers for Rust from a high-level format description language. This innovative approach provides a robust solution to the long-standing trade-off between performance and security in binary data processing. The framework is designed to deliver several key assurances and capabilities:

1. High Performance Implementations: Vest generates zero-copy parsers and in-place serializers. This means that data is processed directly in memory buffers without unnecessary copying or allocations, which is crucial for achieving high throughput and minimizing latency, making Vest-generated code competitive with hand-optimized, unverified solutions.

1. Comprehensive Security Guarantees: Beyond mere memory safety (which Rust's type system largely provides "for free"), Vest formally proves a suite of critical security properties for its generated parsers and serializers:

• Soundness: The parser will only accept valid inputs that conform to the format specification.
• Completeness: The parser will correctly interpret all valid inputs according to the specification.
• Non-Malleability: A valid high-level data representation cannot be transformed into a different byte sequence that still parses back to the same high-level representation. This prevents attackers from subtly altering data without changing its semantic meaning, which can bypass integrity checks.
• Non-Ambiguity: Any given byte sequence will parse to at most one high-level data structure. This eliminates the risk of different interpretations of the same data, a common source of parsing vulnerabilities.

1. Formal Verification with Verus: Vest leverages Verus, a state-of-the-art program verifier for Rust. Verus is instrumental in mechanically proving the soundness, completeness, non-malleability, and non-ambiguity properties of the generated code. This mechanical verification provides a level of assurance that is unattainable through traditional testing alone.

1. Accessibility for Regular Programmers: A significant achievement of Vest is its usability. Programmers do not need expertise in formal methods to benefit from Vest. They can define binary formats using a high-level, domain-specific language (DSL) within a Vest file. The Vest DSL compiler then automatically generates the Rust code, complete with its formal proofs and performant implementations.

1. Proven Impact and Adoption: Vest has already been integrated into several notable projects, demonstrating its practical utility in real-world, security-critical contexts. These include the Owl compiler, which uses Vest to generate constant-time parsers for cryptographic protocols, and the Verdict project, which employs Vest to build formally verified X.509 certificate parsers. Both of these applications were also presented at USENIX Security, underscoring Vest's immediate relevance and contribution to the security community.

These findings collectively position Vest as a groundbreaking tool for developing secure and efficient binary format processing components, setting a new standard for assurance in an area traditionally fraught with vulnerabilities.

Technical Deep Dive

▶ Watch: Vest-Li combinator library and example format specification (5:51)

The technical architecture of Vest is centered around a sophisticated workflow that transforms high-level format specifications into mechanically verified, high-performance Rust code. This process relies heavily on a specialized combinator library and Rust's powerful trait system, all orchestrated with the Verus verifier.

The typical workflow for a programmer using Vest begins by consulting external format specifications (e.g., RFCs, standards documents). These specifications are then translated into a Vest file, which serves as the core input to the system. This Vest file employs a high-level, domain-specific language (DSL) to precisely define the structure, constraints, and dependencies inherent in the binary format. For instance, it specifies data types, field ordering, conditional parsing logic, and length-dependent structures.

Once the Vest file is created, the programmer invokes the Vest DSL compiler. This compiler is the engine that translates the abstract format description into a concrete Rust module. The generated Rust module is comprehensive, containing several key components:

1. Rust Data Types: These are the high-level data structures that represent the parsed binary format within the Rust application.
2. Parser and Serializer Specifications: These are the formal mathematical models of how the parser and serializer should behave according to the Vest file's definition.
3. Security Proofs: Crucially, the module includes the formal proofs for the security properties (soundness, completeness, non-malleability, non-ambiguity) derived directly from the format specification.
4. Performance Implementations: These are the actual Rust functions for zero-copy parsing and in-place serialization, highly optimized for speed.

This entire generation process heavily relies on vest-li, a formally verified Rust library developed by the Vest team. vest-li is a combinator library that underpins the high proof automation, fast verification, and efficient performance implementations. After the Rust module is generated, it undergoes mechanical verification by Verus. This step ensures that the generated performance implementations precisely conform to their mathematical specifications and satisfy all the declared security properties. Upon successful verification, programmers can confidently integrate this Vest-generated module into larger Rust projects, whether those projects are themselves verified or not.

The vest-li library is central to Vest's design, offering a collection of combinators that allow for the compositional specification of binary formats. It includes:

• 10 primitive combinators: These handle fundamental data types like various integer sizes (e.g., u8, u16, u32) and byte arrays.
• 9 higher-order combinators: These enable the construction of more complex structures through operations like sequential composition (e.g., A followed by B), choices (e.g., A or B based on a condition), and repetition (e.g., an array of N elements). Each of these combinators is meticulously designed and proven to uphold non-malleability and non-ambiguity properties. Furthermore, they are carefully crafted to avoid unnecessary memory copies or allocations, contributing to Vest's high-performance characteristics.

To illustrate, consider a classical binary format using the TLV (Tag-Length-Value) scheme. A message might be structured with a tag (identifying the data type), a link (specifying the length of the value), and the value itself. Critically, the interpretation and content of the value field might depend on both the tag and link fields. In Vest, this can be expressed compositionally. One might compose a nested pair of integers for the tag and link, and then, based on their parsed values, conditionally interpret the subsequent bytes as message_one or message_two, each consuming exactly lin (length) number of bytes. For any object defined this way in Rust, Vest automatically provides spec_parsers and spec_serializers methods, yielding a formal mathematical model of the parser and serializer. Remarkably, the same Vest combinator specification used to define the format also automatically derives the formal proofs of security and correctness, alongside the verified, performant implementation.

The elegance of Vest's design is deeply rooted in its clever leverage of Rust's trait system. At a high level, there's a SpecCombinator trait that defines the mathematical structure of a format, along with its straightforward functional parser and serializer specifications. At a lower level, the Combinator trait defines the efficient data types and the zero-copy parser and in-place serializer implementations. Verus is then used to formally verify that the performant Combinator implementation precisely obeys the mathematical SpecCombinator specification. Additionally, Vest uses Rust's trait bounds to enforce that every combinator adheres to a SecureCombinator trait, which in turn proves the advanced security properties (non-malleability, non-ambiguity) of the specification combinators. This layered approach ensures that a single combinator definition encapsulates the format's mathematical structure, its parser and serializer behavior, the correctness and security proofs, and the high-performance implementations. A key optimization for verification speed is the strategic use of higher-order functions, which helps avoid the need for complex quantifiers in most proofs, making the verification process significantly faster.

Future developments for Vest include extending support for recursive formats, enhancing precision for large numbers (big-preciseness), and handling pointer-rich hierarchical formats. These advancements will involve adding features such as parsing actions, error recovery mechanisms, and support for non-linearity during parsing.

Demo / Proof of Concept

▶ Watch: Deep dive: Rust traits for verification and performance (8:00)

To demonstrate its capabilities and practical effectiveness, Vest was applied to generate parsers and serializers for several prominent and complex binary formats, serving as rigorous case studies. These included:

1. Bitcoin Block Format: A critical structure in the Bitcoin blockchain, involving intricate cryptographic hashes, transaction lists, and variable-length fields.
2. TLS 1.3 Handshake Format: A highly security-sensitive protocol for establishing secure communication channels, characterized by complex state machines and cryptographic negotiations.
3. WebAssembly (Wasm) Binary Format: A low-level binary instruction format designed for high-performance execution in web browsers and other environments, known for its compact and efficient structure.

For each of these formats, Vest automatically generated the corresponding Rust parsers and serializers, complete with their formal proofs. The performance of this generated code was then rigorously compared against unverified, hand-optimized industrial baselines:

• For Bitcoin, Vest's generated parser was benchmarked against rust-bitcoin.
• For TLS 1.3, it was compared with rust-tls.
• For WebAssembly, the benchmark used was the cranelift-wasm parser.

The results were compelling: Vest's generated code exhibited execution performance that was "on par or better" than these highly optimized, yet unverified, industrial implementations. This crucial finding validates Vest's claim of delivering high performance without compromising security, directly addressing the traditional trade-off.

Beyond execution performance, the talk also presented a comparison of verification time. Vest's verification process was benchmarked against error-parse, another automated parsing and serialization tool that is verified in Coq. A log-scale chart clearly illustrated that Vest was "orders of magnitude faster" in terms of verification time compared to error-parse. This significant speed advantage is attributed to two primary factors:

1. Verus: The underlying verifier, Verus, was specifically designed with verification performance in mind.
2. Vest's Trait-Based Design: The elegant trait-based architecture of vest-li and the strategic avoidance of quantifiers in many proofs greatly contribute to the efficiency of the verification process.

These case studies and performance comparisons provide strong evidence that Vest is not merely a theoretical construct but a practical, high-impact tool capable of delivering formally verified, high-performance parsing solutions for real-world, security-critical applications.

Defensive Implications

▶ Watch: Performance benchmarks against unverified industrial baselines (10:00)

The advent of tools like Vest has profound implications for how defenders approach the security of systems that process binary data. The insights from this talk suggest several critical shifts in defensive strategies:

• Prioritize Formally Verified Components: For any security-critical application dealing with binary formats (e.g., network protocols, cryptographic systems, file parsers in privileged contexts), defenders should actively seek and adopt formally verified parsing and serialization tools. Relying solely on extensive testing or unverified, hand-optimized code is insufficient given the proven prevalence and impact of parsing vulnerabilities. Vest provides a practical pathway to achieve this high level of assurance in Rust.

• Demand Non-Malleability and Non-Ambiguity: These advanced security properties should become standard requirements for all new parser and serializer development. Understanding that a seemingly valid input can be subtly altered without changing its high-level meaning (malleability) or that a single byte sequence can have multiple valid interpretations (ambiguity) is crucial. Defenders should push for tools and methodologies that explicitly guarantee these properties, as Vest does.

• Leverage Rust's Safety Features with Formal Methods: Rust's strong type system and ownership model provide robust memory safety guarantees, significantly reducing a class of common vulnerabilities. When combined with formal verification tools like Verus and frameworks like Vest, Rust becomes an exceptionally powerful language for building highly secure and resilient systems, particularly for low-level components like parsers.

• Educate on Parsing Ambiguities: The research highlighted in the background section on "parsing ambiguities" underscores a sophisticated attack vector. Defenders, especially those involved in protocol design and implementation review, should be aware of these types of vulnerabilities and understand how they can be exploited. Vest offers a systematic way to prevent these at the design and implementation stage.

• Embrace High-Level Specification Languages: The use of domain-specific languages (DSLs) for format specification, as employed by Vest, allows security properties and correctness to be defined and verified at a higher level of abstraction. This reduces the cognitive load and potential for error compared to manually implementing complex parsing logic in low-level code. Defenders should advocate for such approaches to improve the overall security posture of their software supply chain.

By integrating Vest's principles and tools, organizations can significantly enhance the security of their applications against parsing-related attacks, moving towards a proactive and formally assured defense posture.

Key Takeaways

• Vest is a novel generator for Rust that produces verified, secure, and high-performance parsers and serializers for binary formats.
• It guarantees critical properties including memory safety, soundness, completeness, non-malleability, and non-ambiguity, which are crucial for preventing parsing attacks.
• The framework leverages Rust's powerful trait system and the Verus program verifier to achieve efficient and automated formal verification.
• Vest-generated code demonstrates performance on par with or better than unverified, hand-optimized industrial baselines, effectively resolving the traditional performance-security trade-off.
• Its verification process is orders of magnitude faster than other formal methods tools, making formal verification practical for complex binary formats.
• Vest empowers regular developers, even without formal methods expertise, to build highly assured and secure parsing components from high-level format specifications.

About the Speaker(s)

Yi Cai is a second-year PhD student at the University of Maryland. His research interests lie in the intersection of systems, security, and formal methods, specifically focusing on developing verified, secure, and high-performance solutions for challenging problems such as parsing and serialization in Rust. He is a key contributor to the Vest project, which aims to enhance the security and reliability of software interacting with binary data formats.