NOVA Microhypervisor on ARMv8-A
CC Attribution 2.0 Belgium:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Steinberg, Udo
NOVA is a modern open-source microhypervisor that can host unmodified guest operating systems next to critical host applications. Although originally developed for the x86 virtualization extensions of Intel and AMD, the internals of the microhypervisor and its external API were designed with flexibility in mind, such that the code could also be ported to other architectures. In this talk we present the first ever version of NOVA on ARMv8-A. We will show how the NOVA abstractions map onto the ARM architecture, how modern virtualization features such as GIC and SMMU are being used, discuss the ongoing evolution of the NOVA API and how the ARM port differs from the earlier x86 version. The talk will conclude with a short demo, an outlook into the NOVA roadmap and the formal verification efforts around the code base, as well as opportunities for collaboration with the NOVA community.
 The next talk is given by Udo Steindag. I'm excited about Udo because Udo hasn't been giving a talk here for many years, I think. Six, seven. Now he's back to talk about new developments in the Nova world. Yeah, I'm excited to be here too. Let's first do a little poll. Who of the audience has heard of Nova or who has worked with Nova? Maybe a quick short of hands. Okay, I think about half the folks. So today I'll be giving a talk about Nova hypervisor on ARM V8A, which is our port of Nova to the most recent ARM architecture. And since only half of you know Nova very well, the first part of the talk will go a little bit into detail about what Nova is and where we came from. Then the second part of the talk, I'll talk about virtualization on ARM V8A. ARM A is the A profile for the performance course. There's also ARM R for real-time course and ARM M. We are talking about Cortex A. And then I'll conclude the talk with the current status. We'll do a little demo here. We've already put some equipment here and then I'll talk a little bit about roadmap. So those of you who've been following the micro-commoderum today, you've seen this system which is Nova on x86 already in action when Norman gave his talk on G-node. So Nova on x86 is a system that has existed for more than 10 years. And the way that virtualization works on x86 is that without the virtualization extensions, you have two processor rings, really four of which only two are used. You have ring zero which is used by the kernel and ring three which is user mode. And you have an operating system and applications running in those two modes. With virtualization, these rings are now called guest rings, which is why we call them ring zero, G, and ring three, G. And you get the same set of rings duplicated for host mode. We have ring zero H and ring three H. So ring zero host is occupied by the Nova microhypervisor. And ring three host is occupied by what we call hyper processes. And the whole G-node framework that you saw two talks ago is a framework that runs in rings three host. It's interesting to note that the Nova microhypervisor is the only component that runs privileged. And everything else, all the colorful apps that run in the host and everything that runs in guest runs deep privileged. And there's a little footnote there that says obviously we have no control of firmware. What's also interesting to note is that we give every virtual machine its own instance of a user level virtual machine monitor, which means that should something go wrong in a virtual machine, should you have a VMscape, should an instruction not be virtualized properly or something like that, then a VMscape will only affect that VMM instance and the rest of the system will not be affected. So now we took this system and we said, can we build something like that on ARMv8? And the next slide shows what does Nova look like on an ARMv8 architecture. So at the bottom we have the hardware and then we have four privileged levels which ARM calls execution levels. So starting at the top, we have EL0 which is user mode, EL1 which is supervisor mode where kernel runs, EL2 is called hypervisor mode. This is where Nova lives. And then we have EL3 which is called monitor mode in which a firmware monitor sits that can switch between a non-secure and a secure world. And we do not own this monitor. We do not control it. And we also do not control a trusted execution environment like an opti that runs along the side. But in the world that we own, which is the top left corner, the non-secure world upwards from EL2, Nova is the only privileged component and all the other properties that we had on X86, including a virtual machine monitor, per guest VM, and the deep privileged host environment, all of that has been carried forward to ARM. Now let's talk a little bit about Nova. Nova is hypervisor, micro hypervisor that takes the best ideas from micro kernels, capability-based systems, high performance virtualization, and puts all of that together in a small piece of code where the X86 version is less than 10,000 and the ARM version currently is less than 7,000 lines of code. It is based around capabilities. What does that mean? We have a bunch of kernel objects that I've shown in the middle. We have protection domains. These are address bases. We have execution contacts. You can think of them as threads of virtual CPUs. We have portals. These are communication endpoints by which protection domains and threads inside them can communicate. And all these kernel objects cannot be referenced directly. Instead, we give every protection domain that needs to access them a capability. What is the capability? You can think of a capability as a pointer to a kernel object plus associated permissions. So procession of a capability gives you the right to invoke that capability and to access that object. And if you don't have a capability to an object, you can neither name the object nor access it. So that's a very powerful security system. SEO4 has the same and a lot of newer micro kernels do. And you can build really powerful other systems on top as Norman has demonstrated with Genome. The same principle, by the way, works for memory where you can think of a virtual address as being a capability to a physical memory page with read write execute permissions. So that same principle is also applied for Nova. So we have multiple spaces. We have an object space for these capabilities. And we have a memory space for delegation of writes to memory. In the older version, the x86 version, we used to have a mapping database that tracked all these dependencies of who gave the capability to whom and things like that. We got rid of all that. We replaced it with a new hyper call called control protection domain, which takes two capabilities, the center and the receiver protection domain. And you have a take grant model where the possession of, let's say, a capability A and a capability B for those two protection domains, you can say, take the two capabilities from slots two and three in protection domain A and put them in slots six and seven of protection domain B. And obviously, we have more than eight slots. This is just for illustrative purposes. And then the user wants to refer to a capability. They give us a select door, which is a number and index into that space and say, I want to do something with capability to this is how it works. It's like a file script. So upon this, we built some basic abstractions. And these are the basics abstractions that the Nova version on x86 has had for a long time. So on the left, you can see two protection domain. Think of them as two address spaces, two applications that want to communicate with each other. And in the production domain, A, we have a call us red and EC here and it has a scheduling context attached to it. And those of you who saw gonna talk this morning know that the scheduling context is a really nice abstraction for expressing scheduling parameters and for delegating it along a call to implement priority inheritance and Nova has had this for 10 years. And we also have on the other side a call the execution context that has no scheduling context for the very same reason that Garnet gave that you can completely account the execution. Of a server invocation to the caller. So what what would that look like the caller makes a hyper call in this case called IPC call. It gives a capability select or a selector to a portal. And what's called an empty D we call is message transfer descriptor and a message transfer descriptor tells Nova how many words to copy from the UTCB of the caller to the UTCB of the callee. So the UTCB is like a message in an outbox. It's very abstract and the same mechanism applies no matter whether you are on x86 or on arm. So once that call has been made, you know, transition over to the right side. The situation looks like this. The scheduling context has been given to the callee. This achieves priority inheritance or in case of real time bandwidth inheritance. The callee can now execute because it has a time slice. Time is accounted to the client to the caller. And at some point the callee is going to do a reply. It invokes IPC reply, gives a message transfer descriptor says how many words to a one a copy back from my UTCB to the caller. And then we are back to the left side. This is the basic mechanism by which protection domains and threats in protection domains communicate with each other. And this also illustrates how the different kernel objects sort of come into play there. So the empty D defines the number of words to copy between those two yellow UTCBs. And we'll see in the next slide how the empty D is also used for other purposes. Now I said Nova is a micro hypervisor. This means at some point we need to deal with virtual machines, with virtual CPUs, with emulating instructions and devices. So a lot of you will notice that this light looks very, very similar to the previous light. Why is that? Because we layer VM exit handling and the emulation exactly on top of IPC. So the difference is that we now have two protection domains that are called a virtual machine in which an execution context run that is a VCPU. And we have a VMM, which in this case is the server. It provides the virtual machine service and the execution context here we call it handler. So at some point the virtual CPU is going to take a VM exit on x86 or an exception on ARM, which requires the attention of the virtualization there. This VM exit takes us into Nova. Nova will save the state in a page which we call virtual machine control block because we came from x86. And then Nova is going to synthesize an IPC call on behalf of the virtual CPU, send it to the handler. And the question is now what state do we transmit? And that state is called empty D arc. And it comes out of a portal where every event has its own portal. So you can say, if I see this event, here's that state that I want. If I see some other event, here's this state that I want. And then the VMM gets this message in its UTZB. And the reply works exactly like an IPC reply, except that the handler specifies an empty D arc. The result gets stored in a VMCB. And when the VCPU resumes or erads back to the guest, that state will be restored. So empty D arc is similar to the empty D that I showed you before, which copies state around, except this time between VMCB and UTZB and not between two UTZBs. Same with the scheduling context, the entire accounting of the emulation goes onto the scheduling context of the VCPU. Now we get into ARM territory. And before we do that, I'll show you how we hide the differences between x86 and ARM. And you don't have to understand all these details. But here I've shown you the empty D, the empty D arc for ARM and x86, which is basically a bit field that describes the different fields. And these will also be listed in the NOVA interface specification. So the VMM gets to decide for every event which part of the architectural states it wants to see. And by using this architecture-dependent message transfer descriptor, we can completely reuse all the mechanisms. It's just a message that looks different depending on which architecture you're on. FPU is an interesting state because it's kind of large. So on ARM, it's 32 128-bit words, which is 512 bytes. This is something you do not want to switch on every VM exit or on every context switch. So we switch the FPU lazily, which has some consequences. So we call this thread, which currently has its state saved in the FPU. We call it the FPU owner. And then whenever some other thread wants to access the FPU, we take the state from the owner, we save it lazily, give it to the other guy. So that means that the hypervisor has to do two things. When we switch away from the FPU owner, we have to disable the FPU to see any other access trapping. And when we switch back to the FPU owner, we have to re-enable the FPU because we don't want the owner to trap. The owner has its state in the FPU. And that means on a typical kernel exit pass, you have multiple conditions to check. Like, am I going back to the FPU owner? Is the FPU enabled? If not, and this can all be very time consuming because it's branch heavy code. So how do we make this efficient? Nova has a notion of hazards, which are exceptional conditions that the kernel needs to fix up before it goes back to user mode. And we have two types. We have a CPU hazard for certain exceptional conditions on the CPU, like the CPU needs to reschedule, the CPU needs to flush it, the CPU needs to restore a certain state. And we have the same thing for ECs. The EC needs to reload some state. The EC has been recalled and things like that. So what we do is we overlay two bits of the state from the CPU hazard and the EC hazard. Namely, the state FPU is disabled and the EC is not the FPU owner and FPU is enabled and the EC is the FPU owner. And only if the XOR of both states yields a value of one, which means these two conditions are out of sync, do we actually vector through the hazard pass and do we do this FPU switching magic? In the fast case, where the FPU is already in the right state, so it's disabled and the EC is not the owner or it's enabled or it is the owner, we will not take the slope pass. So these are some of the performance tricks that Nova is using to get really excellent virtualization performance. I'll talk a little bit about interrupt virtualization on ARM because unlike X86, we get a lot of help from the hardware. Actually, ARM V8 has the interrupt controller split into two parts. There's one part that lives in the chipset, which is called, which is the upper part, the upper box, consisting of the gig distributor and the gig redistributor. You can think of it like an IOAPIC. The distributor is the global part, which takes shared peripheral interrupts coming from devices and the redistributors are CPU local parts, which take interrupts like core local timer interrupts, core local performance counter interrupts and things like that. And then the distributor and redistributor send physical interrupts to the CPU interface, which is called gig C, and then they normally go to the processing element, which is your processor. So that's the left side of this diagram. And this is the thing that gets used when virtualization is not in the game. This virtualization, you get the right side of this processing element consisting of something called gig H and gig V. So what ARM did there is they created a virtual interface of the gig C, which looks exactly the same like the physical CPU interface, except that it doesn't get its interrupt from the distributors. It gets its interrupt from the hypervisor control interface. And this is what Nova drives. So what we do is the map gig V directly into the physical address space of the VM so the guest can access it anywhere at once without causing any exits. And all the interrupt injections that come from the hypervisor go to the control interface. And this control interface autonomously injects interrupts into the guest. So this is very efficient. How we expose this at the API level is twofold. First of all, the interrupt injection logic between gig two and gig three uses a different format, which is really not so nice. So we abstract on the injection interface the differences away. We let the VMM always tell us interrupts in gig three format. And if you run on something older, we convert. And then we have a hyper call called assign interrupt, which the partition manager can use to steer interrupts to specific cores. Next thing is timer virtualization. ARM has a global system counter, which distributes the time in the entire system to all the cores. And this is exposed on each core in form of two counters and two timer instances. One is called the physical timer, which is directly reflects the system counter and the other is called virtual timer, which has an offset applied or subtracted from the system counter so that you can hide time progression from a guest. The good thing is that the physical timer can be trapped. So it can be disabled. You can trap and emulate it. And this is what we do. And this emulation works much similar to x86. So the VMM uses a timer interrupt summer for to catch this timer expiring. And then this interrupt is asynchronously delivered. It's much more complicated for the virtual timer because the ARM architecture does not allow you to trap or to intercept the virtual timer, which really forces you to contact, switch it. So every time we switch from one vcpu to another, we context switch the virtual timer, which is obviously a little bit ugly from a context state-saving perspective. But the good thing is that the timer interrupt will always be synchronous to the execution of the vcpu. So the timer interrupt can never come when that vcpu is not running. And whenever a timer interrupt comes, it is for exactly this vcpu. So we deliver such a timer interrupt directly synchronously via a portal. Next thing is I want to talk about is a system MMU. System MMU is a crucial piece of a security critical system because you need not only protect applications from viding to each other's address spaces by means of virtual memory and an MMU. You also need to prevent rogue drivers that can do DMA from DMA, DMAing all over the place, like overriding the hypervisor, overriding their neighboring protection domain, and this is what x86 uses an IOMMU for, and the ARM concept is called a system MMU. So a DMA transaction that arrives at the system MMU on the left side of the picture has two attributes. It has a stream ID which identifies which device it's coming from, and it has a, let's call it a virtual address or an IOM address, which is where the device wants to DMA to. And then ARM has a configuration piece in the SMMU that consists of stream mapping group which allows you to associate streams to translation context. So we have two streams mapping to the first translation, one stream mapping to the first translation context, and two streams mapping to the second translation context. So this would be two devices assigned to the same PD, and then a translation context directly maps to a DMA page table, and there's a TLD in the middle that can cache frequently used translations. So it's really important to have this piece supported in Hypervisor, otherwise DMA is a critical attack vector. So there's a limited number of these stream mapping groups and context, which is why we let the partition manager manage them, and NOVA then manages the translation part, keeping the page tables and the TLD consistent, assigning devices to PDs, and there's an assigned device hypercall for doing this assignment and binding a device to protection domain. So with that, let's take a look at all the platforms that we currently support. We'll do a little demo here in a few minutes. We'll do this demo on the top left board, which is an Affnit-Tilings Ultra96 board, and the reason we are doing that is precisely because it has an SMMU. A lot of the other boards do not, but this board has one, and we obviously want to use the best infrastructure that we can have. We also run on the NXP IMX 8M quad, and those of you who were in Stefan's talk just a couple minutes ago, you already saw that board in action, and the VMM that we use on top of NOVA was, as Stefan pointed out, a joint development effort between Bedrock and Gnode, and it was a lot of fun to work on this together. We also run on an Renaissance R-car. The difference for the R-car is that it's actually two clusters, of course, of different cores, so it's a big little system. We also support big little, and then, as we know, Fustim is a community conference, and a lot of you have probably gotten a Raspberry Pi 4, so NOVA also runs on that. We also did a lot of prototyping on QMU, so naturally, we support QMU out of the box. The NXP, by the way, is the only board we have that has a GIG-3. We have all combinations of different GIGs, this MMU, this out SMMU, single cluster, multi cluster, all of this is supported. With that, I'd like to invite my colleague Shantanu up here, who will do a little demo for you. I'll quickly summarize what we are going to show. We have NOVA hypervisor, we have a bunch of devices. We'll assign different devices to different virtual machines using SMMU, as you can see here in these shaded colors. Every virtual machine has a bunch of VRDIO interfaces, like a virtual ethernet and a virtual UART. We connect the different virtual machines together using a virtual ethernet switch. We also have a console into every virtual machine using a UART multiplexer, with the UART driver being a component in the host that has direct access to the UART hardware. With that, I'll give the mic to Shantanu and he will walk you through the demo and show you a bunch of things. Okay, so Udo, do you make this full screen? Can you make this full screen? I don't know, just this draw, sorry. Okay, it was that easy. Okay, so going by the picture that Udo showed earlier, we've now booted into our UART multiplexer. This is the administrative console of our multiplexer. It's an asynchronous console. Basically, we can cache all the data coming from our virtual machines. We can list the clients that are connected right now. As you see, we have three virtual machines, so three VMMs. We have the console from NOVA. We have the MSC, that's the master controller, that's our root hyper process. Then we have the three guests, which is an Android and two Linuxes. Just to show you the boot logs, maybe from NOVA, because we just had the talk. The screen is not big enough, but what you see here is the typical boot log you get from NOVA. Most of what's here is basically the interrupts that have been passed on and configured for the guests. To show you maybe a virtual machine monitor, these are the logs from our VMM. This one is hosting an Android system. What you see here is a pass-through for the devices, the display, the USB controller, because there's a touchscreen attached, and also a connection to the V-switch. We have a virtual switch that connects three virtual machines here, like Udo showed earlier. Let me quickly get into a guest here. This one is running the network driver. It has our Wi-Fi driver, and I'll also set it up to use the virtual console switch and set up DHCP server so that the other machines can get an IP. What I need to do is probably assign myself an IP address and also start a DHCP server. To make sure that this is working, I have another Linux system. This one doesn't have network connection right now, but I can run DHCP clients here. Now I have a virtual connection and I also got myself an IP address from the other VM. We can exercise this interface, maybe sending some packets, possibly doing a throughput test with the other VM. I think I put the wrong IP address. I can definitely ping. Sorry for that. I put the wrong IP address earlier. We have a throughput of 580 megabits or so between the two virtual machines. This is just exercising the interface. Because this is the VM that has access to our Wi-Fi driver, I can also connect it. Maybe I'll just set up a quick hotspot on my cell phone, not trusting the Wi-Fi here. I just used WPS applicants to set up a Wi-Fi network. Now I have Wi-Fi on my Linux. I have a virtual Ethernet. Now I can show you the console from Android. This is a development build, so please ignore all the audit logs coming from my Linux. As you can see, Android has also picked up an IP address because of our DHCP server running. Basically, what it now needs is just a connection to the Internet. I'll do that. I'll just set up NAT tables and make my network VM behave as a router. Now my Android should have access to the network. It does. Basically, this is how we isolate the network driver from Android. It's a separate virtual machine. Android itself can be connected to the outside world through this connection. Because there was already a Star Wars shown before this, I will probably run some other web page. Maybe the data and time today. I don't know if people at the back can see. I think I misdaped something. Can you type that? Unfortunately, not very used to German keyboards. You should see a page loading here telling you the data and time today. It's a very slow Internet connection. We have today's data time getting it from the network. I'll hand it back to Udo to conclude this. Thanks, Shantanu, for this impressive demo. Shantanu spent a lot of time working on this with the other parts of our user land team. It's only fair to let him demo this system in action. Let me just repeat what you just saw. We showed three VMs, an Android with two virtual CPUs, a Linux and another Linux with a single core. We can support SMP and uniprocessor virtual machines. We can show different types of virtual machines. Android and we saw two different versions of Linux. We have virtual devices, we have pass-through devices with the SMMU. We have a virtual ethernet switch that can connect all the different VMs together. We can do host drivers and all of this on an RMA system. Let's talk a little bit about roadmap because this is obviously not the end of the road. We made the ARM port as a rapid prototyping effort together with our friends from Geno to help us on the VMM side. We developed this independently on a separate branch, which means that today the ARM and the X86 version have a little bit diverged. The next effort that I'll be spending time on is to merge significant portions of the X86 and ARM branch. I said we have roughly 10,000 lines of code on one side and 7,000 on the other side and we can probably get that well below 17,000. Maybe half that or something like that. We want to support newer ARM features because ARM has put a lot of cool features into the architecture such as point authentication, memory tagging, all of which is useful in a secure system. In terms of what additional functionality we'll add to NOVA, then in the X86 and ARM version, we make the hypervisor binary relocatable, which means you can move it anywhere in memory and it will run. So that's good for different systems which have different physical memory layouts. We add a lot of features which will help people build VM introspection on top of NOVA, which means you can use the hypervisor to peek into what's happening inside a virtual machine, maybe protect stuff inside a virtual machine from the outside. We have a lot of ideas how we can improve the current resource management and obviously as part of the effort of merging these two branches, we'll also take a look at all the cool things that other people have built on top of NOVA and see which of those are useful for us. And there's I bet also a bunch of bug fixes that we haven't yet incorporated. There will always be performance optimizations. I think performance is already on par with the best microcores that we have, but we encourage independent benchmarking and we have a big effort going on around formal verification of the hypervisor code and of the verification of the components that run on top of it. And those of you who heard the SFO talk today know that verifying something is a really hard exercise, especially if you're talking about something like on V8 and especially if you're talking about SMP. So what does formal verification on NOVA roughly look like? And I don't want to go into the details here. The head of our form message team is here, so if there are any detailed questions, I will just directly hand those questions to him. But to give you a feeling for what that would look like, you have a really simple function here and obviously the functions in NOVA are a lot more complicated. A function that adds two unsigned 32-bit numbers, X and Y, and returns the result. And what programmers do to make their code formally verifiable is they annotate it with pre and post conditions. Component-lit already showed sort of a similar structure. So what we say here is we have, we introduce in the precondition two new variables, V1 and V2, that carry integer values, V1 and V2, that we bind to the parameters X1 and X2. Otherwise the precondition is empty because this function does not touch any global state. And we have a post condition that also does not touch any external global state except for the return value. And the return value is the sum of V1 plus V2. But since we are adding two 32-bit numbers, this addition can obviously overflow. So we have to trim the result to a 32-bit value. And all the functions in the kernel will be annotated with specifications like this. And then we have a tool chain that looks like the bottom of this slide. So the way this list works is as follows. From a high-level perspective, we have the source code which is written in CPP or HPP files. Then we run a tool on it which is called CPP to V. CPP to V is a tool that we wrote at Bedrock. Gregory wrote it. The gentleman sitting there. It's a clang plug-in which takes the abstract syntax tree of NOVA and converts it into a cog representation of that abstract syntax tree. So what you get out of this is a file called foo.cvp.v. And the annotations of the source code which you can either write inline or we nowadays prefer to write them out of line, come in a separate file called foo.cvp.spec.v. These two files are put in the cog compiler along with semantics of the C++ language. And we are also heavily investing in proof automation because proving something, as you heard earlier today, is a lot of manual effort. And the more you can automate this, the faster you can re-prove things. Like if you make a change which touches only a minor portion of the code, there's a high chance that significant portions of that proof will just go through the automation. What you get out of it is then a file called foo.cvp.proof.vo, which is the machine check proof. And this is an ongoing effort, so we're not as far as SEO4, but I think the toolchain that we have there is already looking really, really good. So with that, I'll conclude my talk and take questions. We just made the source code of the NOVA on port public. As the rest of NOVA, it's available under a GPL v2 license. You can download it from those two links. There's a bedrock systems repository, and there's the repository where NOVA has always lived, my private one. It's important to pick up the ARM branch, not the old XZ6 branch. And there's web pages that have further information, papers, links, and so forth. And with that, I'll conclude the talk and I'll be happy to take any questions you may have. So where do you see the differentiating points to SEO4? So as far as I understand, SEO4 has mostly, so the question was, where do we see the differentiating points to SEO4? So I think the major focus of SEO4 has always been on the formal verification of the kernel. The major focus for NOVA's existence was always to make virtualization and component-based systems on top of a single hypervisor possible. At some point, you also have to formally verify to get a compelling security story. So this is something where I see SEO4 clearly as the thought leader. But performance-wise, I think we are very competitive. I'm not sure, maybe Garnet can comment on that. The way I understood it, SEO4 only runs on ARMv7, and there's an ongoing effort to port it to ARMv8, so NOVA is now running on ARMv8. You're running on ARMv8? We support it on ARMv8 for at least three years at least. So SEO4 also runs on ARMv8, but it's not verified. So we do not plan to support ARMv7 as a hypervisor interface, but we support 32-bit guests, which are ARMv7 backward compatible. I can quite get the formal verification bit. I do understand if you actually could use some kind of input to the formal verifier from the SQL. That's my understanding, but that's different from having, well, a design that actually breaking down stuff and improving stuff in regard to the design. So what you can prove is that a function probably has specific characteristics, but this has nothing about the overall architecture. So what is the question? So you need a model. So the question was, if you have a simple function like this, this connect to the overall architecture because proving a simple function doesn't prove that your whole system is correct. We use a concept called separation logic to be able to reason independently about different functions of the system, which makes the whole proof effort very modular, which means if you can reason about this function, only touches a certain fraction of the state and does not affect anything in the other portion of the state, then you can verify that function and you know it doesn't affect the other side. You need to prove certain things at different levels. So we need to have a model of how the system behaves, like how Nova behaves, but you also need to show that the source code actually conforms to that model. So the system specification and the specification of the Nova functions will be connected through those annotations. The actual source code will be connected to the functional specification of all these functions through the tool CPP2V, which shows that the code that the compiler generated, the abstract syntax tree, conforms to the specification that this function has. Where does the system model come from? It's also something that we built. Okay. Yeah. So is the aim full function correctness? Gregor, you want to take that question? Yeah. So the aim was, or the question was, is the aim full functional correctness? So one of the properties that we will prove at Bedrock is what we call the bare metal property. And the bare metal property in a nutshell expresses that if you execute something in a virtual machine, it will behave as if you executed it on bare hardware minus some timing requirements. But from a correctness perspective, you want to show that execution of something in a VM does not differ except for small timing effects from execution on a bare metal machine. And this function or this property obviously also entails that NOVA does not crash and that the VM emulates the instructions correctly and so forth. Yes, here's another question. Do you have a thing that it will require some changes in architecture to make the oldest form of verification run or you assume that your current architecture is suitable for your goals? No back in architecture, I mean, not looking about it, just deploying crashes. So the question was, will formal verification require us to re-architect certain aspects of NOVA or do we expect it to be formally verifiable as is? I expect that we may find maybe one or two things that we want to change. Maybe also not because they were incorrect but because they make the verification easier. But overall, I don't expect too many surprises in terms of the code being correct because we exercise it already quite a lot and other people like Gino do too. And you've seen the complex scenarios that run on top of it. Are we surprised, of course. Of course. Is there a question in the middle? I've seen VM introspection in the road map. What kind of introspection do we have there? So the question was, we've listed VM introspection in our road map. What kind of VM introspection do we do? So we provide mechanisms for VM introspection for being able to look at the memory of a virtual machine, to be able to look at register state, maybe set breakpoints, intercept execution control at critical points. But these are low-level mechanisms. The more richer VM introspection features that we build on top, we have not yet disclosed. Yep. What's your open source plan beyond NOVA? I mean, you showed several other components. So the question was, what is our plan for open sourcing the remaining parts of the stack? So NOVA has just gone open source. The remaining parts of the system will progressively go open source over the course of the next year. Like we said, we jointly developed the user-level virtual machine monitor with G-Node. Before we make that public, we want to make sure that it really fits their model and our model very well, because we want this to be a community effort. So we don't want to go out with something that is half-baked. So we will polish that a little bit before we make it public. But the plan is to make the entire virtualization layer basically everything that's shown in the host public. Gennad. Will the verification artifacts be open sourced? I'll... Gregory? The question was, will the verification artifacts be open sourced? If you're in discussions about that, I would like to open source as much as possible. So the answer was, you would like to make the artifacts public, but this is a separate discussion and we will discuss it offline. Just so it's clear that all the words match in my opinion. Yep. I think Gregory would agree with that. There was another question here. Which use cases could you imagine for the pro-co-op information? So the primary use case for the proof automation is that we want the code to be agile, not in the development sense, but in the sense that we want to add new features. We want to make changes. We want to make additions, new architecture port. And we do not want to go through a lot of manual labor of fixing up the proof. So we want to automate this as much as possible. So the whole purpose of proof automation is to make the proof go through faster, to make the proof less manual. And I think we also have a plan to work a lot with academia on developing new tactics to make the proof automation smarter. So if anybody is interested in working in these areas, talk to Gregory. Any further questions? Okay. I think that's it. Thank you very much. Thank you very much.
 The next talk is given by Udo Steindag.  I'm excited about Udo because Udo hasn't been giving a talk here for many years, I think.  Six, seven.  Now he's back to talk about new developments in the Nova world.  Yeah, I'm excited to be here too.  Let's first do a little poll.  Who of the audience has heard of Nova or who has worked with Nova?  Maybe a quick short of hands.  Okay, I think about half the folks.  So today I'll be giving a talk about Nova hypervisor on ARM V8A, which is our port of Nova to the most recent ARM architecture.  And since only half of you know Nova very well, the first part of the talk will go a little bit into detail about what Nova is and where we came from.  Then the second part of the talk, I'll talk about virtualization on ARM V8A.  ARM A is the A profile for the performance course.  There's also ARM R for real-time course and ARM M.  We are talking about Cortex A.  And then I'll conclude the talk with the current status.  We'll do a little demo here.  We've already put some equipment here and then I'll talk a little bit about roadmap.  So those of you who've been following the micro-commoderum today,  you've seen this system which is Nova on x86 already in action when Norman gave his talk on G-node.  So Nova on x86 is a system that has existed for more than 10 years.  And the way that virtualization works on x86 is that without the virtualization extensions,  you have two processor rings, really four of which only two are used.  You have ring zero which is used by the kernel and ring three which is user mode.  And you have an operating system and applications running in those two modes.  With virtualization, these rings are now called guest rings,  which is why we call them ring zero, G, and ring three, G.  And you get the same set of rings duplicated for host mode.  We have ring zero H and ring three H.  So ring zero host is occupied by the Nova microhypervisor.  And ring three host is occupied by what we call hyper processes.  And the whole G-node framework that you saw two talks ago is a framework that runs in rings three host.  It's interesting to note that the Nova microhypervisor is the only component that runs privileged.  And everything else, all the colorful apps that run in the host and everything that runs in guest runs deep privileged.  And there's a little footnote there that says obviously we have no control of firmware.  What's also interesting to note is that we give every virtual machine its own instance  of a user level virtual machine monitor, which means that should something go wrong in a virtual machine,  should you have a VMscape, should an instruction not be virtualized properly or something like that,  then a VMscape will only affect that VMM instance and the rest of the system will not be affected.  So now we took this system and we said, can we build something like that on ARMv8?  And the next slide shows what does Nova look like on an ARMv8 architecture.  So at the bottom we have the hardware and then we have four privileged levels which ARM calls execution levels.  So starting at the top, we have EL0 which is user mode, EL1 which is supervisor mode where kernel runs,  EL2 is called hypervisor mode. This is where Nova lives.  And then we have EL3 which is called monitor mode in which a firmware monitor sits that can switch between a non-secure and a secure world.  And we do not own this monitor. We do not control it.  And we also do not control a trusted execution environment like an opti that runs along the side.  But in the world that we own, which is the top left corner, the non-secure world upwards from EL2,  Nova is the only privileged component and all the other properties that we had on X86,  including a virtual machine monitor, per guest VM, and the deep privileged host environment,  all of that has been carried forward to ARM.  Now let's talk a little bit about Nova.  Nova is hypervisor, micro hypervisor that takes the best ideas from micro kernels, capability-based systems,  high performance virtualization, and puts all of that together in a small piece of code where the X86 version is less than 10,000  and the ARM version currently is less than 7,000 lines of code.  It is based around capabilities. What does that mean?  We have a bunch of kernel objects that I've shown in the middle. We have protection domains.  These are address bases. We have execution contacts. You can think of them as threads of virtual CPUs.  We have portals. These are communication endpoints by which protection domains and threads inside them can communicate.  And all these kernel objects cannot be referenced directly.  Instead, we give every protection domain that needs to access them a capability.  What is the capability?  You can think of a capability as a pointer to a kernel object plus associated permissions.  So procession of a capability gives you the right to invoke that capability and to access that object.  And if you don't have a capability to an object, you can neither name the object nor access it.  So that's a very powerful security system.  SEO4 has the same and a lot of newer micro kernels do.  And you can build really powerful other systems on top as Norman has demonstrated with Genome.  The same principle, by the way, works for memory where you can think of a virtual address as being a capability to a physical memory page with read write execute permissions.  So that same principle is also applied for Nova.  So we have multiple spaces. We have an object space for these capabilities.  And we have a memory space for delegation of writes to memory.  In the older version, the x86 version, we used to have a mapping database that tracked all these dependencies of who gave the capability to whom and things like that.  We got rid of all that.  We replaced it with a new hyper call called control protection domain, which takes two capabilities, the center and the receiver protection domain.  And you have a take grant model where the possession of, let's say, a capability A and a capability B for those two protection domains, you can say,  take the two capabilities from slots two and three in protection domain A and put them in slots six and seven of protection domain B.  And obviously, we have more than eight slots.  This is just for illustrative purposes.  And then the user wants to refer to a capability.  They give us a select door, which is a number and index into that space and say, I want to do something with capability to this is how it works.  It's like a file script.  So upon this, we built some basic abstractions.  And these are the basics abstractions that the Nova version on x86 has had for a long time.  So on the left, you can see two protection domain.  Think of them as two address spaces, two applications that want to communicate with each other.  And in the production domain, A, we have a call us red and EC here and it has a scheduling context attached to it.  And those of you who saw gonna talk this morning know that the scheduling context is a really nice abstraction for expressing scheduling parameters and for delegating it along a call to implement priority inheritance and Nova has had this for 10 years.  And we also have on the other side a call the execution context that has no scheduling context for the very same reason that Garnet gave that you can completely account the execution.  Of a server invocation to the caller.  So what what would that look like the caller makes a hyper call in this case called IPC call.  It gives a capability select or a selector to a portal.  And what's called an empty D we call is message transfer descriptor and a message transfer descriptor tells Nova how many words to copy from the UTCB of the caller to the UTCB of the callee.  So the UTCB is like a message in an outbox.  It's very abstract and the same mechanism applies no matter whether you are on x86 or on arm.  So once that call has been made, you know, transition over to the right side.  The situation looks like this.  The scheduling context has been given to the callee.  This achieves priority inheritance or in case of real time bandwidth inheritance.  The callee can now execute because it has a time slice.  Time is accounted to the client to the caller.  And at some point the callee is going to do a reply.  It invokes IPC reply, gives a message transfer descriptor says how many words to a one a copy back from my UTCB to the caller.  And then we are back to the left side.  This is the basic mechanism by which protection domains and threats in protection domains communicate with each other.  And this also illustrates how the different kernel objects sort of come into play there.  So the empty D defines the number of words to copy between those two yellow UTCBs.  And we'll see in the next slide how the empty D is also used for other purposes.  Now I said Nova is a micro hypervisor.  This means at some point we need to deal with virtual machines, with virtual CPUs, with emulating instructions and devices.  So a lot of you will notice that this light looks very, very similar to the previous light.  Why is that?  Because we layer VM exit handling and the emulation exactly on top of IPC.  So the difference is that we now have two protection domains that are called a virtual machine in which an execution context run that is a VCPU.  And we have a VMM, which in this case is the server.  It provides the virtual machine service and the execution context here we call it handler.  So at some point the virtual CPU is going to take a VM exit on x86 or an exception on ARM, which requires the attention of the virtualization there.  This VM exit takes us into Nova.  Nova will save the state in a page which we call virtual machine control block because we came from x86.  And then Nova is going to synthesize an IPC call on behalf of the virtual CPU, send it to the handler.  And the question is now what state do we transmit?  And that state is called empty D arc.  And it comes out of a portal where every event has its own portal.  So you can say, if I see this event, here's that state that I want.  If I see some other event, here's this state that I want.  And then the VMM gets this message in its UTZB.  And the reply works exactly like an IPC reply, except that the handler specifies an empty D arc.  The result gets stored in a VMCB.  And when the VCPU resumes or erads back to the guest, that state will be restored.  So empty D arc is similar to the empty D that I showed you before, which copies state around, except this time between VMCB and UTZB and not between two UTZBs.  Same with the scheduling context, the entire accounting of the emulation goes onto the scheduling context of the VCPU.  Now we get into ARM territory.  And before we do that, I'll show you how we hide the differences between x86 and ARM.  And you don't have to understand all these details.  But here I've shown you the empty D, the empty D arc for ARM and x86, which is basically a bit field that describes the different fields.  And these will also be listed in the NOVA interface specification.  So the VMM gets to decide for every event which part of the architectural states it wants to see.  And by using this architecture-dependent message transfer descriptor, we can completely reuse all the mechanisms.  It's just a message that looks different depending on which architecture you're on.  FPU is an interesting state because it's kind of large. So on ARM, it's 32 128-bit words, which is 512 bytes.  This is something you do not want to switch on every VM exit or on every context switch.  So we switch the FPU lazily, which has some consequences.  So we call this thread, which currently has its state saved in the FPU.  We call it the FPU owner.  And then whenever some other thread wants to access the FPU, we take the state from the owner, we save it lazily, give it to the other guy.  So that means that the hypervisor has to do two things.  When we switch away from the FPU owner, we have to disable the FPU to see any other access trapping.  And when we switch back to the FPU owner, we have to re-enable the FPU because we don't want the owner to trap.  The owner has its state in the FPU.  And that means on a typical kernel exit pass, you have multiple conditions to check.  Like, am I going back to the FPU owner? Is the FPU enabled? If not, and this can all be very time consuming because it's branch heavy code.  So how do we make this efficient?  Nova has a notion of hazards, which are exceptional conditions that the kernel needs to fix up before it goes back to user mode.  And we have two types.  We have a CPU hazard for certain exceptional conditions on the CPU, like the CPU needs to reschedule, the CPU needs to flush it, the CPU needs to restore a certain state.  And we have the same thing for ECs. The EC needs to reload some state. The EC has been recalled and things like that.  So what we do is we overlay two bits of the state from the CPU hazard and the EC hazard.  Namely, the state FPU is disabled and the EC is not the FPU owner and FPU is enabled and the EC is the FPU owner.  And only if the XOR of both states yields a value of one, which means these two conditions are out of sync, do we actually vector through the hazard pass and do we do this FPU switching magic?  In the fast case, where the FPU is already in the right state, so it's disabled and the EC is not the owner or it's enabled or it is the owner, we will not take the slope pass.  So these are some of the performance tricks that Nova is using to get really excellent virtualization performance.  I'll talk a little bit about interrupt virtualization on ARM because unlike X86, we get a lot of help from the hardware.  Actually, ARM V8 has the interrupt controller split into two parts. There's one part that lives in the chipset, which is called, which is the upper part, the upper box, consisting of the gig distributor and the gig redistributor.  You can think of it like an IOAPIC. The distributor is the global part, which takes shared peripheral interrupts coming from devices and the redistributors are CPU local parts, which take interrupts like core local timer interrupts,  core local performance counter interrupts and things like that.  And then the distributor and redistributor send physical interrupts to the CPU interface, which is called gig C, and then they normally go to the processing element, which is your processor.  So that's the left side of this diagram. And this is the thing that gets used when virtualization is not in the game.  This virtualization, you get the right side of this processing element consisting of something called gig H and gig V.  So what ARM did there is they created a virtual interface of the gig C, which looks exactly the same like the physical CPU interface, except that it doesn't get its interrupt from the distributors.  It gets its interrupt from the hypervisor control interface. And this is what Nova drives.  So what we do is the map gig V directly into the physical address space of the VM so the guest can access it anywhere at once without causing any exits.  And all the interrupt injections that come from the hypervisor go to the control interface.  And this control interface autonomously injects interrupts into the guest. So this is very efficient.  How we expose this at the API level is twofold.  First of all, the interrupt injection logic between gig two and gig three uses a different format, which is really not so nice.  So we abstract on the injection interface the differences away. We let the VMM always tell us interrupts in gig three format.  And if you run on something older, we convert.  And then we have a hyper call called assign interrupt, which the partition manager can use to steer interrupts to specific cores.  Next thing is timer virtualization.  ARM has a global system counter, which distributes the time in the entire system to all the cores.  And this is exposed on each core in form of two counters and two timer instances.  One is called the physical timer, which is directly reflects the system counter and the other is called virtual timer,  which has an offset applied or subtracted from the system counter so that you can hide time progression from a guest.  The good thing is that the physical timer can be trapped.  So it can be disabled. You can trap and emulate it. And this is what we do.  And this emulation works much similar to x86.  So the VMM uses a timer interrupt summer for to catch this timer expiring.  And then this interrupt is asynchronously delivered.  It's much more complicated for the virtual timer because the ARM architecture does not allow you to trap or to intercept the virtual timer,  which really forces you to contact, switch it.  So every time we switch from one vcpu to another, we context switch the virtual timer,  which is obviously a little bit ugly from a context state-saving perspective.  But the good thing is that the timer interrupt will always be synchronous to the execution of the vcpu.  So the timer interrupt can never come when that vcpu is not running.  And whenever a timer interrupt comes, it is for exactly this vcpu.  So we deliver such a timer interrupt directly synchronously via a portal.  Next thing is I want to talk about is a system MMU.  System MMU is a crucial piece of a security critical system because you need not only protect applications from viding to each other's address spaces  by means of virtual memory and an MMU.  You also need to prevent rogue drivers that can do DMA from DMA, DMAing all over the place, like overriding the hypervisor,  overriding their neighboring protection domain, and this is what x86 uses an IOMMU for, and the ARM concept is called a system MMU.  So a DMA transaction that arrives at the system MMU on the left side of the picture has two attributes.  It has a stream ID which identifies which device it's coming from, and it has a, let's call it a virtual address or an IOM address,  which is where the device wants to DMA to.  And then ARM has a configuration piece in the SMMU that consists of stream mapping group which allows you to associate streams to translation context.  So we have two streams mapping to the first translation, one stream mapping to the first translation context,  and two streams mapping to the second translation context.  So this would be two devices assigned to the same PD, and then a translation context directly maps to a DMA page table,  and there's a TLD in the middle that can cache frequently used translations.  So it's really important to have this piece supported in Hypervisor, otherwise DMA is a critical attack vector.  So there's a limited number of these stream mapping groups and context, which is why we let the partition manager manage them,  and NOVA then manages the translation part, keeping the page tables and the TLD consistent, assigning devices to PDs,  and there's an assigned device hypercall for doing this assignment and binding a device to protection domain.  So with that, let's take a look at all the platforms that we currently support.  We'll do a little demo here in a few minutes.  We'll do this demo on the top left board, which is an Affnit-Tilings Ultra96 board,  and the reason we are doing that is precisely because it has an SMMU.  A lot of the other boards do not, but this board has one, and we obviously want to use the best infrastructure that we can have.  We also run on the NXP IMX 8M quad, and those of you who were in Stefan's talk just a couple minutes ago,  you already saw that board in action, and the VMM that we use on top of NOVA was, as Stefan pointed out,  a joint development effort between Bedrock and Gnode, and it was a lot of fun to work on this together.  We also run on an Renaissance R-car.  The difference for the R-car is that it's actually two clusters, of course, of different cores, so it's a big little system.  We also support big little, and then, as we know, Fustim is a community conference,  and a lot of you have probably gotten a Raspberry Pi 4, so NOVA also runs on that.  We also did a lot of prototyping on QMU, so naturally, we support QMU out of the box.  The NXP, by the way, is the only board we have that has a GIG-3.  We have all combinations of different GIGs, this MMU, this out SMMU, single cluster, multi cluster, all of this is supported.  With that, I'd like to invite my colleague Shantanu up here, who will do a little demo for you.  I'll quickly summarize what we are going to show.  We have NOVA hypervisor, we have a bunch of devices.  We'll assign different devices to different virtual machines using SMMU, as you can see here in these shaded colors.  Every virtual machine has a bunch of VRDIO interfaces, like a virtual ethernet and a virtual UART.  We connect the different virtual machines together using a virtual ethernet switch.  We also have a console into every virtual machine using a UART multiplexer,  with the UART driver being a component in the host that has direct access to the UART hardware.  With that, I'll give the mic to Shantanu and he will walk you through the demo and show you a bunch of things.  Okay, so Udo, do you make this full screen? Can you make this full screen?  I don't know, just this draw, sorry.  Okay, it was that easy.  Okay, so going by the picture that Udo showed earlier, we've now booted into our UART multiplexer.  This is the administrative console of our multiplexer. It's an asynchronous console.  Basically, we can cache all the data coming from our virtual machines.  We can list the clients that are connected right now.  As you see, we have three virtual machines, so three VMMs.  We have the console from NOVA.  We have the MSC, that's the master controller, that's our root hyper process.  Then we have the three guests, which is an Android and two Linuxes.  Just to show you the boot logs, maybe from NOVA, because we just had the talk.  The screen is not big enough, but what you see here is the typical boot log you get from NOVA.  Most of what's here is basically the interrupts that have been passed on and configured for the guests.  To show you maybe a virtual machine monitor, these are the logs from our VMM.  This one is hosting an Android system.  What you see here is a pass-through for the devices, the display, the USB controller,  because there's a touchscreen attached, and also a connection to the V-switch.  We have a virtual switch that connects three virtual machines here, like Udo showed earlier.  Let me quickly get into a guest here.  This one is running the network driver.  It has our Wi-Fi driver, and I'll also set it up to use the virtual console switch  and set up DHCP server so that the other machines can get an IP.  What I need to do is probably assign myself an IP address and also start a DHCP server.  To make sure that this is working, I have another Linux system.  This one doesn't have network connection right now, but I can run DHCP clients here.  Now I have a virtual connection and I also got myself an IP address from the other VM.  We can exercise this interface, maybe sending some packets, possibly doing a throughput test with the other VM.  I think I put the wrong IP address.  I can definitely ping.  Sorry for that.  I put the wrong IP address earlier.  We have a throughput of 580 megabits or so between the two virtual machines.  This is just exercising the interface.  Because this is the VM that has access to our Wi-Fi driver, I can also connect it.  Maybe I'll just set up a quick hotspot on my cell phone, not trusting the Wi-Fi here.  I just used WPS applicants to set up a Wi-Fi network.  Now I have Wi-Fi on my Linux.  I have a virtual Ethernet.  Now I can show you the console from Android.  This is a development build, so please ignore all the audit logs coming from my Linux.  As you can see, Android has also picked up an IP address because of our DHCP server running.  Basically, what it now needs is just a connection to the Internet.  I'll do that. I'll just set up NAT tables and make my network VM behave as a router.  Now my Android should have access to the network.  It does.  Basically, this is how we isolate the network driver from Android.  It's a separate virtual machine.  Android itself can be connected to the outside world through this connection.  Because there was already a Star Wars shown before this, I will probably run some other web page.  Maybe the data and time today.  I don't know if people at the back can see.  I think I misdaped something.  Can you type that?  Unfortunately, not very used to German keyboards.  You should see a page loading here telling you the data and time today.  It's a very slow Internet connection.  We have today's data time getting it from the network.  I'll hand it back to Udo to conclude this.  Thanks, Shantanu, for this impressive demo.  Shantanu spent a lot of time working on this with the other parts of our user land team.  It's only fair to let him demo this system in action.  Let me just repeat what you just saw.  We showed three VMs, an Android with two virtual CPUs, a Linux and another Linux with a single core.  We can support SMP and uniprocessor virtual machines.  We can show different types of virtual machines.  Android and we saw two different versions of Linux.  We have virtual devices, we have pass-through devices with the SMMU.  We have a virtual ethernet switch that can connect all the different VMs together.  We can do host drivers and all of this on an RMA system.  Let's talk a little bit about roadmap because this is obviously not the end of the road.  We made the ARM port as a rapid prototyping effort together with our friends from Geno to help us on the VMM side.  We developed this independently on a separate branch, which means that today the ARM and the X86 version have a little bit diverged.  The next effort that I'll be spending time on is to merge significant portions of the X86 and ARM branch.  I said we have roughly 10,000 lines of code on one side and 7,000 on the other side and we can probably get that well below 17,000.  Maybe half that or something like that.  We want to support newer ARM features because ARM has put a lot of cool features into the architecture such as point authentication, memory tagging,  all of which is useful in a secure system.  In terms of what additional functionality we'll add to NOVA, then in the X86 and ARM version,  we make the hypervisor binary relocatable, which means you can move it anywhere in memory and it will run.  So that's good for different systems which have different physical memory layouts.  We add a lot of features which will help people build VM introspection on top of NOVA,  which means you can use the hypervisor to peek into what's happening inside a virtual machine,  maybe protect stuff inside a virtual machine from the outside.  We have a lot of ideas how we can improve the current resource management and obviously as part of the effort of merging these two branches,  we'll also take a look at all the cool things that other people have built on top of NOVA and see which of those are useful for us.  And there's I bet also a bunch of bug fixes that we haven't yet incorporated.  There will always be performance optimizations.  I think performance is already on par with the best microcores that we have,  but we encourage independent benchmarking and we have a big effort going on around formal verification of the hypervisor code  and of the verification of the components that run on top of it.  And those of you who heard the SFO talk today know that verifying something is a really hard exercise,  especially if you're talking about something like on V8 and especially if you're talking about SMP.  So what does formal verification on NOVA roughly look like?  And I don't want to go into the details here.  The head of our form message team is here, so if there are any detailed questions,  I will just directly hand those questions to him.  But to give you a feeling for what that would look like, you have a really simple function here  and obviously the functions in NOVA are a lot more complicated.  A function that adds two unsigned 32-bit numbers, X and Y, and returns the result.  And what programmers do to make their code formally verifiable is they annotate it with pre and post conditions.  Component-lit already showed sort of a similar structure.  So what we say here is we have, we introduce in the precondition two new variables, V1 and V2,  that carry integer values, V1 and V2, that we bind to the parameters X1 and X2.  Otherwise the precondition is empty because this function does not touch any global state.  And we have a post condition that also does not touch any external global state except for the return value.  And the return value is the sum of V1 plus V2.  But since we are adding two 32-bit numbers, this addition can obviously overflow.  So we have to trim the result to a 32-bit value.  And all the functions in the kernel will be annotated with specifications like this.  And then we have a tool chain that looks like the bottom of this slide.  So the way this list works is as follows.  From a high-level perspective, we have the source code which is written in CPP or HPP files.  Then we run a tool on it which is called CPP to V.  CPP to V is a tool that we wrote at Bedrock.  Gregory wrote it. The gentleman sitting there.  It's a clang plug-in which takes the abstract syntax tree of NOVA and converts it into a cog representation of that abstract syntax tree.  So what you get out of this is a file called foo.cvp.v.  And the annotations of the source code which you can either write inline or we nowadays prefer to write them out of line,  come in a separate file called foo.cvp.spec.v.  These two files are put in the cog compiler along with semantics of the C++ language.  And we are also heavily investing in proof automation because proving something, as you heard earlier today,  is a lot of manual effort. And the more you can automate this, the faster you can re-prove things.  Like if you make a change which touches only a minor portion of the code,  there's a high chance that significant portions of that proof will just go through the automation.  What you get out of it is then a file called foo.cvp.proof.vo, which is the machine check proof.  And this is an ongoing effort, so we're not as far as SEO4,  but I think the toolchain that we have there is already looking really, really good.  So with that, I'll conclude my talk and take questions.  We just made the source code of the NOVA on port public.  As the rest of NOVA, it's available under a GPL v2 license.  You can download it from those two links.  There's a bedrock systems repository, and there's the repository where NOVA has always lived, my private one.  It's important to pick up the ARM branch, not the old XZ6 branch.  And there's web pages that have further information, papers, links, and so forth.  And with that, I'll conclude the talk and I'll be happy to take any questions you may have.  So where do you see the differentiating points to SEO4?  So as far as I understand, SEO4 has mostly, so the question was,  where do we see the differentiating points to SEO4?  So I think the major focus of SEO4 has always been on the formal verification of the kernel.  The major focus for NOVA's existence was always to make virtualization  and component-based systems on top of a single hypervisor possible.  At some point, you also have to formally verify to get a compelling security story.  So this is something where I see SEO4 clearly as the thought leader.  But performance-wise, I think we are very competitive.  I'm not sure, maybe Garnet can comment on that.  The way I understood it, SEO4 only runs on ARMv7, and there's an ongoing effort to port it to ARMv8,  so NOVA is now running on ARMv8.  You're running on ARMv8?  We support it on ARMv8 for at least three years at least.  So SEO4 also runs on ARMv8, but it's not verified.  So we do not plan to support ARMv7 as a hypervisor interface,  but we support 32-bit guests, which are ARMv7 backward compatible.  I can quite get the formal verification bit.  I do understand if you actually could use some kind of input to the formal verifier from the SQL.  That's my understanding, but that's different from having, well, a design that actually breaking down stuff  and improving stuff in regard to the design.  So what you can prove is that a function probably has specific characteristics,  but this has nothing about the overall architecture.  So what is the question?  So you need a model.  So the question was, if you have a simple function like this,  this connect to the overall architecture because proving a simple function doesn't prove that your whole system is correct.  We use a concept called separation logic to be able to reason independently about different functions of the system,  which makes the whole proof effort very modular,  which means if you can reason about this function,  only touches a certain fraction of the state and does not affect anything in the other portion of the state,  then you can verify that function and you know it doesn't affect the other side.  You need to prove certain things at different levels.  So we need to have a model of how the system behaves, like how Nova behaves,  but you also need to show that the source code actually conforms to that model.  So the system specification and the specification of the Nova functions will be connected through those annotations.  The actual source code will be connected to the functional specification of all these functions through the tool CPP2V,  which shows that the code that the compiler generated, the abstract syntax tree,  conforms to the specification that this function has.  Where does the system model come from?  It's also something that we built.  Okay.  Yeah.  So is the aim full function correctness?  Gregor, you want to take that question?  Yeah.  So the aim was, or the question was, is the aim full functional correctness?  So one of the properties that we will prove at Bedrock is what we call the bare metal property.  And the bare metal property in a nutshell expresses that if you execute something in a virtual machine,  it will behave as if you executed it on bare hardware minus some timing requirements.  But from a correctness perspective, you want to show that execution of something in a VM does not differ  except for small timing effects from execution on a bare metal machine.  And this function or this property obviously also entails that NOVA does not crash  and that the VM emulates the instructions correctly and so forth.  Yes, here's another question.  Do you have a thing that it will require some changes in architecture to make the oldest form of verification run  or you assume that your current architecture is suitable for your goals?  No back in architecture, I mean, not looking about it, just deploying crashes.  So the question was, will formal verification require us to re-architect certain aspects of NOVA  or do we expect it to be formally verifiable as is?  I expect that we may find maybe one or two things that we want to change.  Maybe also not because they were incorrect but because they make the verification easier.  But overall, I don't expect too many surprises in terms of the code being correct  because we exercise it already quite a lot and other people like Gino do too.  And you've seen the complex scenarios that run on top of it.  Are we surprised, of course.  Of course.  Is there a question in the middle?  I've seen VM introspection in the road map.  What kind of introspection do we have there?  So the question was, we've listed VM introspection in our road map.  What kind of VM introspection do we do?  So we provide mechanisms for VM introspection for being able to look at the memory of a virtual machine,  to be able to look at register state, maybe set breakpoints,  intercept execution control at critical points.  But these are low-level mechanisms.  The more richer VM introspection features that we build on top, we have not yet disclosed.  Yep.  What's your open source plan beyond NOVA?  I mean, you showed several other components.  So the question was, what is our plan for open sourcing the remaining parts of the stack?  So NOVA has just gone open source.  The remaining parts of the system will progressively go open source over the course of the next year.  Like we said, we jointly developed the user-level virtual machine monitor with G-Node.  Before we make that public, we want to make sure that it really fits their model and our model very well,  because we want this to be a community effort.  So we don't want to go out with something that is half-baked.  So we will polish that a little bit before we make it public.  But the plan is to make the entire virtualization layer basically everything that's shown in the host public.  Gennad.  Will the verification artifacts be open sourced?  I'll... Gregory?  The question was, will the verification artifacts be open sourced?  If you're in discussions about that, I would like to open source as much as possible.  So the answer was, you would like to make the artifacts public,  but this is a separate discussion and we will discuss it offline.  Just so it's clear that all the words match in my opinion.  Yep. I think Gregory would agree with that.  There was another question here.  Which use cases could you imagine for the pro-co-op information?  So the primary use case for the proof automation is that we want the code to be agile,  not in the development sense, but in the sense that we want to add new features.  We want to make changes. We want to make additions, new architecture port.  And we do not want to go through a lot of manual labor of fixing up the proof.  So we want to automate this as much as possible.  So the whole purpose of proof automation is to make the proof go through faster,  to make the proof less manual.  And I think we also have a plan to work a lot with academia on developing new tactics  to make the proof automation smarter.  So if anybody is interested in working in these areas, talk to Gregory.  Any further questions?  Okay. I think that's it. Thank you very much.  Thank you very much.
uk_nova_0_167.png uk_nova_168_1067.png uk_nova_1068_1883.png uk_nova_1884_4607.png uk_nova_4608_6071.png uk_nova_6072_9779.png uk_nova_9780_15755.png uk_nova_15756_16823.png uk_nova_16824_19919.png uk_nova_19920_23171.png uk_nova_23172_28007.png uk_nova_28008_30107.png uk_nova_30108_31463.png uk_nova_31464_32063.png uk_nova_32064_33563.png uk_nova_33564_34223.png uk_nova_34224_34271.png uk_nova_34272_34319.png uk_nova_34320_34439.png uk_nova_34440_34775.png uk_nova_34776_35087.png uk_nova_35088_35435.png uk_nova_35436_35963.png uk_nova_35964_36083.png uk_nova_36084_36395.png uk_nova_36396_36443.png uk_nova_36444_36731.png uk_nova_36732_36791.png uk_nova_36792_37151.png uk_nova_37152_37331.png uk_nova_37332_37487.png uk_nova_37488_37667.png uk_nova_37668_37919.png uk_nova_37920_38495.png uk_nova_38496_38543.png uk_nova_38544_38675.png uk_nova_38676_38735.png uk_nova_38736_38831.png uk_nova_38832_38915.png uk_nova_38916_39155.png uk_nova_39156_39371.png uk_nova_39372_39551.png uk_nova_39552_39623.png uk_nova_39624_39851.png uk_nova_39852_39899.png uk_nova_39900_39947.png uk_nova_39948_40223.png uk_nova_40224_41183.png uk_nova_41184_41891.png uk_nova_41892_41975.png uk_nova_41976_42371.png uk_nova_42372_42455.png uk_nova_42456_42539.png uk_nova_42540_43259.png uk_nova_43260_43559.png uk_nova_43560_44735.png uk_nova_44736_47891.png uk_nova_47892_51935.png uk_nova_51936_55367.png uk_nova_55368_62507.png uk_nova_62508_65147.png uk_nova_65148_65282.png