Rust Programming Language Rust Verification Workshop 2021, 11 May 2021

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: Verifying that Rust programs don't crash

Description

Herman Venter

A

I'm at facebook um in a novi group which is like the blockchain financial uh crowd and uh you know, sort of like a little little tiny little research group there um and I'm going to talk about how to verify that dress programs, don't crash.

A

um So let's first talk about um why we have um work going on under application, and I think that I guess it's kind of obvious to everybody here, but um so here's a pretty recent quote from a paper that, if you guys haven't seen yet you really should read that it's a kind of a very well written paper and as if I could affect my views very precisely so uh thanks aleister for being so very eloquent about what I feel about verification.

A

So uh this is a very recent quote, but um going back three years ago to the start of the mirai project, um things were not very different. So basically, there was a team of people who decided on the programming language to use to implement the blockchain thing dm and they ended up choosing rust. But they came to the conclusion that rust was great everywhere, except in static analysis. It just didn't, compare well to other languages, particularly to cnc, plus plus, and all the tools available for that, and so they reached out to me.

A

While I was um sitting in hawaii at exactly this exact spot, where my background is um and said, how do would I like to come and work on static analysis for rust, and I said: yeah? Yes, okay I'll, do that.

A

So that's the origin of the rust project um going back almost three years now, I've only been working on for maybe two and a half, um but it's uh started to be a fairly long, undertooth project already and uh still feels like it feels like fusion like it's always going to be another year, and then it will be great, so not quite there yet, but okay. So uh meanwhile, what else is there um that russ broker can can use?

A

So it turns out that the rust type system is a wondrous thing and the fact that the rust standard library has a functional library and the whole rust ecosystem, the rust way of doing things and clippy, and all that stuff means that when you're writing rice code you're not really writing a lot of um the classical bugs and kind of stuff that you see in c plus plus.

A

So it's not this of like huge bug, fest that static analyzers for c can have. So, if you want to view static, analyzer um writer c is kind of like your best case like it's like it's just like a like. There are gold nuggets lying everywhere. If I, if every 10 lines of c there's about 15 bugs or something like that, um rust is not like that. So rust is really much more difficult place of doing business, but even so, rust programs can still terminate abruptly and disgracefully so.

A

um Hence this workshop and everything we're going to talk about in this workshop.

A

And so, let's get to what what mirai? What why me write today, in fact, today's view of mirai is that we want to produce. You know one of these compiler plugins that nichols has been telling us about so so they could fit smoothly into cargo, and we want to very specifically ingest arbitrary and annotate across code, so just meet the programmers where they are take rust code, as it is all of it no exceptions and produce actionable diagnostics for very low, fast positive rate.

A

We want this to run so quickly and efficiently that you can just make it part of your normal workflow and also should be part of ci, and there should be no.

A

There should be no barriers to use of this thing, so um I guess, as all of you can imagine, this is maybe a little bit over ambitious, uh there's still nowhere close to doing all of this, but that's kind of our goal so um also, I guess, if um I'm gonna say that uh if I, if we can do this without um solving any um any new novel problems or making research contributions, that's actually a plus point.

A

When I get to all of this done, but as as low risk and as easily as possible, so research is not really the objective here.

A

So how to use mirai? um Well you go to the github.

A

uh This is not maybe the most uh wonderful url to get there, but if you go to the github from the readme or get to some page telling you how to install mirai, which is a little bit complicated because you have to install z3 as well, but it's all there, then you just basically build your project without using me right.

A

um But there is a little caveat. You have to set this damn flag and so nikos please make that flag go away uh or somebody make that flag go away, and I will be very thankful.

A

Then you have to touch your main file or the library file. So we can do some incremental compilation. Now you run cargo again, but this time you tell it to use not rust c, but the little mirai wrapper that will invoke the callback object and do all of the right things and then you'll get. um Hopefully it doesn't crash, but sometimes it will- and you will maybe get some diagnostics that maybe some of them will be useful uh in the future.

A

um It would be so much nicer if we could just do something like cargo verify not have to do all of that double bolding and touching and flags and stuff. So uh there is really some um some more work to be done in terms of support. I think that rust has for verification.

A

Okay, so uh as as I've mentioned, we're still at least a year away from having a really uh polished, useful product, I think- and maybe a year from now I'll have to say the same thing.

A

So if you try out mirai, you really should expect it not to work, but I would like it if you try it out anyways and let me know how it goes. I only ever get negative feedback. Sometimes it's nice to hear if something went well, so if you use it and it actually worked for you, I would just love to hear that I've not so far had the pleasure of hearing that from anyone.

A

Okay, so what does mirai actually do? It's essentially just a reachability analysis, and so it does control flow reachability. So, basically, um if there is some way, starting from a starting point to flow through the program to some to a panic, it will tell you about and say: hey, do you know your program? Can panic uh if you follow this path through the program, and it also does data flow reachability.

A

So basically, um as part of the analysis, it's tracking values, and so um you get to add tags to values, and so the analysis will be able to track data as it flows from variable to variable and by expressions and you get to control exactly how it flows through expressions.

A

And then you can check whether this tag, data reaches a sync and if tag data shouldn't get there or gets there without the tag that you want, then you can give a diagnostic with a precondition.

A

There are also implicit channels, for example, timing channels that people are concerned about for security analysis.

A

So you can also there's also an option to say that, if tagged, data flows into any kind of condition that is used to control control flow, that you can call that an error so that you can do things like constant time analysis. So, if you have say crypto algorithms, where they don't want the runtime of the crypto algorithm to be influenced by the secret key in any way, you can build a check using this data flow analysis. Reachability analysis.

A

So basically, uh data control, flow, reachability and data flow analysis and data flow reachability is just very primitive um basic forms of analysis, so uh you can do all sorts of other things like code injection, leaking of secrets, and you can basically build whatever analysis that you are truly that you're actually.

B

A

To do or that's interesting for your particular thing by building on top of this basic analysis and typically, you would then need to start making use of annotations and custom tags and there's a great in create supplier called mirai annotations.

A

It has a whole bunch of macros, of which these are the, um in fact, the principal ones that you can put into your program to sort of like build up custom analysis, if that's what you're trying to do so. Basically, we all know about pre and post conditions verify it's kind of like a cert.

A

You can also help the approver by adding assumptions, and then you can do uh control data flow analysis with add tag and hashtag, and you can also uh model, do have moral state by setting model fields and looking at model things.

A

A

So I said that we want to make mirai work as as well as possible for arbitrary unannotated risk code and keep false positives down to a bare minimum.

A

So since we are reporting every time, there's a panic or you can reach a panic well, most panics and rust programs, and what these the ones I've been looking at are intentional checks that parents parameter values are saying, so you don't want to point out to a programmer. Hey you've checked your parameter for validity, because that's not really going to get you a lot of love from the people using it too.

A

So um also, these checks um sometimes are just implicit. um A programmer will just put in an index into some array and say: okay, it's don't call me of a bad index or don't call me with um it'll unwrap a value, an optional value and say: don't call me with something that is not unwrappable.

A

So a lot of these checks are implicit and pretty far away from the public api function.

A

So if you want to do things really properly, you will annotate the public api function with explicit preconditions that will make sure that no panics can actually happen once you pass the preconditions but- um and this is kind of like how I always thought things should be done because it has and it adds nice documentation and so on, and it's very explicit what's trying to do, but uh in practice at least the rus programmers that I've been working with, um find all of this annotations to be very redundant and verbose, and they push back against us.

A

So in the spirit of meeting programmers where they are.

A

Basically, we want the analysis to.

A

Infer preconditions that will preclude these panics so instead of issuing a diagnostic when you find that there's a path leading to a panic, if it's possible, you want to just produce a precondition that precludes the panic and so by inferring these preconditions and just adding them to summaries of the function that you analyze.

A

You will not produce any diagnostics for that. Let me just make um adjustment to my screen.

A

So I can find my cursor. I can't read my speaker notes because it's blocked by my.

A

Little pictures, but okay, I can't find my cursor um okay, so um the other part of keeping false positives down is to make the analysis as precise as possible um and as general as possible. So it's basically not a modular analysis like um against, like what I was used to with microsoft. Research were always the religion was you do modular analysis because the only way to scale and be fast and step up, so uh the analysis is to be precise.

A

Is it starts at an entry point and from there on, you want to basically traverse the call graph and you want to resolve every function, call so that you can get a precise summary of its behavior and which you can then specify specialize at the call side.

A

Information such as the actual arguments, so resolving functions is not always possible, but it turns out that we can do it often enough, so that when we start from an entry point and we just carry down the core graph, most functions can be resolved and the analysis can be useful.

A

So that constrains what can be an entry point? So basically, an entry point is, can be the main function of a binary or it can be a public function of a library, but it has to be non-generic and it must be first order because analyzing a function that has um parameters that are maybe traits for which you can call or as function first or higher order. So you have function parameters. If you don't know what those functions are. You can't resolve the calls to those functions.

A

You don't know what the summaries are and then the analysis basically breaks down another potentially good place. To start an analysis is human tests.

A

So um I think one of the um the ways that we really need to go with static analysis for um for rust is to really um start with unit tests and essentially use the symbolic reasoning, capabilities to uh traverse not just the specific values in the unit tests, but like the entire value of space and all of the paths through it.

A

Okay, so let's see so, we start with an entry point, reverse down it and we get to a function called the function summarized on demand um and then the summary is cached. If we don't cache the summaries we'll end up in exponential explosions of runtime or the analysis of real programs that become infeasible.

A

But don't summarize a function just once uh particularly the generic functions, it's like a concretization compiler make up a key of the concrete types, the actual arguments, the function pointers are reachable from parameters, concrete types of any trade fields, reachable from parameters and so on, and then summarize, the function being able to hopefully resolve all function, calls and then.

A

For future users, we see this kind of invocation again.

A

Nevertheless, there are still some function, calls that do not resolve for various reasons, and there are also a lot of function, calls um that you reach this way that actually have no mirror. um Some of them is inevitable, because those are foreign function, causes to uh rapid, c, plus plus functions or to intrinsics um in other cases.

A

It's because we're calling something in the standard library and the dear uh rus compiler writers, in their infinite wisdom, have decided that quite a few of the functions of the standard library will be stored in the libraries without near.

A

So uh we do get in practice to a lot of functions where there is now there.

A

So um there are ways in the um analyzer to there are ways to write summaries for these functions by hand and the analyzer is: um let's go to the next slide for that, so the um analyzer is bundled with a bunch of built-in functions for some of the intrinsics and foreign functions that we know about, and programmers are also able to add their own handwritten summaries format form functions that they call, but um in practice the analysis will still uh quite often get to a function for which there's no mirror and no summary and then basically all bits are off, and now the question is what to do um so.

A

This fun, this unknown function could panic. It could have pre-conditions, so it could even call back to the code via a function parameter.

A

um It can have all sorts of side effects and it can have established post conditions that we would like to use, and so uh all of these, the lack of knowledge about all of these things basically means that when you get to a function that you couldn't resolve, you're kind of in a very bad state for the analysis.

A

And there's not really a lot that the programmers that want to run mirai on their code can do about this. Because it's you kind of reach this point in some third-party library or standard library or in some situation, where it's very far removed from the code that is being analyzed and so.

A

What we want to do is.

A

Not just say: okay, uh hey, there's a problem here, uh tough um we'd like to carry on with the analysis as far as possible and reduce false positives. So basically, the technique that I've settled on is, if you look at the path condition to the function, call. So if it's possible for the caller of the function to avoid calling this missing function at all, then um they shouldn't be bothered for diagnostics.

A

So, basically we promote the path condition of such function, calls into preconditions and then, if at the call site, it turns out that that path um that contains the front functions never actually called, then they won't be a diagnostic for it and you're not overloading the programmer with a message that they really care about and can't do anything about.

A

Okay, so I think I've talked about this, so one um case that I often see with um functions that are missing, but don't matter is um if you call a function with an argument that is some kind of trait, uh but it's actually an optional uh value and you're calling it with none.

A

Then, uh at the call site you haven't specified what the type of t is, and so you can't um analyze the function with a known type for that traits. So when you analyze the function, you'll get to that trait call for the sum case and that's not resolvable, and now you would normally give a diagnostic, but by making it into a precondition.

A

Because if I go back to the call site you see, oh the call side actually supplies none. So it turns out that the precondition which in this case is that the function should not be sum is honored by the fact that the actual argument is none and you can then suppress that you don't need a false positive in terms of you may be calling this unknown function because it never actually does get called from that call site.

A

Okay, so um coming to uh just a little a few words about the internals of mirai okay, so we all know what mir is so. uh The ai part of mirai stands for abstract interpretation and it is fair to call me ryan, abstract interpreter, but that's not the whole story.

A

uh The abstract interpreters instantiates it with a domain that actually tracks symbolic expressions rather than the more classical uh ways of doing abstract transportation. So it's also fair to call mirai symbolic execution engine, but there's more one of the things to notice that symbolic expressions have this habit of growing exponentially in size.

A

So um there's extensive support within mirai for constant folding that algebraic simplification. While it is running this interpretation phase, but when we get to an actual proof obligation when our decision has to be made about whether a code block with a panic is reachable or not, then the residual path condition if it is not a constant because of constant folding simplification at this point is actually translated into an expression for an smt solver.

A

So you can also think of mirai as being a more classical smt solver based theorem proving kind of system. So it's kind of like a hybrid of all of these things.

A

um The interpreter works by tracking the values of variables, fields by means of a functional map of path, value pairs, mere terms paths are essentially places and values are essentially operands and it uses a functional map so that we can basically keep lots of copies of these things from various program points. As we do the fixed point, computations.

A

And the values in this data structure is basically just containers for the symbolic expressions, but when a symbolic expression gets too large, it gets wider and then we compute additional abstract values such as intervals, and we also do this during symbolic algebraic simplifications.

A

And this is very heuristic bottom up and shallow, so it's kind of effective and most path values are really concrete, rather than abstracts, but apps when they do become extract. We do have to worry about adhd, so there's a lot of complexity around updating the environment in such a way that we take care of aliasing.

A

Okay, then there's also a bunch of k limits that limit things from getting too big, particularly the symbolic expression, so that the analysis will not diverge uh in the future. Okay, I want to do more formal work, so uh supporting parameterizing the tests.

A

It will also be nice if we can take the models from the smt, solver and synthesize counter examples, um and then we are saying that there's a for some test case when we find that there's a panic that might be reachable back to make it really easy for people to use miui in their project by simply making publishing github action uh like to have human readable function summaries and they have much better id integration at some point. So these are all things that hopefully will happen in the future.

A

uh Okay, so for all of you out, there um help want it. um I know uh most people are working on russ verification at moment. They've got their own private infrastructures that have been working on for decades and rust is just like another feather in their cap and.

A

That's the right thing to do, particularly when you come at it from a research perspective, but once you get an interesting result, maybe consider porting.

A

That into mira certainly will be very happy for you to try and do that and give you all the help I can, uh and even just using mirai on your own code will also be very helpful, and uh uh the other thing that I think all of us will benefit from enormous is if we can come up with a common set of test cases or benchmarks that are all uh verification tools can run against uh I'm keeping this workshop going and um um having more of them in the future.

A

I think it's also a good thing to do so. It's kind of like all, I have to say um running a little bit over them.

B

Yeah we're a little over. I don't. I don't want to take any questions, but there was one question in the chat that maybe I'll throw at you and then we'll go to the next.

A

B

And then we can follow later. It says daniel schwartz narbonne asked: how do you handle the standard library? Do you use a model or the concrete code? A concrete.

A

Code and then models for all of the stuff where the rust compiler devs have been had decided.

B

A

Me beer, yes, which please please please fix that.

C

Just to avoid one brick comment here: miri not to be confused with mirai has also needs mirror for everything, and we have some pretty good ways to do that so uh happy to talk. If you want to know more about what we are doing, I would.

A

C

B

Yeah, that sounds like a useful follow-on item um all right. So if you can end your screen, share herman will move to the next talk.