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.

Most things work

As part of our approach of “Meeting developers where they are”, our goal so far has been to figure out how to take an arbitrary Rust crate and turn it into a bitcode file that an LLVM-based tool such as KLEE can use.

As a user of our tools and libraries, what you will mostly see is

• Our “cargo-verify” script can build many real-world crates and generate bitcode that KLEE can use.

  • “cargo-verify” behaves a lot like “cargo test”.

  • (Most of) how we persuade cargo build to generate bitcode files for KLEE is described here.

• Our “verification-annotations” crate supports almost all of the functions in KLEE’s intrinsics. In particular it provides
  • A Rust trait for creating symbolic values implemented for all the primitive types.
  • Functions for adding assumptions and for reporting errors.

  This API is also implemented for other verification tools such as SeaHorn and Crux-Mir.

• Our “prop-verify” crate provides a Domain Specific Language (DSL) on top of “verification-annotations” for easily building complex symbolic values. The DSL is also implemented by the “prop-test” fuzz-tester so you can use your verification harnesses for fuzzing and your fuzzing harnesses for verification.

• We can use kcachegrind to find verification bottlenecks in Rust code (using a simple tool to demangle function names correctly).

• We have a Docker container for all the tools (because installing the full set of tools and their dependencies is quite complicated).

While the use of LLVM means that all the obvious Rust language features like closures and memory allocation “just work”, real programs depend on a bunch of other “language features” that are provided by the compiler, linker, package manager or popular libraries and we have been slowly working away on supporting all of these.

• To get bitcode for the standard library, we build the Rust compiler and standard library ourselves with just the right flags.

• Rust has enthusiastically switched to LLVM-11 (the latest LLVM) but not all verification tools support this yet. To generate the more widely supported LLVM-10, we use a Rust compiler from around August 2020 just before the Rust compiler switched to LLVM-11.

• To support command line arguments (std::env::args()), our preprocessor “rvt-patch-llvm” arranges that initializers are invoked at the start of main. (KLEE already had a similar behaviour built into it – but for a different type of initializer so it didn’t help.)

• To support Rust’s foreign function interface, our script “cargo-verify” arranges that we generate and link in bitcode for any C code in Rust crates.

• To avoid the use of vector instructions,

  1. We compile Rust code with auto-vectorization disabled.

  2. Our preprocessor “rvt-patch-llvm” modifies code used to dynamically detect the presence of vector support in the processor to say that SSE2, AVX2, etc. are not supported.

  3. We are in the process of revising the set of flags used to compile Rust’s standard library. It seems that the “hashbrown” hashing library has some hand-vectorized vector code that statically tests whether the processor supports SSE2. Sadly, turning off SSE2 can cause the compiler to generate code for the x87 FPU 😕.

With all this in place, we are starting to be able to use KLEE with interestingly large programs such as uutils / CoreUtils: a Rust rewrite of coreutils that can more-or-less be used as a drop-in replacement for the GNU originals. This is a fun choice because one of KLEE’s original demonstrations was finding bugs in the GNU coreutils suite. Whether the Rust version has any of the properties that make coreutils a good choice for KLEE benchmarking remains to be seen.

More still to do

There are a bunch of things that still need work though.

• Threads – while it is ok to use thread-safe code that protects itself using locks, it is not ok to have more than one thread 😕.

• Dynamic linking seems to be causing problems.

• Some crates have hand-written assembly language. In many cases, there is both an assembly version and a Rust version of the same code – I hope to be able to persuade the crates to just use the Rust version.

• On the design side, our cargo-verify script combines building the bitcode file with running KLEE on the bitcode. This makes it behave like “cargo test” and seemed like a good design choice. when we could only tackle toy examples. But now that we are tackling larger examples with longer build times and much longer verification times, we are starting to think about separating this into two separate phases.

• The main trick for extracting LLVM bitcode for a program is to use link-time optimization (LTO). Unfortunately, LTO can be quite slow: we need to find a way to get LTO to do less optimization!

We have also been experimenting with how to use the rest of KLEE’s API (see KLEE’s documentation [#1, #2]). In particular, we have experimental interfaces for testing whether an expression is symbolic, a Rust trait for concretization of symbolic values, and a macro for merging paths within a block of code.

Summary

So we have tools that can handle reasonably complex Rust applications, and we are starting to use them to find inputs that trigger panics and other runtime exceptions. There is more work to be done but it feels like our tools are getting close to being useful.

That said, there is a difference between a “useful” research quality tool and a “usable” tool to use as part of your everyday development and I suspect that our tools are still a bit rough for all but the most enthusiastic to tolerate. In the meantime though, we would love to talk to other people working on using KLEE or other LLVM-based tools with Rust:¹ How did you solve the problems you ran into? What can you do that we can’t do? Can we combine our ideas?

---

1. All of our code is MIT+Apache dual-licensed so you should be able to use the code or borrow code/ideas from it if you wish. ⤾