Rust Programming Language Rust Verification Workshop 2021, 11 May 2021

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: RustBelt: A Quick Dive Into the Abyss

Description

Ralf Jung and Michael Sammler

A

With that, we are ready to introduce the first talk, so the speakers will be ralph jung and michael sumler they're, both from the max blanc institute for software systems in germany and are working there with derrick dryer, and so they they're working, among other things, on rust belt, which has been a very influential project in our area and I'm really looking forward to hearing their thoughts about uh rust and unsafe rust. So please go ahead.

A

B

uh Thanks thanks for this kind introduction, so hi everyone, uh I'm michael.

C

And I'm ralph- and we are your diving instructors for today, where we'll take a quick dive into the abyss that is called.

C

I need rasped focus the right thing, so the goal of rust belt is to put rust safety story on formal footings and the way we view rust safety story is that it really rests on two main pillars. The first pillar is the obvious one. It's the sophisticated ownership and borrowing checks that the compiler is doing to ensure that everything works safely.

C

The second pillar is less obvious, but we think equally important and it is unsafe code and the idea of safely encapsulating that unsafe code behind an api.

C

So the way we view a rust program is that there's a large body of safe code making up most of the application, which is well saved by construction, because it's type checked by the compiler. But then there are some libraries in particular at the bottom of the stack which internally use unsafe code.

C

However, to shield the rest of the application from this unsafety, they will wrap this unsafe code behind an api together with a promise that, if all you do is interact via that api in a well-typed manner, then your program will not go wrong and you still have all of the safety guarantees of rust.

C

So as part of rustbelt we've set out to formally approve this, and I hope it's clear now that, as part of the proof, we have to account for these unsafe libraries- and we want to do this in a way that is extensible so that when a new library comes along, we don't have to redo all of the proofs so to get started.

C

Let's prepare for our dive by mapping out the abyss that we are interested in, namely by looking at the structure of respect at the core of rustbed, is lambda rust, the formal modeling language for us that we developed we're not going to talk much about the language itself here, but rather focus on its type system. The type system provides some of the usual base types you might expect.

C

It provides three kinds of pointer types where these owned pointers correspond to boxes, but we also use them to model stack variables and then mutable and shared references are exactly what you know from rust. You also have product and sum types corresponding to structs and enums respectively and not shown here. We have function, pointers and recursive types which are tricky to model, but not the focus of this talk.

C

Those types are then assigned to paths in the typing context: we're using paths instead of the more usual assigning types to variables, because the borrower checker is able to reason about the fact that different fields of a struct are disjoined and can be separately borrowed, so to be able to represent that our typing context can separately talk about fields of a struct, and this is exactly what a path denotes.

C

And finally, of course, at the core of the type system are the typing judgement, the two most important ones, being first of all, well typed instructions. So an instruction I is said to be well typed under some context, e and l, which tracks the which track the lifetimes and do the borrower, tracking and typing context c1mt2, where t1 is the typing context before the instruction I executed. Nt2 is a type of context. After the instruction is done.

C

We need to type in context because, of course, in rust we can use an instruction to move ownership from from our context to somebody else's like by calling a function, so the second context might actually be smaller than the first one. This is, our type system is substructural in that sense, and then the other typing judgment I want to highlight here is the one for typing: an entire function body, which also has e l and t contexts. It doesn't have a t2 context as a post context because functions, don't return.

C

Your model functions in continuation, passing style, so they're called a continuation when they are done and k tracks the available continuations.

C

So what are the properties of this typesis? Well, usually, the main thing you would be interested in proving is our type safety theorem which says that if the, if a function body is well typed, then the function is safe to execute. In particular, it's thread safe and memory is safe. However, this theorem is actually not as useful as you might think, when applied to a rust program, because every basically every rust program has some unsafe code somewhere. An unsafe code is essentially untyped, for all intents and purposes, and our typing judgment or typing theory.

C

Sorry, our safety of the safety theorem only applies if the entire program is typed and well typed, so we can't apply it to a program that contains some unsafe code. We have to use some other mechanism and the approach we're using is based on the idea of logical relations. It's the semantic approach where you basically give semantic meaning to all of the type system concepts in particular for each of the types in our type system.

C

We give what's called a semantic interpretation which essentially formalizes the invariants that are reflected by this type and then for each judgment of our type system. We also give a semantic adaptation, which formalizes what promises and guarantees such a typing judgment makes about the code that it applies to.

C

So let's look at those in a bit more detail. First of all, the semantic interpretation of types. What we have to basically do is define for each type, a corresponding predicate, except which precisely captures what are the invariants, that the type reflector that the type makes on the data that it applies to in raspberry. Specifically, we don't just make these a predicate that expresses invariance over the value, but also over the idea of the thread that is claiming to own this data.

C

This is important when modeling types, which are not send or sync- and we will see this in action later- recalling is an ownership invariant because in rest of course, type don't just reflect the structure of the data. They also reflect ownership of resources such as memory, and this has to be reflected in these invariants as well.

C

So a question now arises, which is how do we express this ownership? How do we express the invariant? What kind of logic do we use to do that? In our case, the logic we use is separation lodge, which might seem like a strange choice at first, but it's actually really well suited for modeling the rust type system, because separation logic already has a built-in notion of ownership, which we can use directly to model ownership and rust.

C

Specifically, the separation logic we are using is iris and we're using it, not just because it's our own logic, but also because it really fits the task for modeling rust very well.

C

First of all, it is implemented in the cockproof assistant with an interactive proof mode, so we can do all of these type system proofs in and have the machine check for errors, and, secondly, ios is designed to be extensible with new reasoning, principles which is useful not only to model complicated, new rust concepts, just borrowing and lifetimes, also, but also to verify intricate libraries such as the reader writer log, that require non-trivial reasoning to show their correctness.

C

So let us now assume that we have defined the ownership invariant for every type tau in our system. What's next well, we're now going to lift this through the other constructions of the type system. So next up are typing context. We have to define, when is the typing context? Satisfied and, of course, essentially, a typing context is satisfied when all of the individual type assignments in the context are satisfied. So for each path p mentioned in there, the value denoted by that path satisfies the invariant denoted by the corresponding type to compose these invariants.

C

Where there's multiple elements in the in the typing context, we use a separating conjunction, which very concisely expresses the fact that in rust, distinct variables are separately owned. So if you have two vectors and you give away one of them- you still own the other. So here we have a very nice and abstract way to represent this rather subtle concept, and we can also reason about it.

C

Abstractly, thanks to the power of separation logic, this would be much harder to do if we hadn't chosen the separation logic as the foundation for all of this having solved the typing contexts, we move on to the typing judgments. So, for example, when is an instruction to become semantically considered well typed.

C

The basic idea here is that an instruction is well typed if, whenever all of its assumptions that it makes like the e and l contexts and it's pre-typing t1, whenever those are satisfied, then we can execute the instruction safely and once the instruction is done, the post type in context, t2, is satisfied and also e and l they're left unchanged.

C

So again, we can use a connector from separation logic, if you say this very abstractly by just using a halter, we don't have to invent new ways or or use complicated mechanisms to express properties of program executions. We already have a principle built in for that in iris and all the corresponding reasoning principles.

C

So once we did all that now, what does this story look like when we have a large application where there's some unsafe code in there, and we want to reason about the safety of the whole program. Well, in the top left corner, we can think of having the safe code, which the compiler type checked and which hence, we have a safe typing deliveration. For, however, somewhere in the program, there will also be a library like cell, which is not syntactically, well typed in our type system. However, we can still look at the statement.

C

That cell is semantically well typed, which is, as I've just shown basically over triple, and we can manually verify that quarterback using standard program, verification techniques in our case manual proofs in.

C

Furthermore, we can show that the semantic notion of typing composes, in the same way that you would hope any type system composes that syntactic typing implies semantic typing and that semantic typing implies safety, so putting all of this together. The result that we get is that a large body of code, a large program, is safe. If all the unsafe pieces are safe, we only have to manually prove the unsafe bits, and then we get safety of the entire program and of all of its safe code for free.

C

So this is exactly what you would hope for in a rus program.

C

Now that we have an idea for what the structure of rust belt looks like, we can start to get our feet wet by looking at how one can define these ownership invariants and we're going to start by looking at the box type that we all know and of box represents ownership of some part of memory, and so it should not be too surprising that to represent the ownership environment of box type, we use the points to connect if the hallmark connective of separation logic, which exactly represents ownership of memory.

C

Specifically sub-location l, is a valid box pointer if it points to some memory w such that at w. We have indeed some data which satisfies the ownership and variant of the point of the type tau which the box promises to point to there's some more stuff going on here that I'm hiding related to dear location. But we don't really need to worry about that now. Instead, let us look at the type, the ownership and variant for mutable references.

C

First of all, we can see that it's mostly the same. We again have that. There's some memory that l points to some data w and that at that, at that value, w is indeed um satisfying the typing invariants for top. So, as you would expect a mutable reference is a lot like box. The key difference, however, is that we don't just plainly own that memory, but we own it below this funny little ampersand, kappa full, which is the connective of the lifetime logic.

C

The lifetime logic is an extension of separation logic that we developed to be able to reason about lifetimes and borrowing and rust, and it's really one of the one of the key contributions of raspberry most of its complicated details are not very relevant here. The key aspects of it are the kind of statements that the lifetime logic lets us make as part of our separation logic and variance and proofs, namely, first of all, this ampersand kappa full p that we've already seen expresses exclusive ownership of p but restricted to the duration of the lifetime, kappa.

C

So we know nobody else can use p, but only as long as kappa is ongoing to be able to actually use p. We just need some way to say or prove that kappa is still running, which is where the other lifetime logic connective comes in this bracket. Kappa here is what we call a lifetime token and it witnesses the fact that kappa is still ongoing and also represents some form of ownership of the lifetime, because we can use this token to end the lifetime if we want to so.

C

This uh concludes the first part of the talk where we very kind of getting prepared, I'm not going to hand over for michael for the underwater parts of our little journey. Great.

B

Thanks so I'll take over the dive from here and we're going to look at maybe the uh most well-known type using interior mutability in rust, which is cell and especially at how we can verify the cell type using rust belt.

B

So, let's start by looking at the steps, we need to do to verify a type like cell in rust belt. So the first thing we need to do is we need to figure out the type and variance of our new type, and especially uh or formerly, this means we need to figure out the right semantic interpretation of the cell type into a iris and as a second step, once we have the semantic interpretation and the type and variance we need to prove that the functions on this type are respect these invariants or formally.

B

We need to verify that all functions, especially the function using unsafe code, are semantically well typed, using the type interpretation for the cell type.

B

So, uh let's get started by figure by looking at the type and variant for cell, and for this we look at the functions which convert between t and cell ts in particularly, we look at a new which takes a value of type t and converts it to salty and into inner, which takes a value of type salty and converts it to t, and, as you can see here, both of these functions don't really do anything right.

B

As you may know, cell is just uh and a no wrapper around the value of type t using the unsafe cell marker type and necessary for interior mutability, but both functions just kind of copy, the value, its argument to the return value and basically just change the type uh change its type.

B

So this means when we define the when we define the ownership invariant of cell, we only really have one choice, which is to set the ownership invariant of cell to the ownership invariant of t, because these two, these two functions kind of witness, an isomorphism between cell t and th.

B

So um now that we have the ownership invariant for cell t, we can actually do the second step and uh prove that one of these functions uh here we'll take mu, is semantically well typed uh for that uh ownership invariant.

B

So the first step we need to do is we need to figure out what do we actually need to need to prove about this new functions? And for this we look at the type of new, so we get a value of type t as the argument. So this means we need to prove a triple where the precondition is that we have t owned for for well, and the function returns the salty, so we have to prove in the end, in the post condition uh salty own for the return value.

B

So with that out of the way we can look at the the code and the the ownership invariant for salty again, and when we look at this, um we see that this proof here is very simple right, because we start with the uh ownership uh of val, like t uh t own for val and the function doesn't really do anything um and t on uh for well is the same as uh salty own for for for the value. um So we just need to kind of unfold.

B

This definition once- and we are immediately done with this proof- and this way we've actually verified our first one function in roswell like shown that it's semantically well typed, but now, let's dive a bit deeper.

B

Let's look at the more interesting aspect, which is a shared reference to a cell, so so far, we've seen that uh t uh kind of is the same as salty like when when they're owned. But um we also know that a shared reference to t is also it's very different than uh shared reference to a celti, because when you have a shared reference to a t, you usually cannot mutate through that shared reference.

B

But if you have a shared reference to a celti, you can you can mutate through that, so there's something very interesting going on, which is that the ownership invariant, which we've seen so far, cannot be the whole picture right, like it's the same for tea and salty, but like uh for shared reference. They are different.

B

So what we actually need is we need to have a separate invariant for kind of shared references, uh a separate invariant for for a shared cell, which makes it which is then different to the shed invariant of just t its own on its own and the way rust belt does.

B

This is that a semantic type not only consists of the ownership invariant which we've seen so far, but there's also a sharing invariant tito chair and used by shared references, and it has three parameters so first, the lifetime kappa, is the lifetime of the of the shared reference. It's also parameterized by a thread. Idt and l is the location or the pointer of the shared reference.

B

So now that we know there that there's also the sharing invariant, the obvious question is: what's the sharing invariant for celti.

B

So, uh let's figure that out and for this we look at one interesting function which uses shared references to cell, which is the set function, so uh set gets a shared reference to a cell as the argument and a new value, and then it uh mutates the the value stored in the cell and, like updates it to the to the argument and now the question is: why is this function safe and uh at first glance?

B

This is a very, very, very weird function for us, because um we get a shared reference as an argument, but we mutate through that shared reference, and normally this is something which rust doesn't allow, and this is for very good reason, because if you have that shared reference and maybe like and you have it in multiple threads and you use that from this function here concurrently, you can very easily get data races which are very bad and we want to prevent.

B

So um why is this not a problem here? And the reason is that cell, as you may know, is not syncs. So this means that shared references to cell are tied to the same thread. You cannot send them to another thread, um which means that there is no concurrent accesses um to to ourselves through uh shared references.

B

So there's actually not a concurrency problem here, because there is not really any concurrency around the shared reference to a cell, and there is another bit more subtle reason why cell set is safe, which I don't want to go too much into, but um so it's important that you cannot get a pointer to the value stored inside the cell and because the set function would invalidate such interior pointers um so yeah. So now, let's figure out the sharing invariant for cell.

B

So we know that uh we somehow need to exploit that a shared reference to a cell does not allow concurrent accesses and the way we exploit. This is using a special kind of borrow and which is called a non-atomic borrow that you can see here. So the there are two important aspect about the non-atomic borrow. So first, the non-atomic borrow is tied to a specific thread.

B

So you can see it's parameterized by the thread idt here um and the non-atomic borrow is always always stays on the same thread, which means we don't have to worry about interference from from other thread when opening this, when interacting with this non-atomic borrow and the other important aspect of the nonatomic borrow, is that it's duplicable and right, which is important because um it's like we put into the sharing invariant and the sharing invariant needs also be to to be duplicable.

B

Because you can, you can copy a shared reference uh right and you can do that uh as often as you want. As long as you stay mo stay on the same thread.

B

So now that- uh and that's also the reason why we cannot use a full borrow here, the that ralph showed before, because the full borough is not duplicable so, uh but we can use this non-atomic borrow here.

B

So now that we've seen this uh talked about. This non-atomic borrow. Let's look what's inside the nomin atomic borrow, so um the invariant there is that uh the value of the uh of the cell points to some some value b, and we know that uh v is well typed at the type t great. So now that we know the sharing invariant for cell we can.

B

We can look at how we can verify this. This set function. So again we look at the type of set and we see that uh the first argument is a shared reference to a cell.

B

So we get the sharing invariant for uh for the self argument, uh yeah the for for cell t, and the second argument is something of type t, so we get t.one for for well, but there's one important other thing which we're getting, which is um a lifetime token for the lifetime of the shared reference, because we know that this function can only be called while the the lifetime is alive.

B

The lifetime a is alive, and we also have to give back this lifetime token at the end of the function to um yeah, because, like th, this function cannot end the lifetime a so uh now we can look again at the code and the the sharing invariant and start the proof, and the first step of the proof is that we we take this lifetime token, and we kind of combine it with this.

B

Non-Atomic borrow in particularly what we can do with this non-atomic borrow is that we can give up the this lifetime token uh for for the lifetime alpha and uh trade it for the content of the of the non-atomic borrow. So from that we get some new value b, prime, and we know that uh self.value points to that v. Prime, and we also know that b, prime as well type, the type t, um and now that we have access to this points.

B

To fact, we can actually symbolically execute the code and now know that self.value as type no points to val and from the precondition. We also still know that uh t-one holds for well now we're almost done, but we need to know at the end of the function. We need to get back the lifetime token, and we do this by kind of closing the borrow by uh putting what we got out of the borrower back into into the borrowing and using that to get back the lifetime token right.

B

So we put these two assertions about like the points to fact and the t-one for val back into the borrow and from that we get back the lifetime token and uh then we're we're done with our proof. uh So this is uh actually yeah. So now, we've actually verified our first function using interesting, unsafe code using uh rust belt.

B

So now we actually go to the deepest point of of our dive, which is how a rust belt looks like in cog and let's first look at the definition of the cell type uh in in cork, and we see that this definition is very similar to what the informal definition which I showed before.

B

So this thai own is the ownership invariant of the cell type, and you can see it's directly defined as just the ownership invariant of tie and the sharing invariant of of cell is very similar uh like in in cork, is very similar to what what I've showed you before.

B

So uh now, let's look at how cell new uh looks like in cork and and it's proof so we see a cell new translated to lambda. Rust is just basically the knob right, as we've seen before. There's nothing interesting going on in cell new and the proof for new might maybe look a bit intimidating, but it's mostly boilerplate code and the only interesting part is the uh happening in the don tactic.

B

At the end of this proof, which is just looking at this uh unfolding, the definition of tie on for cell and proving that is the same as taion for for thai.

B

um So now, let's look at uh cell replace uh in cog, which is what we actually verified in in rust belt, because it's a bit more more interesting than cell set and you can actually verify uh or you can implement cell set using cell, replace using safe code.

B

So I don't want to go into much detail about this code, except that it is more complicated than cell new and the proof for cell cell replace is also a bit more complicated, at least when you're not familiar to uh with iris. If you know iris, this is actually a relatively straightforward, straightforward proof, and this is also a bit more complicated than the informal proof I've shown you before, because in cog you need to do a bit more bookkeeping like the life story around the lifetime.

B

Talking is a bit more complicated than than what I actually showed you before, and certainly we can develop also better automation for these for these proofs in cog.

B

But um if you actually know iris, then it's pretty easy to actually follow. Follow this proof and understand what's going on, and this is that actually verifying semantic type. Safety is just doing a kind of relatively standard iris proof.

B

So that's also the note which I want to end our dive on, um which is that semantic typing might look a bit intimidating, but actually fundamentally, it's just standard program, verification uh in iris, and I hope you enjoyed our quick dive and uh thank you for our attention and careful of decompression.

A

Thank you very much for a very nice presentation, so we have time for one or two questions. There have already been a couple of questions on the chat which I guess we will handle there. Are there also any questions that you would like to ask via audio.

A

But I can maybe start with one, so I noticed that your deep dive, so the the depth grew exponentially. Does that reflect the difficulty of the proofs? Is that really that it gets so much harder when you go from from one language feature to the next.

B

Well, the yeah the depths were chosen kind of in a random manner. It's it's hard to quantify difficulty because, like it's also very different things right like if you look at the own interpretation of cell, it's like really trivial and, like figuring out like there's, none atomic boros.

B

They are kind of quite quite more difficult and there's like also a lot of stuff going on under the hood uh to make actually this non-atomic boroughs work and then doing everything in is also harder than doing it just informally or like at the side level with which we've done before, um but yeah. Whether it's exponential, I don't know.

C

A

C

To add zeros, then try not trying to do anything precise.

A

So we have a question on the chat that I think is probably uh interesting to many people in the audience. So so what what are the chances of of using these ideas and uh and putting them into a tool, and maybe automating uh part of these proofs? So what's what are your thoughts there.

C

I mean my thought is that I would really like to develop such a tool.

B

So this is something which we're actually also kind of starting to work on, and so I personally also worked a bit on on uh verifying actually c code, where I also developed kind of ideas of actually making this more automated and automating iris proofs, and I would be very interested in actually applying this also more to raw spell so that we can actually um kind of automate. This proof.

B

I think we can get uh get a lot of automation and, like a lot of it, is also just engineering like building a front end which translates stuff in into um which yeah well like there's quite a bit of intra interesting engineering to do which we haven't done yet.

C

Yeah, I think types like vic should be basically entirely ultimate entirely automatable. Once somebody gave the key typing and variants um because there's not even in terms of ownership, that's not going on in big cell is a bit more complicated. Ref cell and rc are a lot more complicated, so I don't think those are in reach for verification currently, um but I mean we can start with the easier types and then I think in the end, we totally should just throw every automatic or semi-automatic verification technique.

C

We have at this thing, because only interesting stuff can happen when we do that, all right.

A

Good, so thanks again for a very nice presentation.