[klee-dev] KLEE/Rust - status update

[Alastair Reid]

Here's a quick update on where we have got to with using KLEE to find bugs
in Rust code.
Website: https://project-oak.github.io/rust-verification-tools/
Github: https://github.com/project-oak/rust-verification-tools/

Our goal so far has been to figure out how to take an arbitrary Rust crate
and turn it into a bitcode file that KLEE can use.
We have only scratched the surface of how best to use KLEE once we have
that. (I suspect that others on this list can do that far better than we
can.)

If anybody out there is also working on using KLEE with Rust, we'd love to
talk to you about it. And our code is all MIT+Apache dual-licensed so you
should be able to use any or all of it.

Some of the things that work are

- Our "cargo-verify" script can build many real-world crates and generate
bitcode that KLEE can use
- Our "verification-annotations" crate supports almost all of the functions
in klee.h
   - klee_make_symbolic, klee_assume, klee_abort, klee_silent_exit,
klee_is_replay,
     klee_open_merge, klee_close_merge, klee_get_value_*, klee_is_symbolic
  - It exports an API that seahorn and crux-mir can also support
- Our "prop-verify" crate provides a DSL on top of
"verification-annotations" for easily building
  complex symbolic values. The DSL is also implemented by the "prop-test"
fuzz-tester.
- We can use kcachegrind to find verification bottlenecks in Rust code
   (including demangling function names correctly)

- To get bitcode for the standard library, we build the Rust compiler and
standard library ourselves with just the right flags
- To generate LLVM-10, we use a Rust compiler from around August 2020 just
before they 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 has similar behaviour built into it - but for a different type of
initializer)
- To support Rust's foreign function interface, "cargo-verify" arranges
that
   we generate and link in bitcode for any C code in Rust crates.
- To avoid the use of vector instructions, we
   1) 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 AVX2,
etc. are not
       supported

Some of the things that don't work are

- Dynamic linking
- Our attempts to disable vector instructions sometimes cause the compiler
to
  generate code for the x86 FPU :-(
- 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 was a fine choice when we could only tackle toy examples but we are
   starting to think about separating the two steps.

And, since everyone on this list is familiar with GNU coreutils, I should
mention that I am very close to being able to use KLEE with "uutils": a
Rust rewrite of coreutils that can more-or-less
be used as a drop-in replacement for the GNU originals. Whether it has any
of the properties that make coreutils a good choice for KLEE benchmarking
remains to be seen :-)

--
Alastair Reid
Google Research

ps Here are some links to blog articles about the above

- Dockerfile for building Rust compiler:
https://github.com/project-oak/rust-verification-tools/blob/main/docker/rustc/Dockerfile
- (most of) how we persuade cargo build to generate bitcode files for KLEE:
https://project-oak.github.io/rust-verification-tools/using-klee/
- verification-annotations and cargo-verify:
https://project-oak.github.io/rust-verification-tools/using-annotations/
- prop-verify DSL:
https://project-oak.github.io/rust-verification-tools/using-propverify/
- profiling verification bottlenecks:
https://project-oak.github.io/rust-verification-tools/2021/03/12/profiling-rust.html
- initializers, "argv" and our preprocessor:
https://project-oak.github.io/rust-verification-tools/using-argv/
- foreign function interface:
https://project-oak.github.io/rust-verification-tools/using-ffi/
- Rust rewrite of coreutils: https://github.com/uutils/coreutils
-------------- next part --------------
HTML attachment scrubbed and removed