So, thanks Udo for the kind introduction, and I'm thrilled to be here.
This is my first, first demo.
My usual community is formal verification, formal specification and verification.
So today, I'm going to give you a high level overview of the formal specification and
verification of the NOVA and Michael Hypervisor that we, the formal metal, formal metal team
at blue rock security is doing.
So, what we are building at blue rock now is a virtualization start with NOVA at a bottom running
in Hypervisor privilege, and then we have give you a high level overview of how we perform
modular, formal specification and verification of NOVA, Michael Hypervisor within the whole stack.
And so, if you are not familiar with formal specification and verification, at a high level,
the idea is just to state the properties and verify the properties, meaning doing proof
in a very rigorous logic.
This is allow us to, and forks us to actually think about all of the properties of our components
in a most ambiguous way, most implicit way, a more thorough way, and with the result is that
we have much greater confidence on our proven properties than just simple testing and even
stronger than just running static analyzers.
Now, it may be obvious now that this requires a lot of effort, and obviously what we really
want is that we want to do this incrementally, and the keyword here is modularity in a way
that we want to be able to specify and verify components in a more or less independent way,
and then we can compose the results to get the specification and the verification result for bigger
systems. And in this talk, I will give you a quick overview of the techniques, which is separation
logic, a very recent development in the formal verification research that we apply in order
to achieve modularity. And last but not least, in order to scale our specification and verification
to bigger system, we want to be able to perform these proofs in a more automatic way, and one of the
most important thing, and the modern standard of formal applications is doing this in a proof
assistant where our tens of thousand lines are proof, check algorithmically, and what we're using
is the expressive type system of the proof assistant. And on top of that, we also want to
reduce the effort or even when if you're familiar with horror logic from university, the specification
in horror logic is often given as a triple where you have the pre-condition, the program itself,
and the post-condition, and the triple is just simply saying that the program update, the pre-condition
state to the post-condition state. And in this case, it's doing that sequentially. And in this version
of separation logic, the pre and the post-condition mentions what we call a small proof-print
points to assertions, which only talk about the fragment of a state that our piece of code
care about. So for example, what we're showing is that in the pre-condition of updating a
capability, we only need the points to assertion of the selector that's our ownership of that
capability. For example, if we just running cap update on one single entry in the capability page
table, then the specification of that functions, we just mentioned that particular entry and nothing else.
And for that, we can specify and verify cap update in cap really date each function in isolation
and when we need to compose them, for example, here we have a thread, two threads running
these two function in parallel. And if we happen to know that, well, this is actually
cell one, sorry. The cap update is working on cell one and cap update is working on selector
two. And we happen to know that these two are the joint in the capability table. This is
encoded as the separating the junction a star in separation logic and basically say that these two
are the joint resources. Then we can simply compose the specification that we have up here
without understanding the implementation of this function to get the help proof of the composition
and basically the proof here to saying that small complicated and say a resources are very
common. So we have to go to more stay up here at logical construct in modern separation logic
in order to be able to encode and to specify and verify this concurrently access share resources.
And in a way, you can see this is actually a separation because it's a separation in time
where everyone would in only one moment in time access one particular resources.
And for that, we go to more advanced features of separation logic and that was called concurrent
separation logic and you probably familiar with the very basic form of concurrency where
excessive concurrency resources are protected by lock. So this is, for example, if you happen to have
through threatening, update in capital A now on the same selector, you want to be able to
to distinguish separate them so that one does not interfere with each other, you can put the
lock to protect the selector and this come up very naturally in separation logic by just saying
that, okay, now the lock protects the tiny little bit of resources, the capability table entry
and whoever acquired lock will get access to that, sequentially, and can do whatever they want with them
and when it release the lock, they have to return that. This is very natural and
very basic also concurrency separation logic. Yeah, and then, but you don't really want to use
lock based concurrency, but what we have seen is that in highly concurrency code, we want
five grand concurrency where access to the resources are atomic. And in this case, if we happen to
have an implementation, I've kept very long and kept update to just using atomic to
access the resources, then we need a word to specify this highly concurrency behavior
of operation. And more importantly, you can now chain up this atomic update to be able to specify
multiple linearization points. It happens that your function doesn't have one single atomic effect,
but it's hadn't had multiple atomic effects, multiple linearization point. And so, we will jump to
an example directly in Nova and this is a bit blurry. This is the specification, the documentation
of Nova, and this is just screenshotting the page about control and semaphore. And you don't need
to read it as blurry anyway, but at the first step, you can think of it in a more form of way
that this is basically the visibly atomic effects of semaphore control up and semaphore control
down in which the effect is something up. There will be a linearization point an atomic effect
that check the capability, this will require you to use the capability of the semaphore.
And then there will be an atomic effect of actually bumping the counter of the semaphore. And on
now, you have also a capability check and then several other points. One of this is that the
now actually happened to because the execution context is blocked waiting for the semaphore.
And then it can happen that as a simulator, it's either it's unblocked. So, definitely an acquired
semaphore or it just simply time out. So, this is one important point here is that these
points are the linearization points so it can happen concurrently. And so it can be the case that
some other operation running concurrently can just happen to update the capability. But the
semaphore, the rest of the behavior is still going on as long as here we have the permission.
We have the capability to perform the operation. And one other important point is that if you look
at the documentation, it's just say okay in what cases in the behavior will be that you get
some error code. But without specifying the exact order of these operations. But in order to
specify these more formally, we have to create have to see and specify the order between these
to the realization points. And so, in order to specify the semaphore, we have to think about
what are the resources of a control semaphore care about in this operation. And what I
from listed here is basically it's just briefing. You need the capability to store the permission
to access the semaphore. And then you need the counter value of the semaphore and potentially
the list of block execution contacts waiting for the semaphore. And we just simply introduce
though free or not simply we have to prove that we can do that in the interface of separation logic
for NOVA. And with that we can use the idea of logical atomic updates to specify the behavior.
And this is just pretty easy to read. I'm hoping this is easy to read. And it's basically just
saying okay there's read up the cover really up a selector. And then you check if that one
have the right permission to perform enough. And if that happened, then it will be the case that
the counter value will be updated. Otherwise you get that capability. And the Q here is a logic
assertion that is picked by the client or specification to specify what exactly will happen
after the call up the control semaphore. And now there is also very similar. You can see that at
each linearization point we use an atomic update to specify the pre-inport condition of what
happened. You certainly again have to check the capability. And then if it happened, then the state
the list of block AC will be appended with the current AC. And then sometime later it will be
unblock because you have a hammer out or it will be actually decremented. The counter will be
recremented because somebody unblock it. And so we actually acquired the semaphore. And one
important point here is that we use a classical conjunction to specify the possibilities that
the client have to deal with. And in this case both cases can happen and so the client should be able
to deal with either a semaphore or a timeout happen. And just to summary to summarize this idea,
the simple idea is to use separation of repot the arrows. And so in a way the entrances client
cannot crash nobody. Okay, so I quickly show you how this the verification of some controls
and before down works. And this is the code, the implementation, the current implementation of
Nova. And what happens here is that this is the internal C++ code. And we have our own internal resources
stated on some institutional logic to specify the behavior of the C++ structure or data in this
case. And this is fairly complicated but we look really we have strong proof automation for C++.
And this can be blast through mostly before we just have to manually write these pre-imposed condition.
Again, this is you can see here that there's a lock. And so this is happening sequentially.
But on the other side, you can see that when we're doing this proof, we will have to be able
to certify the interface, the specification using atomic updates. And I'm just showing you that
where these atomic updates will happen. And they happen in connection with the internal data
to the internal states or those in separation logic. For example, here the updates are actually
downing the counter, acquiring the resource, happen at the pawns where the count is decremented.
And in the case, that's the normal case. So that actually happens is that the execution
can't technically block waiting for the semaphore. And in one of the case, it will set a time out.
And when the time out happen, which is in another implementation, not exactly in the call out
control valve, we will commit the rest of the case in the specification. And this is if you're familiar,
this is called an external linearization pawns. And this can be handled easily with atomic updates.
In a case where you suddenly got unblocked here, then your unblocked is actually done with the
help of another control and up semaphore. And so the update is happening inside the up. And this is
also a notion of helping in a linearization. And this is so easily handled. And with that,
I'm just showing this specification. This is a fairly complex protocol, but
doing formal applications just mean that we have to stay this explicitly and have to check on
the case on the case explicitly. And we were able to specify the behavior of Nova and just to
move up one level of abstraction, which is the then the behavior of the whole VCPU running on top of Nova.
This combination of a user semantics, where the kernel semantics is replaced by
humans, then just simple testing or setting analyzes. But that's also a lot of efforts.
But luckily we have reached a pawn where we have a lot of tools to be able to have modularity
in our process and also a lot of automation in the process to reduce their efforts.