Thesis: Simple Verification of Rust Programs via Functional Purification


#1

Hey Rustaceans,

You may have read my previous post on my masters thesis on program verification in Rust. Well, I’ve since successfully defended my thesis, so here you go:

I’ve mostly been back at working on the theorem prover, Lean, itself since then, but I may very well pick up this project again in the future as soon as start my PhD in… *checks watch* oh, tomorrow!

/cc @nikomatsakis @RalfJung @cmr


Status of Rust Code Analyzers
#2

Awesome! One thing, though - in reading through it, the signature of the WhyML in the “Related Work” section doesn’t seem to match the Rust code you give.

The Rust you give is:

fn get_mut<T>(slice: &mut [T], index: usize) -> &mut T

while the WhyML is

let get_mut (a: array (ref int)) (i: int) : ref int = a[i]
let get_mut (a: array int) (i: int) : ref int = ref a[i]

However (depending on the semantics of WhyML, which I am not familiar with), those seem like they’d be more similar to the following:

fn get_mut(a: Rc<[&mut i32]>, index: usize) -> &mut i32;
fn get_mut(a: Rc<[i32]>, index: usize) -> &mut i32;

and that a more accurate analogy might be

let get_mut (a: ref (array int)) (i: int) : ref int = ref a[i]

(Which would still return a copy, thus preserving your point that WhyML does not permit all of the niceties that Rust’s references do).


#3

These definitions weren’t meant to be equivalent — “For example, the first of the following two WhyML functions fails to type check […] In contrast, Rust can provide a perfectly safe function with this functionality”.


#4

@myfreeweb: The distinction I’m making is that there is a spurious difference, namely that while the Rust function mandates unaliased access to the whole slice, the WhyML functions do not - and instead use an “array of unaliased references”, or even merely an array of integers. This obscures the point that “this function (signature), which types in Rust, cannot be implemented in WhyML.”


#5

IIRC (yeah, maybe I should have described WhyML in more detail), array already implies both indirection and mutability and is subject to the same aliasing restriction as ref, so nesting them like this doesn’t buy you anything. Curiously, I can’t even get it compiled on http://why3.lri.fr/try/. The original WhyML paper doesn’t talk about the aliasing restrictions at all, unfortunately. The best description I could find is this mailing list post: https://lists.gforge.inria.fr/pipermail/why3-club/2014-January/000890.html


#6

Very impressive stuff. A couple of questions:

  1. Is there any intrinsic reason for choosing inductive Lean library vs the constructive (HoTT-based) one, other than maturity/familiarity? Or would there be some incompatibility with the other model?
  2. Any thoughts on gradual deeper integration with rust, so that over time whole subsystems and entire crates could get proofs?

#7

Congratulations @Kha :slight_smile:


#8

The HoTT support in Lean has been removed and won’t be coming back, see this recent mailing list post: https://groups.google.com/d/msg/lean-user/90_nKwp-euU/LpRIIZBwDgAJ


#9

While HoTT is gone in Lean 3, as @cmr mentioned, my thesis was still written in Lean 2. My work is mostly constructive, except for the loop combinator, which has to “solve” the halting problem after all. I’ve never really familiarized myself with HoTT, but I don’t think there are many benefits to using it for topics such as program verification.

[quote=“tupshin, post:6, topic:9704”]
2. Any thoughts on gradual deeper integration with rust, so that over time whole subsystems and entire crates could get proofs?
[/quote]What kind of integration are you thinking of? You could totally use the tool to verify arbitrary crates right now (as long as it’s in the supported subset of Rust), it’s just that you would probable need to verify sizable portions of the standard library first, and of course that verification takes some huge time and effort in general (hopefully less so in a future version using Lean 3).


#10

Thanks for the perspective on #1.

Regarding deeper integration, some semi-random throughts:

  1. a cargo plugin would be an obvious start, so that if a crate included lean verification, running cargo lean-verify would recheck against any changes to the rust code
  2. rust annnotations, on a per function and per module basis, that flags them as being verified, and requires verification to succeed for compilation to work.
  3. Ability to annotate your rust code with #[assume_verified(fun1, fun2)] (or some such) to automatically generate lean lemmas to assume fun1+fun2, allowing this rust crate to assume itself as verified pending proof of its unproven dependencies.

#11

I think that Rust shines and can fill a niche as being a high performance, high security language. Which is a big niche and point being security is extremely important for Rust to succeed.

Which makes this one of the most important Rust projects I’ve seen yet.

Personally I would do a search of cargo to find the most used core Rust functions and one by one starting from the most used verify them and train some other people to help out.

Might even be able to get some kind of Mozilla grant or something for it.

Congrats on the great work! Keep it up!


#12

The Prototype Fund is still open for project submissions with grants of up to €30,000.


#13

Plus they also have bug bounties if you find something and there are a bunch of companies using Rust who might happily chip in something, maybe even programmers toward the effort:
https://www.rust-lang.org/vi-VN/friends.html

I would particularly talk to the companies where security is a priority.


#14

Wouldn’t formally verifying the standard library first require a formal model of the unsafe code semantics?


#15

Thanks for the grant suggestions :slight_smile: . I don’t know what shape my PhD program will take yet, but it may be hard to get publications out of “just” doing verification work - except when they necessitate coming up with novel ideas, of course.

Thanks, those are some nice suggestions for attacking the problem at scale. For the modest number of current verification proofs, I was thinking about a simple approach like having a nightli.es hook check daily that everything is still working. But for that I’d first have to update my project to link against a recent rustc that can actually build the nightly stdlib (which usually breaks everything in my code).

Verifying “the standard library” isn’t a very realistic goal anyway, I’m afraid. You would usually start with a single function or data structure whose correctness you’re interested in and then choose to prove or simply assume the correctness of each of its dependencies - if the dependency uses unsafe code, you will have to do the latter. Correctness proofs will always be dependent on some unproven assumptions (axioms) until we have a verified Rust compiler.