Using Klee on Rust Programs
I've written before about klee: a symbolic execution engine that operates on LLVM bitcode. It's traditionally been used to verify C & C++ programs, but in principle it could analyze programs in any language that we can compile down to bitcode… like Rust.
In practice, however, it's proven to be quite an undertaking. When moving to a new language, with a new compiler & new package ecosystem, your bitcode will be sufficiently different to give klee trouble (for instance, using compiler intrinsics new to klee). The other major issue is that klee only operates on complete programs, so to truly verify your code you need to not only compile your application down to bitcode, but also all the libraries on which it depends. This is a chore even in C & C++, where klee has been working for years. In a new language like Rust, it's a serious undertaking.
I found a few efforts around this, all abandoned. The most serious was Project Oak, an effort at Google Research that seems to have died-out in 2021 when it's lead, Alistair Reid, departed for Intel.
Still… their code is still up. One could pick it up & try it. I dunno… feels like a rabbit-hole to me. I wonder if the way forward is focusing less on whole-program analysis and more on validating smaller units of code. Could we replace mocks with propositions?
11/08/23 17:09