EverParse: Hardening critical attack surfaces with formally proven message parsers

EverParse is a framework for generating provably secure parsers and formatters used to improve the security of critical code bases at Microsoft. EverParse is developed as part of Project Everest, a collaboration between Microsoft Research labs in Redmond, Washington; India; and Cambridge, United Kingdom; the Microsoft Research-Inria Joint Centre; Inria; Carnegie Mellon University; and several other open-source contributors. The Everest team has produced several formally proven software components, including the EverCrypt cryptographic provider and verified implementations of the TLS 1.3 record layer, the QUIC record layer, the Signal messaging protocol, and the DICE measured boot protocol. This is the fourth blog post in a series about Project Everest.

• Project Everest Blog Posts
  • “Project Everest: Reaching greater heights in internet communication security” (opens in new tab) 
  • “EverCrypt cryptographic provider offers developers greater security assurances” (opens in new tab) 
  • “Project Everest: Advancing the science of program proof” (opens in new tab) 

Software security exploits often begin with an attacker providing an unexpected input to a program, confusing the program and causing it to misbehave in a way that allows the attacker to gain access to a critical system, leading to crashes and service disruption, information disclosure, or even granting the attacker full control of the system.

Most programs are designed to validate their inputs before further processing to avoid such scenarios, but input validation is hard to get right, particularly as both the message formats and the validation code are often optimized for performance. Improper input validation is the third most “common and impactful” vulnerability, according to MITRE’s 2020 CWE Top 25 Most Dangerous Software Weaknesses list (opens in new tab), with input validation bugs lurking at all levels of the software stack. Modern software is built on a tower of abstractions, spanning several trust boundaries. Each time more privileged code receives inputs from less privileged layers, a missing input validation check can cause the tower of abstractions to collapse. Input validation—and, more generally, parsing—is especially difficult when input formats are complex, such as when dealing with variable length data and other forms of data dependency. For efficiency reasons, formats can be densely encoded in binary and are expected to be parsed by low-level code in systems programming languages like C or C++, which are hard to use securely. A single missing check can lead to a buffer overrun and system compromise.

One fruitful and widely adopted line of research is to discover flaws in parsers using fuzzing, a technique to automatically generate tests for programs. Fuzzing is indeed an effective strategy for identifying broad classes of vulnerabilities, but it’s challenging to obtain strong guarantees of correctness or security from fuzzing (though not impossible as some research from Microsoft Research shows). For the most critical systems, we advocate instead automatically generating input parsers and validators from high-level declarative specifications of binary message formats. Importantly, using the program proof methodology and toolchain of Project Everest, we can produce efficient C code backed by mathematical proofs of correctness and security.

In a 2019 paper (opens in new tab), we introduced EverParse (opens in new tab), a framework that automatically produces high-performance, formally proven C code for parsing binary messages. EverParse is now being used to ensure that certain network virtualization components in the Windows kernel correctly parse attacker-controlled inputs. Put another way, network packets are handled first by EverParse code that is proven to correctly parse and accept only well-formed messages, rejecting potentially malicious inputs before they reach the rest of the system. Virtualized networking hardened with EverParse is available today for use via the Windows Insider Program (opens in new tab). Future versions of Windows Server will contain the same hardening, improving the security of virtual machines and containers on Microsoft Azure. 

EverParse: A mathematically proven parser generator

With EverParse, programmers no longer need to write error-prone binary message parsers. Instead, from a declarative message format, EverParse generates code in the F* programming language together with automatically checkable formal proofs that the code is memory safe and correct—for example, that it doesn’t read outside the bounds of arrays and that it successfully parses exactly those messages that are formatted according to the input message specification. Once F* checks these proofs, it emits secure, high-performance C code for the generated parsers, as described in this paper about verified low-level programming in F*. What’s left is for programmers to focus on architecting their software to interpose EverParse’s formally proven parsing code prior to their main application-specific processing.

The code sample above shows a simple example of an EverParse specification. The example highlights EverParse’s support for variable-length, data-dependent message formats; EverParse uses a syntax that augments C’s syntax of type definitions with various kinds of semantic constraints (highlighted in blue). The variable-length Messages structure pairs a size field, constrained to be at most 1024, with an array of messages whose size in bytes is exactly size. The Message structure itself pairs a tag with a message field, a data-dependent union, or a casetype, whose case is determined by the tag.

From this specification, EverParse produces a formally proven C procedure to check that an untrusted input contains correctly formatted messages—its signature in C is simply BOOLEAN CheckMessages(uint8_t *bytes, uint32_t len). That is, given bytes a pointer to an array of at least len bytes, CheckMessages decides whether those bytes correctly represent a Messages array. A proof in F* ensures that CheckMessages is correct, returning true whenever bytes contains a valid Messages and false otherwise, while reading each byte in the bytes array at most once and not modifying any existing memory or performing any heap allocation.

What remains is to insert a call to CheckMessages in a program just as soon as untrusted input is received, using it to filter out only all ill-formed messages. In addition to simply validating untrusted input, EverParse also offers several other constructs to safely read relevant parts of the input for further application-specific processing and to report parsing errors. The parsers produced by EverParse can be used within a larger F* project, enabling proofs of correctness and security of complete software components. For example, we use EverParse in our verified implementations of the TLS 1.3 record layer, the QUIC record layer, and the DICE measured boot protocol, which are programmed and verified in F*. However, the C code produced from EverParse can also be directly integrated within an existing C or C++ project, hardening the attack surface of a critical piece of software by ensuring that messages are validated and parsed properly, as we describe next.

EverParse in network virtualization

We now turn to the use of EverParse in the Windows kernel to secure the virtual networking stack, specifically its use in Hyper-V Virtual Switch (opens in new tab). Virtual Switch provides virtualized access to the network to virtual machines (VM). Virtual Switch runs in the privileged root partition (opens in new tab) of Hyper-V and dispatches network packets to and from the VM guest and hardware network interface card. Efficient and secure handling of these network packets is key to the proper functioning of several critical systems, including Microsoft Azure.

Together with the Network Virtualization team, we’ve specified the format of more than a hundred different kinds of messages spanning four different protocol layers handled by Virtual Switch. EverParse produces about 30,000 lines of verified C code for validating and parsing those messages. While describing those message formats in EverParse requires careful specification engineering and discovery (some of these protocols involve proprietary formats with a long history of evolution), the generated C code can be deployed with confidence in its correctness and security. In the particular context of Virtual Switch, in addition to memory safety and correctness, EverParse proves the code free from double fetches (opens in new tab), protecting it from time-of-check/time-of-use bugs.

Of course, Virtual Switch is also a performance-critical component. A major concern was whether adding additional input validation checks would significantly reduce its performance. As such, we spent a substantial amount of effort in ensuring the code produced by EverParse is fast. By design, EverParse validators operate in place without copying any data and, because of their double-fetch freedom, guarantee to never read a memory location more than once. Further, we designed our specifications and input validation strategy in a layered manner, to support incremental input validation rather than incurring the upfront cost of validating a packet in its entirety before processing. All these measures ensured that the use of verified parsers didn’t introduce any noticeable performance overhead, and in a few cases, we were able to remove redundant copies and checks in existing code since these checks were already performed by EverParse.

Aside from the technical improvements to security, the use of EverParse also increased the productivity of the team.

“EverParse was instrumental in our ability to implement the product,” says Omar Cardona (opens in new tab), the engineering lead of the Network Virtualization team, adding that “the scope and complexity of protocols/messages involved could not have been addressed manually to meet the project’s timelines.”

Additionally, while maintaining our code in the Windows code base over the past 18 months, EverParse’s formal proofs of correctness and security have provided confidence that code changes don’t introduce unnecessary risk. For instance, when refactoring EverParse specifications, we prove in F* that no semantic changes were inadvertently introduced.

Scrap your handwritten parsers

We’ve replaced handwritten input validation code with automatically generated, provably safe parsers in Virtual Switch, but this is just the beginning. There are attack surfaces exposed to input validation bugs throughout the software ecosystem, and hardening them all is a long road. We believe EverParse can help.

To conclude, we offer some perspective on the landscape of input validation and parsing, particularly in the context of security-critical low-level code.

Programmers in high-level languages rarely write message parsers by hand; they use parser generators or language-integrated message formats such as JSON. Yet, for performance-critical low-level code, handwritten parsers for custom binary formats are still the norm, with parsing bugs leading to unexpected attacker-controlled “weird machines.” (opens in new tab) Language-integrated message formats for low-level code are beginning to see some uptake, notably with frameworks like protobuf (opens in new tab), FlatBuffers (opens in new tab), and Cap’n Proto (opens in new tab). However, in situations where the wire format is dictated by external constraints—as prescribed by a standard or by legacy constraints, for example—a more flexible way of specifying and parsing custom binary formats is still needed. Besides, existing frameworks don’t provide mathematical assurances about the correctness and security of the generated parsers.

EverParse seeks to make handwritten low-level parsers a thing of the past. With the state of the art in program proofs, we can generate highly efficient, provably correct, and secure low-level parsers from high-level message formats and integrate them within both fully verified components and legacy applications.

EverParse is open source on GitHub (opens in new tab). Give it a spin and get in touch!

Opens in a new tab