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.
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