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.
Posts
-
Retrospective
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.
-
Using KLEE on Rust-for-Linux (part 3)
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 KLEE on Rust-for-Linux (part 2)
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. -
Using KLEE on Rust-for-Linux (part 1)
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.) -
Research risks in the Rust verification project
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.
-
Using KLEE on Coreutils
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. -
Fixing bottlenecks in Rust verification
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. -
Verifying vectorized Rust revisited
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. -
Using Seahorn
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. -
Rust/KLEE status update
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. -
Verifying hand-vectorized Rust code
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. -
Profiling Rust verification
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. -
Using Rust's foreign function interface
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.) -
Using command-line arguments ('argv')
One important difference between C and Rust is that the C main function expects
to be given a list of command line arguments via argc/argvfunction parameters while Rust programs access their command line arguments via thesys::env::args()library function. -
Crux-Mir installation
The best way to install crux (aka mir-verifier) is to follow the instructions on crux’s GitHub page.
-
Using the `propverify` library to verify Rust programs
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. -
Using the `verification-annotations` crate
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-levelpropverifylibrary it is useful to describes how to use theverification-annotationslibrary in case you wonder howpropverifyworks. -
Using KLEE
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