Putting the Rust in Trust

Formal verification is using mathematical techniques to analyze software. In general, one wants to show that a particular program implements some specification ("functional correctness"). But there are other things you can show too! For example, seL4 shows high-level security properties like integrity and confidentiality. Actually doing this is quite hard, but relatively well understood these days. You need to model the program, then show that the model satisfies the spec. Hopefully, the model corresponds to reality. In practice, many verification techniques have serious problems with reality-correspondence.

As one semi-famous example, binary search was "proven correct" many times, but still had buggy implementations. What was the failure here? The model used mathematical integers, but the reality is finite, wrapping words. This is a complete embarrassment that any principled use of formal methods should avoid. If your model doesn’t correspond to reality, you need a tedious, manual, error-prone validation of the implementation. We can do better!

The first phase is modeling the semantics of Rust programs. There are quite a few partial approaches to this so far. This is not to disparage their efforts - I hope they continue and succeed, because more work in this space can only be good!

On the one hand, you want a semantics so you can prove things like soundness of the language’s type system, or memory safety of fragments of the language. On the other hand, sometimes you want to actually prove properties about specific programs in the language. The former can sometimes use a simplified model, depending on the type system and guarantees it wants to make. The latter needs to capture all details of the language that are relevant to the program under consideration, and is generally much more formalization-intensive.

I have my own in-progress semantics for MIR, that I’m working on between Robigalia sprints. In general, I think MIR is the best short-term approach for initial verification of Rust programs. In the long term, someone will need to write a full semantics for actual-Rust, and write either a verified compiler or a proof-producing translator from that into MIR. This will be very challenging, as Rust’s type system is rather complex. I suspect the RustBelt folks will have the best start of this.

At this point, implementations of Rust (eg, rustc) could use the semantics to resolve confusions and as a ultimate arbiter of deciding correctness of some program transformation (eg, an optimization). In the long run, the semantics could serve as the normative specification of the whole language.

Given a semantics for MIR, one can define things like Hoare logics over MIR programs. The benefit of having a semantics at this point is that the program logics can be shown sound, which is rather important. Soundness of a program logic means that properties proved in the logic are also true of the program. Ticki’s and RustProof’s works, mentioned above, can not be shown sound without a semantics for MIR.

You really want properties in the program logic to be nicely composable, so that proving results about, for example, portions of libcore can be slotted easily into proofs about larger programs. At this point, one could start writing specifications and proving functional correctness of small programs or library functions.

My plan for this right now is to use a separation logic and a semantic Hoare logic combined with something like AutoCorres to make verification easier. I hope to lean very heavily on the extensive libraries and infrastructure that the Data61’s TS group has created. It will be a lot of work getting this working, but the down-the-line productivity benefits could be huge.

Given a proven-correct MIR program, we need some way to actually execute that program, in a way that the correctness proofs still apply. And ideally, we would like to retain most of the efficiency of writing in Rust instead of some higher level language like Haskell.

My plan for this right now is to write a MIR-to-"CakeML" translator, and use CakeML’s verified compiler to do all the heavy lifting of compiling to machine code. At first it would use their garbage collector for memory allocation. But with a verified allocator, potentially written in Rust, the GC should be avoidable.

In the very long run, it’d be good to connect to something like CompCert or even VeLLVM. These have their own unique challenges. For particular high-value programs, it might even be worthwhile to do something like seL4 and prove correspondence of compiler output and source program. I don’t know how feasible this will be, but it’s worth investigating.

Once we’ve written our program, shown that it satisfies the desired specification, and have an implementation that formally corresponds to that program, and have proved that the specification has the properties we depend on, we can start relying on these programs for the most critical of software. At this point, our software is truly trustworthy.

This is my long-term vision, and a lot of sweat and elbow grease needs to go into making it a reality. But my hope is that the inherent strengths of Rust will make it easier and cheaper to build trustworthy software, compared to traditional methods used in C.

Thanks Alex Elsayed, James McGlashan, Gerwin Klein, and ticki, for early feedback on this post!