GoKawiilMany open-source and industry software projects, including several here at Amazon, are embracing the Rust programming language, since it provides performance and flexibility similar to that of the C programming language, while its clever type system automatically prevents a variety of bugs and security vulnerabilities. The result is fast code that's more correct and secure than average.
However, "more correct and secure" is not the same as "actually correct and secure". For example, in C, accessing an array out of bounds — indexing into an array past the boundary of the memory allotted to it — is a dangerous mistake that can have unforeseeable consequences. In Rust, it will halt the program, which is definitely safer, but a correct program would never perform the out-of-bounds access in the first place. Similarly, Rust cannot guarantee that your program will compute the results you were expecting or that it won't leak the secrets it has access to. That's where Verus comes in.
Accessing an array out of bounds is a dangerous mistake that can have unforeseeable consequences. A correct program would not permit it.
What is Verus?
Verus is an open-source, automated program verifier for Rust. A "program verifier" takes in a formal mathematical specification of how your code should behave and mechanically checks that your code matches that specification for all possible inputs.
For example, your code might implement an optimized binary-search algorithm to look for a particular value within a sorted array. The specification might state that when the code successfully returns an index, the corresponding element in the array matches the target value. The verifier checks that this specification holds for all possible input arrays and target values.
In contrast, traditional testing techniques might try a few specific arrays but can miss corner cases (e.g., what if the target value is the last element in the array or not present at all?). A key aspect of program verification involves constructing a mathematical proof that the code matches its specification. In an automated program verifier like Verus, the tool automatically handles many of the boring, low-level steps of proof construction, while the human developer provides high-level guidance (e.g., setting up an inductive proof or supplying a loop invariant). As we discuss below, these days, even the high-level steps can often be automated by AI.
At Amazon, we're proud to have been a founding member of the Rust Foundation, and we use Rust extensively for projects like Firecracker, which powers AWS Lambda and AWS Fargate, our serverless distributed SQL database, and the Nitro Isolation Engine, which enforces virtual-machine isolation for the Nitro hypervisor, the software that manages virtual-machine allocation for Amazon Web Services (AWS). Amazon's excitement about Rust, combined with more than a decade of work on automated reasoning, makes it natural to adopt Verus to provide even stronger guarantees for the Rust code we're writing. Indeed, we've used Verus to prove the correctness of key primitives used by the Nitro Isolation Engine, as well as a number of critical pieces of infrastructure used within Amazon. We'll explore these use cases in future posts, but for now, we want to tell you more about what it means to verify Rust code with Verus.
Verifying Rust code with Verus
... continue reading