Rust Programming Language PDXRust, 7 Oct 2016

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: PDXRust October 2016: RustProof

Description

PDXRust: PSU Capstone team shares progress on static analysis using MIR

More on http://www.meetup.com/PDXRust/events/234601233/

Help us caption & translate this video!

http://amara.org/v/2Fi3/

A

Okay, so welcome to rest proof: team from the Portland State capstone project, hello,.

B

Everyone I.

C

Am extremely excited to be here tonight. This is a this is exciting. All right. All right, I'll stay over here, all right, so uh hello, everyone, my name, is Bradley Rasmussen. Some folks know Mia's badger. This is a Matthew silken and Michael Salter. We are part of the breast proof, capstone team, oh.

A

C

Come over here, tada, so.

D

C

Ended up building a verification condition generator in the rust language and if you don't know what a verification condition generator is, don't worry, we barely know but yeah.

D

C

Will explain it shortly because it is it's pretty exciting, we're ahead, we're very proud of it. So as you, if you don't know, we are from the Portland State University as part of the capstone project.

C

If you would like to sponsor a project, there will be details at the end of the slides on how to how to inspire a great idea with with some with some college students that are all sorts of enthusiastic all right. So let me preface this: we are enthusiastic students. We are not experts, so I'm not I admire.

B

C

Means an excerpt of a formal verification and I apologize, but some of the some of the things in here are really quite cool. The project we built is strictly a concept in most part, because everything that we built was built on unstable breasts and actually at the end of our capstone project, are we had to refer some of our tended to a outdated version of the night ways in order to get it to work? It's still in that state currently and maybe someday one day, we will little fixin updated to something newer, but yeah.

C

Despite all of this, we believe that what we built has value like there's formal verification, is pretty important more on that later so I'm going to talk to you guys today about why ye formal verification is and why I would like to see it used more often in industry and a little bit about the reasons why we don't currently and so I suppose many of us already know right we'll see um and then we're going to talk about the theory and I do apologize.

C

It's going to get it's going to get a little, there's there's a lot of theory, but we have to explain it in order to explain what we did and then we will finally talk about rust, proof and the problems that we encountered when building it. So some of the problems with formal verification, it is very tedious and slow it.

C

It's a it's a long, arduous process of learning like how how to write mathematical proofs, it's it's! That's it! It's a long process process and formal verification is it has benefits? Sure you can you can you can make promises about your code, but it's really. No, it's not a replacement for good testing. You! You will never use a formal verification to outright just will never test again, we'll just do it all with with formal methods and we'll call it good know.

C

Any tests tests are great tests or fast, and they they cover enough to make sure that your code is good, but formal verification for those cases where you want to know for absolute certainty that it will always work the way that you intend it to you. So in the process of.

A

Building rust-proof, we.

C

We kind of analyze some of the some of the things that we encountered.

C

For example, a a while back I was enamored with this. This project called SEL, for which is a it's a microkernel written in C, it's about 7500 lines of c code, and it's in that respect, I suppose very simple. But it's it's a formally proven microkernel and so the developers of SEO for in order to verify that the code of the SEL for microkernel was correct, had to write two hundred thousand lines of Isabel code to verify it.

C

As you can see, maybe that's a little problematic and can really put a damper on you're your software engineering process.

C

Many many of us here by a familiar potentially with Haskell at least briefly. We all know of it as thats a little the language of it's got a little bit of ivory tower syndrome. It's it's complicated, it's hard to write in.

C

If you can write in haskell, it works great, but a lot of people don't use haskell because it's hard to use and it's hard to use in a way that rest isn't quite as hard to use and then there's tools, there's a lot of other other tools out there that, for example, from a see which is very close to the thing that we built and it's a lot more complicated.

C

It's a lot more fully featured, perhaps obviously as being a capstone project and it it's got all the bells and whistles and it formally verifies your c code.

C

But I tried, I tried to figure out how to do Franta see over the past six months, and I wasn't very successful. um So, as I mentioned before, formal verification is useful. It can give your code a degree of reliability that you can you can you can point at it and say we promise that our code has certain qualities. We promise that our code will never have an integer overflow, for example. In these particular cases yeah you can make your code. You can make your code more security.

C

You can shun start making promises about your code and really really the key to getting on with the verification used in the industry. I feel, is to automate it more and make it more accessible for everybody to use and a formal verification condition generator allows us to automate that process and make it easier and make it something that people might actually want to use.

C

So at this point I will hand off the the discussion to mr. medve slogan, who will discuss some of the theory behind everything that we did. Yeah.

D

So, there's a lot of kind of theory that goes into making this all work, and you really need to understand it before you can see why what we did is a thing and how it works. So we're going to go over briefly what logic is and what it's used for. It's just a construct. That's used to reason about programs, and so you define some precondition. P, that's basically the state of your program going into execution, and then you have some set of statements, s and then a post condition. That's true.

D

After those statements are executed, and we can see an example of that right here we give the precondition that x is less than four and then after we take that value of x and add one to it. We can say that it that value is less than 10, and so it's just purely a construct to reason about the correctness of programs, but we leveraged it to generate these weakest preconditions and the weakest precondition. It's a it's.

D

The most permissive precondition that you can come up with and it's generated by applying the statements in reverse order to the post condition and you generate a new weakest precondition. So let's look at an example of how that goes.

D

So here we've got that same example that we're familiar with, but here working backwards. We we want something new. Instead of P, we want the weakest precondition, and so we take Q, which is y, is less than 10, and then we substitute into it. Whatever is the assignments that happen inside the statement blocks s, and so in here we're going to substitute X, plus 1 for the value of y, and now we have generated a weakest precondition and we can look at this and we can see that that could replace the precondition p.

D

It would be more permissive, but no matter what happened, the postcondition q would still be fulfilled.

D

So what do we do with that week of spring condition? That's good and all to have it, but we need to use it so we construct this verification condition that is, the precondition, implies the weakest precondition.

D

So we get this, this P implies WP construct and we can use this to check for the validity of the precondition you supplied. So in this one shown at the bottom right right there, the P implies WP. We can see that when x is less than four that implies that X plus 1 is less than 10 and there's a little bit of some nuance. That's lost here, because here x, is it's bound, is bound to less than 4 there's no value that would make this false right.

D

This is a tautology, but if X wasn't bound effects could hold any value. The FX was eleven. Eleven plus one is not less than 10, and so we would have some discrepancy there, and so what we're doing with all this? We build up this, this verification condition and then we hand it off to an external theorem prover, it's an smt silver and it looks to see if there's any way that it can make this thing invalid, and if there is it reports it back to us and.

D

Oh there's one little caveat here, which is that when you actually pass it over the SMT solver, it's looking to find one way in which it can make your formula valid, and so we actually pass over the negation of the formula. So it looks for one way it can make it invalid and if it can't find those, then we've proven that what we have is its ecology and law. We get to finally talk about what we actually built.

E

Hi I'm Michael Salter, so the software we built this cult rust-proof and it's a compiler plugin and we're going to go over some of the designs, the design decisions we made and then actually follow through the program kind of step by step and what it how it works. So we're a compiler plugin, basically I mean we have to access user code.

E

The s in the theory you were looking at before those are the actual statements that you write in your code, the pre and the post, conditioner things that you know you write about because you assumedly think you know what the program I supposed to be doing. So we need to access the head and the compile already does that for us, the compiler simplifies it and it does a lot of the work like type checking and stuff. You know, if we had to do, the neurone will be a be complicated.

E

So as a compiler plugin, we need to be on the nightly build which has its own set of challenges, but we also get to cut it. The nice feature that whenever you make a change in your code, you try to recompile it. You end up running rust-proof again and formally verifying every time you make a change. So hopefully you can't break it without knowing it easily. Unless you turn it off.

E

Of course, we also ended up using Mir and after you weren't familiar because it's a mid-level intermediate representation that the compiler creates when it's compiling your code to do certain optimizations and checks we found using Mir was actually very useful, because Mir is much simpler than user code, it's more as much simpler than the high level representation that the compiler said that before basically, when you get into ma are everything is sort of like a big control flow graph? You have basic blocks, everything's, an assignment statements, very simple. It's very easy to do.

E

The weakest preconditions generation makes everything easier. So, hopefully a matter will continue be useful in the future, and so what we used to know my art pass. The compiler will call rust-proof when you decide to call your code, you have our tag in there. The first thing we do is we'll look at the pre and post conditions the user puts in will try to validate those. If those are valid in the right format, then will parse them, and then we store them internally, using a parser, Jenner where's, your generator.

B

E

Bars are you never called lollipop, let's kind of weld? Oh then we start to actually looking at the user code and traversing Mir, which is in sort of a tree structure, and we start traversing those Emily our blocks. We do a depth-first search, go all the way to the end points work our way back up, generating the weakest precondition as we go.

E

There's different rules for different things you encounter in code, but essentially it all gets lumped together in one really long, boolean expression that could evaluate to true or false, depending on the values you feed it, and then we create a verification condition, as we mentioned before, by joining the weakest preconditions and the precondition, then we use lip smt to take that verification condition and send it off to z 3, which is our sm solver of choice, and we wait to hear back from it and then eventually will report whatever those results are to the user.

E

Hopefully, if it involved we'll have a little counter example. So you can, you know, hone down your bug, hunting.

E

We had a few problems while we were designing it. Wasn't that bad, but obviously dealing with nightly and keeping that up to date was a little tricky at times, because it can move very fast in some ways and be unexpected if we're not following the blog posts.

E

Eventually, we decided to set down with a specific version just because we're getting close to our deadline didn't have to worry about upgrading Kruger, trying to design things and then test became kind of an issue. I mean obviously wanted to test to make sure our program, that's supposed to prove.

E

Other programs was doing what it was supposed to and we started off with some unit tests, but dealing with Mir became a bit of an issue, some of the objects we needed to handle ranted complicated life times and we're difficult to mock up the very complex tree structures.

E

So we mostly moved on to system testing, which also be game kind of an issue because, as a compiler plug in our program runs when someone else compiles their code and to run tests and a nice automated sweet through cargo you'd have cargo call our program to call another program to call our program and it got weird. Sometimes we made it work that we have a pretty good sweet that covers most everything now, as could be expected because the student project, we don't cover all the possible things we encounter in west CO 2 fact.

E

We cover a very small subset of those, but some of the basics. We have integer, arithmetic, bullion's, half of assertions and conditionals. You know if else statements. So as long as your code only has those things, rustproof can try to prove things about it in the future, we're looking at the loops and other stuff. The theory is pretty clear. We just have to look at how to actually implement it in a good way.

E

We have a demo right now do so you can work.

E

And this was originally made for a less technical audience, but them should be fine.

D

Let's take a look at some of the things that rough grip can prove that our programs for us we've defined a function called foo. It has one argument which is a 64 bit unsigned integer and it returns a 64 bit unsigned integer. This function takes one argument: X and returns 10 divided by X when using rescue you supply, pre and post conditions to a function like this. The precondition we've defined here is that X is equal to 5, and the post condition is that the return value is equal to 2.

D

Now, what this is saying in logic is that, given the precondition that x equals 5, the return will be too. So, let's just take a look at how that would work can convince ourselves. That's true in this function, with an input of 5 10, / 5 will yield a result of 2, so this should be true and match up with this function. Let's take a look at what rust-proof tells us about this function in this attribute.

D

So rust-proof is telling us the condition is valid and that's good. Let's take a look at what rust-proof says if we mess up the condition and say that the return should be three instead of two rust group here tells us that our verification condition is not valid. It also tells us under what condition the verification condition is not valid.

D

This is telling us that when x is equal to 5, the verification condition does not hold, because here we can see that with an input of 5 10 / 5 is 2 and not 3, as we supplied in our post condition.

D

So let's take a look at how we can change this function, to prove it for all cases of input, and not just this specific case where x equals 5, so we're going to delete this restriction that x equals 5 and we're going to allow X to hold any value on the input and for the post condition will say that return is equal to 10 /. Our argument, X.

D

Let's take a look at what Russ group has to say about this.

D

So here rust-proof is calling us that our verification condition is not valid. So that's a bad thing. That means there's some discrepancy between our code, in our verification condition. Here, rest group is saying that when x is equal to zero, we have some error in our code. So let's take a look at what that could be here. 10 is being divided by our argument.

D

X and since we know, division by zero causes undefined behavior we've identified something in this function, but we might not have noticed before so let restrict X and see what rough script says will say that X is not equal to 0 and see what Russ group has to say about that.

D

So rest group says that our verification condition is valid, so here we've proven that when X doesn't equal zero for all other cases of input, this function is valid and that's pretty cool to write a unit test that tested all these conditions. You would need a loop with 18 billion billion, iterations I.

E

Although is edifying for some of you and then uh land well, I didn't know any how to scroll in this okay, and then we just wanted to mention that the psu capture of capstone program is always looking for sponsors. Please check it out. If you have you no idea for a cool project or you're part of an organization that might one of the bank, our sponsors, Gina, sharp and Aaron tome and be any questions.

A

It's a mic just speak into it with your question. Oh.

F

Okay, better great a big event.

B

F

Type of algorithms does rust-proof utilize and what's your speed, can you meet enemy.

B

F

Is getting be very frank, can rust proof you saying Bay is in vain, because I'm working with a agency accompany who can reach a hundred, teraflops and second instructions a process can roast proof.

C

So, during the process of building rust proof, we had no limitations on performance on and in some cases we can't have limitations on performance because the tool that we use xiii being what it is, it's trying to solve a it's trying to solve the halting problem. Essentially- and there are some conditions where our code might never return from z, z, 3 or xiii I suppose specifically will never return, and this is true for for all SMT, solvers and so, though buy it by by by no means is our code at all efficient and it's yeah.

D

F

C

There anybody assigned to optimize it.

F

C

Currently, no, um it might be a think that we do in the future, because that would be. That would be better because you know this being what it is. Our current compilation times can sometimes measure in minutes, depending on how complicated how complicated the code can be.

C

So it our project is definitely it's a it's a work in progress. It needs a lot a lot of love, so yeah poll requests are absolutely welcome. um Yeah, so.

G

Less a question more of a comment: if this project had preceded the flight controller project by like two years, it would have been greatly useful when we were writing our our flight controller. It's definitely the kind of thing that we would have used if it was available. Rust is, of course, a new language, and things still need to be built for it, but that, like operating systems, all those things would be would be really really useful to have. I have.

D

A comment about your earlier question: the algorithm that we're using is basically that weakest preconditions generation stuff and that that's really quick. We just examined all the basic block structure that you have in your code and since we're not dealing with loops or anything, we can't get caught in a loop trying to figure out what the invariant is or something like that. So none of the actual slowness of the program is really related to our code. It's pretty much all on xiii-2 return when it wants a.

F

Topic systems are Pam valet and with best proof, because it looks almost exactly like it from me sitting here, can't would rust proof be able to handle I mean apart. Guess you can put the the platform to rust proof of rust proof to their platform, because it looks the only thing that that statement didn't have was a what well, you say, handles what, if it didn't have what they call. Cece saw the condition, return, see cities, because you have that it looks exactly like those.

F

My background is extremely aviation and computers and I did something that someone told me I couldn't do they said. Well, you can't write. You can't write a parser and sort online. I did a bubble sort online and I grow the extreme parses using the hashing algorithm with a binary having also and they kept everything down to a sub second- and the guy was amazed at that. That's nice, that's! Okay! If it measures good as long as it works, but um well that was good. Focusing on how easy would it be?

F

Do you go the direction of porting rust-proof to other platforms, all the platforms or restaurant decimal.

D

Rust-Proof will run on any tier one rust platform. Basically, anything that supports Knightley's will run rust-proof. As far as I know, we haven't tried to tested it on like arm or anything, but it passes our compile tests.

D

So that's about it. Now we don't have any plans to port it outside of roster to any other platform. That's not a tier one, Russ platform. It's.

E

Been ferment for rust programs running on ok.

A

Many other high-level questions for the group and if you have more detailed questions about afterwards, you're welcome to catch up with the team. Since we have until eight here just.

B

Wondering if there's a way to establish a universal good condition for a function, but that I mean can guarantee that none of the other functions that call this function will ever pass in zero. For example, as.

D

Far as I know, and so we haven't implemented, actual function, calls inside what we've done so far, so we haven't dealt with that, but the theory that I know behind it is that it's kind of based on the contracts surrounding the function that you're calling and the post condition of that function and that, if you set it up all right, you don't need to worry about what's happening outside. You can just worry about your own contracts on your own functions.

D

Jamie. Is that a thing good.

B

So what would you do in that case, with the function that divides by 0 if.

D

Something was trying to hand is 0 yeah.

B

D

Eat I mean you could put an assertion in right. That 0 is not allowed. You could.

B

Happen, I don't want up at runtime I wanted so.

H

Just this notion that you know, we've got a statement and you're looking at the weakest precondition for that statement, so you work backwards from what you were expecting the postcondition to be two or three conditions should be the way you handle statements that are function, calls is I.

H

You require that the postcondition declared for the function you're calling has to imply the post condition that follows the call and then the precondition the week is precondition for the function call is going to be the precondition for the function, you're, calling it's actually a little more complicated than that, but but you basically just copy the pre and post conditions from the function you're calling into the call site. Does that make sense.

B

Well, can you annotate the you.

H

Don't have time so you've annotated the function that you're calling right and then everywhere that it's called when you're checking the functions that make those function calls you just reuse, the annotations that were on the function, they're calling.

B

I'm not sure at all, but I can.

H

They sound like a conversation there later yeah.

A

Ok, any other high-level questions before we break for some hack time, I.

A

Mean let me get to the mic, so we can catch your question for the recording on the.

F

On the function calls can they be nested and if so, how many levels deep? Can you go in and give us the limitation on nesting I.

D

Would think arbitrary, yeah.

H

What about is our because you're not actually evaluating the function, calls there's not like any call stack or something where you could run out of memory. It's it's sort of flattening the the logic here.

A

Okay, thank you very much to the rust proof. Capstone group.