RVT is a collection of research tools/libraries to support both static verification (formal verification) and dynamic verification (testing) of Rust. You can download RVT from https://github.com/project-oak/rust-verification-tools/; RVT is dual-licensed (Apache/MIT) so that you can use and adapt our code for your own tools.
There are lots of hard problems in industrial research but one of the hardest is timing. If you start a project too early, your users are focused on other problems and don’t yet feel a need for your solution. And, if you start a project too late, your users have already hit the problem and you have to work round whatever solution they have found. And so it is with this project.[^but-also-other-things] At the moment, our potential users are still working on all the things you must have to support a new language in a large company and there is not a strong pull for a new, unproven research idea. So, as we close the project down, I thought it would be good to have a bit of a retrospective on what the project was trying to do and how.
To conclude this series on using KLEE with Rust for Linux, we are going to write a simple verification harness for testing the
rust_semaphoredevice driver written in Rust and symbolically execute the verification harness in KLEE. It’s worth repeating that the goal of these posts is not to verify the Rust for Linux code or to find bugs in it. Instead, my goal is that you should be able to apply these ideas to do that verification yourself. You might choose to continue in the same direction as these posts suggest by creating better mocks and test harnesses. Or you might want to try something else based on different answers to the questions in the first part of this series; or, perhaps, using some tool other than KLEE that I described in the second part of the series. The code changes described in this post are in this branch of my fork of Rust for Linux.
Using tools like the KLEE symbolic execution tool or bounded model checkers with Linux kernel code is still a bit of a black art. The first part of this series on using KLEE on the Rust for Linux considered what we would want to check. This second part, digs deeply into how to prepare the codebase for use with LLVM-based tools like KLEE. (Warning: it may contain far more detail than most people are interested in.) The final part will show how we can build simple verification frameworks. The code changes described in this post are in this branch of my fork of Rust for Linux.
The Rust for Linux project is working on adding support for the Rust language to the Linux kernel with the hope that using Rust will make new code more safe, easier to refactor and review, and easier to write. (See the RFC for more detail about goals and for the varied responses of the Linux Kernel community.)
In larger, long-running research projects, it can be useful to make a list of all the risks and research questions you have and use that as one way to guide what you tackle first. This is a list that we considered as we were planning the Rust verification project. Although some of the questions are specific to our particular context (what we want to achieve, who we want to help, etc.), I think that many of the questions apply to any project that aims to help developers to verify their own code.
A lot of our work over the last year was on identifying and fixing obstacles to using KLEE with Rust and the main technique we used for finding new obstacles was to try to use KLEE with different Rust programs and libraries. One of the largest suites of programs we tackled was the Rust CoreUtils library: a Rust rewrite and drop in replacement for the GNU CoreUtils suite that includes programs like ls, cp, df, cat, and about 90 other standard Unix shell commands.
It is inevitable that automatic verification tools will have performance problems because they push up against “the decidability ceiling”: trying to solve undecidable problems and often getting away with it. In an earlier article, we looked at how to profile the verification process to find which part of your program is causing the problem. But that is only half the problem: we need to actually fix the problem.[^not-even-half] So this article looks at one way that we can fix performance bottlenecks when verifying Rust code using the KLEE symbolic execution tool. In particular, it looks at using path-merging to overcome the path explosion problem.
Research is characterized by allowing yourself to make mistakes: performing experiments; drawing conclusions; later, realizing that your experiment was not sufficient and you got it wrong; and trying again. Back in March, we thought that we knew how to deal with vectorized Rust: tell the compiler not to auto-vectorize code; tell the compiler not to use vector instructions; and use existing conditional compilation feature flags to disable hand-vectorized code. Unfortunately, two of those three ideas don’t work – but we think we have a viable approach now.
SeaHorn is an automated analysis framework for LLVM-based languages. For users SeaHorn provides a push-button verification tool, and for researchers its modular design provides an extensible and customizable framework for experimenting with new software verification techniques. In contrast to KLEE (see previous post) which uses symbolic execution, SeaHorn uses software model checking and abstract interpretation. This, we hope, will provide better results in some cases.
A lot of our work on Rust formal verification is based on LLVM based tools and, in particular, the KLEE symbolic execution tool that can be used to find bugs and to generate high coverage testsuites. We still have more work to do but it’s a good time for a Rust/KLEE status update.
One of the major themes in our work on Rust verification is eliminating verification obstacles: things that mean that you can’t even run a verification tool on your code. So we have worked on how to verify cargo crates, how to verify code that uses the Rust FFI and how to verify programs with command line arguments. One recurring obstacle is that some code depends on processor-specific intrinsic functions. For example the Aho-Corasick crate supports fast string searches using SIMD acceleration and uses intrinsics to access the x86 architecture’s AVX2 or SSE2 vector extensions if they are available. Although verification tools could support these intrinsics, most of them do not – so if your program uses Aho-Corasick (or any crate that depends on it like the regex crate), then you won’t be able to verify your program.
Automatic formal verification is usually pushing up against what Leino calls “the decidability ceiling”: pushing the tools beyond what they can be guaranteed to solve in some reasonable time, taking the risk that the tools will blow up, but often getting away with it. But what can we do when the toast lands butter-side-down? This is a summary of a quick investigation to find out if anybody had any answers. Tl;dr: they do.
Rust is able to call C code using the FFI (Foreign Function Interface). This note describes how to verify crates that consist of a mixture of Rust code and C code that is built using a build script such as Alex Crichton’s cc-rs crate. (If your crate calls a separate C library (e.g., libX11 or libSSL), you will need to do a bit more, although this note may be a useful starting point.)
One important difference between C and Rust is that the C main function expects to be given a list of command line arguments via
argvfunction parameters while Rust programs access their command line arguments via the
The best way to install crux (aka mir-verifier) is to follow the instructions on crux’s GitHub page.
The goal of the tools and library in this repository is to let you verify interesting things about non-trivial programs. Unfortunately, interesting/non-trivial programs are too large for introducing you to a tool so, for now, we will consider this trivial program.
Our tools for verifying Rust programs are based on the
verification-annotationsAPI that provides a common API for multiple tools to use. While we recommend that you use the higher-level
propverifylibrary it is useful to describes how to use the
verification-annotationslibrary in case you wonder how
One of the most straightforward and most solid automatic verification tools is the KLEE symbolic execution tool that can be used to search for bugs in programs. KLEE was originally developed for C but, because KLEE and the Rust compiler are both based on the LLVM platform, it is possible to use KLEE with Rust programs.
subscribe via RSS