[klee-dev] Rust verification tools

[Alastair Reid]

Hi KLEE-devs,

A quick update on where we got to with Rust verification over at Google

- We am able to compile/link most Rust programs to generate LLVM bitcode.
  (The main obstacle at the moment is crates that include C code.)

- We can run KLEE on that bitcode directly
  Details:
https://github.com/project-oak/rust-verification-tools/blob/main/docs/using-klee.md

- Compiling and then running KLEE is quite complicated because you need
lots of
  obscure Rust flags to make it work.
  So, we have written a script 'cargo-verify' that hides a lot of the
complexity
  Details:
https://github.com/project-oak/rust-verification-tools/blob/main/docs/using-annotations.md

- A major theme in our research project is trying to narrow the gap between
  dynamic verification (aka testing) and static verification (aka formal
verification).
  So we have reimplemented the 'proptest' property-testing library so that
it can be
  used with a formal verification tool.
  This lets you write a single test harness and then choose to use it
either with
  the proptest library (dynamic verification) or with our 'propverify'
library
  and KLEE (static verification).
  Details:
https://github.com/project-oak/rust-verification-tools/blob/main/docs/using-propverify.md

The complete collection of tools and libraries are open-sourced using the
usual Rust licenses.
https://github.com/project-oak/rust-verification-tools

This is very much a research prototype at this stage - more interesting
than useful.

--
Alastair
-------------- next part --------------
HTML attachment scrubbed and removed