Kani Rust Verifier
| Abstract: Rust has made significant inroads as a popular safe systems programming language over the decade since its release. Stack Overflow has named Rust the "most loved language" every year since 2016. One of the language's main selling points is its focus on reliability---the ownership type system is a success story of programming language memory safety research breaking into the mainstream. The borrow checker eliminates certain high-impact classes of bugs, including null pointer dereferences, use-after-frees, and leaked memory. A team writing safety- or security-critical code, though, may seek an even higher level of assurance than what the current type system alone provides. |
While Rust's type systems rules out most memory safety bugs in checked safe code, there remain many ways for execution to go wrong. The language provides an “unsafe” dialect that allows programmers to bypass restrictions to regain more expressivity for lower-level regions of code. Even in safe Rust regions, the type system does not rule out dynamic panics from out-of-bounds or indexing errors (for example, consider the well-type-checked snippet let v = vec![1, 2]; v[3]}). Finally, engineers may want assurance of functional correctness – the ability to assert specific properties about the result of a program under all possible inputs.
At Amazon Web Services, we are building an open-source tool, the Kani Rust Verifier, for sound, bit-precise symbolic analysis of Rust programs. In our previous work on symbolic correctness proofs of production C code, we found that (1) embedding specification into proof harnesses similar to unit tests, and (2) integration with existing developer workflows were key to broad impact on software engineering teams. We discuss the unique needs of high-assurance Rust systems programmers, and how Kani is designed to seamlessly integrate into their existing verification workflows.
Daniel
is a Sr. Software Development Engineer in the AWS Automated Reasoning Group. His work has focused on using formal methods to verify and debug low-level code, ranging from runtime verification of multi-threaded C programs, to automatic inference of the causes of C crashes, to verifying the side-channel resistance of cryptographic implementations. Most recently, he has been the tech lead of the Kani Rust Verifier, a bit-precise model checker for Rust.
When he’s not working, you might find Daniel in the kitchen making dinner for his family, in a tent camping, or volunteering as an EMT with a local ambulance squad.
Zyad Hassan is an Applied Scientist in the Kani Rust Verifier team at AWS. Prior to that, he was part of the R&D team at Siemens developing their hardware formal verification tool. Zyad got his PhD in model checking from the University of Colorado at Boulder in 2014.