Rust Programming Language Rust Verification Workshop 2021, 11 May 2021

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: Rustv: Semi-automatic Verification of Unsafe Rust Programs

Description

Yulu Pan and Yuichi Nishiwaki

A

So the second talk was uh proposed by judo pan and yuichi nishiwaki. They are both students at the university of tokyo and so yulo is here today, and I think he will give the presentation about formalizing the rust semantics in isabel hall. Yes, so you please go ahead.

B

And share your screen and start okay.

B

So, can you see the window.

A

B

And is a pointer available? Can you.

A

B

Yes, okay, nice, so hello, I'm yuru from the university of tokyo, so here in japan, it's midnight. So probably I maybe I looks sleepy so in this talk. We introduced our project called last play semi-autumn verification of ancillary programs.

B

So here is a summary of work, so our ultimate goal is a formal reaction method applicable to production code. Yes, it is sounds very ambitious, so we developed a deductive verification framework for unsafe last using isabelle and simple. This is a serum improver and simply the framework formalized in isabel.

B

So this project is pretty much working progress mode, but we prove and disproves the safety and correctness property for some very small and serious programs using our frameworks. So here is a label of the the europe of the ripple. So you can see the formalization artifact here. So this is our trend of the talk. First, we overview the background and approach we took next. We see some technical details that explains how we model us in isabel.

B

Then we introduce an example where we verify the safety condition for beta soft function is correct, so in uh using our special using our framework. Next, we briefly talk about the verification effort for some other small answer functions. We have verified a mobile. We show some an interesting example where we found that formalizing the safety condition can be tricky due to stuff procedures.

B

Finally, we talk about some observations and feature work, so, let's see the overview so currently, when we listen about the safety of unsafe last programs, so we have a very nice culture where we usually write these safety sections when defined as functions and safety comments when calling assay functions so that we can be sure that the safety are actually made. However, the listening is down in our head, so we make many mistakes, and here we have this list of several vulnerabilities.

B

So therefore we like to have a formal rescue missile for safety and functional quickness for unsafe last programs to gain more reliability. Moreover, the muscles should be able to listen about low-level memory model of unsafe loss and we want the verification effort to be a minimal. So this course looks very quite changing, but we can look back on history of research like last designer already did and we can stand on the shoulder of giants. So in this project the name of the change is called the cell 4.

B

The cellphone is a formally verified industrial level kernel written in c, so they achieved the formulation of functional greatness of more than 10 000 lines of low level c implementation.

B

To help this work, they have developed several powerful automation tools. So here is the artific architecture of sorry. Here is architecture of the city for verification they use the ceremony approval called isabel hall for the verification. So first they write down the formal spec of their carne in izabel hall.

B

Then they automatically translated their c implementation to isabel using a framework called simple, which we talked later. They also introduced some high level representations of programs for the ease of the verification.

B

So finally they proved that this representation implements a spec concluding that this c called satisfy the spec. So the sample project successfully, this verification works. So we saw that this approach can be adapted to last. So in this approach we translate the last program to israel instead of c. So currently we are missing this high-level representation on automated translator, so in current setting we need to manually translate last program, so sim is avail and we are writing direct proof against the formal specification of the function and not a representation of the last implementation.

B

Now so, let's see how the this last example translation works. So we adopt this simple framework, which is um imperative. Programming languages for magazine in isabel hall are used in the safer project. It comes with impressive control flows and generic space and quality for verification.

B

What is interesting is that this simple frame, work on its whole logic, are parameterized by this set space. So once we can encode last memory model into this, like simple state space, we can leverage simple infrastructure such as holologic for verification of unsafe flash programs. So we briefly show how we encode last memory model into simple.

B

First, we represented the global heap memory as a pair of bias and exo stacks following the last stacked force areas in model. So in this definition, this memory path corresponds to the content of the memory at each location and this tags part tracks byte references using different styles. So this left kind means that permission given to this set of tags and they form a stack to deal with reporting.

B

Then for each function to be verified, we define a set space for that function and we and this this state space is used for verifying last programs using simple. So, for example, I mean the function. Csps is defined. A pair of global heap and variables, for example, uh swap function in the standard. Library takes two arguments x and y, and it has local variable name temps.

B

So the space for soft function consists of the global heap and these variables in our formalization local variables and arguments are represented using differences to global heap so, for example, x and y main areas.

B

So let's see an example of verification, so here we want to verify that the safety conditions on the pointer swap function in the. So I mean I'm sorry, so we would like to verify that safety condition of point as well function written in the standard library, dogs are actually sufficient to be safe. To call the point of swap so so to verify this, we first translate the implementation point of function into simple.

B

Then we formalize the safety conditions of the function is in isabel. Finally, we write a proof of safety, so, for example, this is a translation from the implementation pointers up in last into simple.

B

So this is a simple, simplified implementation point as a function in last, so it first allocates a temporary memory space and copy x to temporary and y to x and temperature y. So we can translate this last program into isabel hall like this. So this is a kind of literal translation.

B

We allocate a temporary space for temp, then copy exit, temp invited x and them to y.

B

So next we formalize the safety condition in the documentation, so the standard private documentation says that two pointers x and y must be bright, for both leads and lines and x and y must be properly aligned. Since we do not formalize alignment, yet we focus on this variety part.

B

The formalized safety condition statements using the horizon in our framework, so.

B

In this whole triple so, the precondition corresponds to the safety conditions. So this part waveform heap s, means that no undefined behavior occurs so far, and this writable x and writable y means corresponds to the validity in the uh standard documentation.

B

Moreover, in this example, we only care the case where the two pointers are not areas each other, because it's easier to verify, and this non-areas in assumption comes here.

B

So the area case I explained later so- the verification of the safety is mostly automatic. We learn the verification, condition generator of simple and simplifier of isabelle, so they give up remaining beneficial conditions, but we can invoke sledgehammer 2, which is a very powerful proof, search to provided by isabel- and this is summer to conclude the proof with this lemma in this case, so we can prove the safety of a function like this.

B

So next we talk about the result of our formalization, so this table shows the scale of the effort required to verify some very small, unsafe loss functions such as cell missiles, like guess so, the lines of code for verifying the safety and functional correctness of this.

B

uh These functions are very minimal, but we observe that proof checking time can easily blow up. So, actually, our framework is not very scalable in its current state, so over the areas in case so where two, the arguments of the pointers up are area, same requests, a bit more verification work, and during this verification we found an interesting example where formalizing safety condition can be tricky, so consider these two programs.

B

So both programs creates two low pointers to x named p1 and p2, and we pass these two pointers to point our soft function.

B

On the left hand, side p2 is directly varying from p1. However, on the right hand, side there is a mutable difference supplying p1 and p2.

B

Indeed, under the stack both rules, the left one lands safely, while the right one exhibits an undefined behavior when calling point as well, so to explain why there is this difference, we assume the understanding of suck o. So please feel free to ignore this slide. If you don't know much about success, so, basically, on the left hand, side since p2 are directly revolved from p1, p1 and p2 share the same partition to access x, so in other words, p1 and p2 are simultaneously byte differences.

B

While, on the right hand, side there is a uh there, is a mutable differences spreading p1 and p2, so under the stack both used when we use p1 in the implementation of pointer swap, it invalidates p2, so in other words, p1 and p2 are not similar dc varied. And, finally, this pointer sub code leads to an undefined behavior.

B

So the point of this example is that this distinction is not clear from the safety section of point of documentation. It just say the both x and y must be valid, but uh it doesn't say it's the point, that's up by inverse sense so and actually, when we try to improve safety of the left hand, side and the unsafety of the right-hand side. The reasoning is much more complex due to aliasing.

B

So here is some observations of our thing we found in our work, so we found that modern last using isabelle, simple, is capable, actually switch hammer, which is a proof such tool provided by isabel, is very painful for proving the property of, like suppose or verifying programs.

B

However, our formerization suffers from longest proof checking time, and actually we observed some exponential block up of verification conditions, so it's not scalable. Now, moreover, we found that formalizing safety conditions can be tricky, as shown in the previous slides, especially under stockpiles loose. So I opened the issue at last long last repository about how to document pointers of safety conditions. So if you have any idea, please go ahead so also future work.

B

To be honest, uh formalization only supports primitive types, such as integers and differences, so we don't have aggregate types of like structs in absolute arrays and we don't have loose and function codes and we like to support this stem.

B

Moreover, we are currently manually translating last programs into simple, so we'd like to to automate this process. um Moreover, we like to have some high-level representations of implementations so that the verification effort can be reduced.

B

So, thank you for listening. You have any questions.

A

Thank you very much. We we do have time for questions. um Maybe florian. Can I encourage you to answer to ask the question via audio that you just put into the chat? I think it would be an interesting one to discuss.

C

uh Yes, certainly um yeah. I just wanted to ask whether you thought about moving from simple to imperative fall. It's also a very nice imperative framework for isabel, which also has some nice refinement capabilities. Yeah. There was also a best paper award nominate nomination.

C

This year's hit ups conference so yeah. I think it could maybe probably help you in some of the points you mentioned earlier.

B

B

I have of the isabel and pm.

B

So on this oh cute, but I think, uh if I understand correctly, space logic used by them does not directly support stack for us, so we so it is one of the reason we use our very primitive path. Formalization.

B

This is that's a question.

C

Yes thanks: I didn't uh really look into whether stick borrows would work with it, so that makes sense that this is very yeah unfortunate, missing feature.

B

A

So leonard gay, I asked the question: what does your spec for cell look like? Do you model lifetimes.

B

uh We did in one lifetimes it it just say, given the share difference to sell.

B

So I mean the spec of sales says like given the share reference to cell we can set by or we can leave from the cell and the barrier is correct. So the statement is pretty simple and the validity of differences are tracked by such posters.

B

Let us answer your question.

B

It wasn't my question. I just.

A

Read it from the tree today, okay, it did answer the question. Thank you. um So I'm wondering did you do anything to validate your semantics to see whether you really faithfully captured the rust semantics in your formalization.

B

uh I'm I'm saying, can you speak a little more sorry or write tongue in the comments.

A

No, I I was wondering whether what you did in order to validate the semantics so that you really make sure that the formalization reflects the actual rust.

B

Semantics, I see so.

B

I have some smoke tests that testing whether or formalization you reproduce some stuck most lures, but actually we don't have not much this set so.

A

Okay sure fair enough, so let's conclude the discussion here thanks again yulo that was very interesting.