Gernot Heiser | SeL4: Formal Proofs for Real-World Cybersecurity
AAllison DuettmannOct 19, 2021 at 10:38 am59min
S
00:00Speaker 1
Thank you for joining everyone. And welcome to foresight intelligent preparation group. Granted, I really can't tell you how long and how much and this group has looked forward and welcome to welcoming because whenever someone is asking me about concrete things that are implementable today, that could build Intelligent Systems of voluntary cooperation in something that would just something that this group is interested in, then something that comes to mind is SEO for and in this group, and in the company book draft, we will go from the premise that any desirable future will we be rely on computer security at every level, from hardware to operating system to software, all the way to the user interface. And, you know, it's essential for a variety of things, including de risking cooperation, but also preventing essential attacks for from automated autom automated webinars, mobile technologies, and so forth, things that we all discussed you in the past. So I think SEO boys, we need like a key, if you wish, for making sure that all of these technologies, amble well, and so we're really, really excited to have you here today. I'm very, very excited also to talk about perhaps I'm failing time, even how ncfr I will start with a regime attack with such a good rating that attackers couldn't even make progress on hearing out how to how to make progress on attacking so far. So thank you so much, everyone, for joining. And we look really much very much forward to presentation and to this session afterwards. So thanks.
S
01:31Speaker 2
Alright, so the SEO for microkernel is it's really about mathematically proving properties of a real world software system, in particular security relevant fonts. So what is SEO for? It's an open source, high assurance, high performance operating system microfil. So, kernel means it's the part of the software that runs in the most privileged mode of the hardware. And that implies if it gets compromised, and everything else is compromised, because the kernel there's no no protection against what the kernel that's operating system microkernel, meaning it's the core of an operating system. So you build an operating system on top of this grid. It's high performance, whoops, I claim it's the world's fastest microkernel. There's some partial evidence of that another complete proof. And it's high assurance. And this is really what what is SEO for is famous for in that it's the world, the operating system kernel with the most comprehensive mathematical vision story. And the cool thing, of course, is it's open source. So it's really available on the GitHub. And that doesn't apply only to the kernel itself to the code. But also the the proofs everything is open source. And such as 04 is arguably the most trustworthy foundation for building safety or security critical systems. And this is happening increasingly so people are deploying and CFO already in deployment or working on products that are going to be deployed across a very large range of domains, including automotive, which is presently apparently the holdest. area. avionics, space defense depends of causes where it's your hole was initially employed, mostly people deployed because they are the most security paranoid, IoT, industrial automation, everything. So it's, it's really taking off unnecessary, particularly the automotive sector. And we have this SEO Foundation, which was created the and a half ago, and it had a very strong influx of automotive companies this year, generally, companies operating on autonomous driving cars. And it seems like that's going to be the next big thing. In terms of performance. I said, there's a partial proof in the sense that there's some independent comparisons of performance only against open source systems. These are latency numbers. So smallest good and done by researchers in China, and we had nothing to do with they wrote several papers on using extra hardware support for improving microkernel performance. And they in the cause of that big comparison of SEO for performance against two other microkernels fiasco and Google circle. And you can see from these tables with between a factor of two and 10 pasta. So I and and I know that the non open source or many of the non open source systems, the performance is closer to that of Zircon than that of SEO work. And so I unashamedly make this claim. It's the world's fastest like brutal, and you can find the sources there. But what's important to understand is a microkernel is not an operating system. It's the Cool have an operating system. So in a microkernel based system, you have the TV, operating system services, which is includes storage systems, subsystems, networking, etc. General Resource Management. This is all contained in user level processes that are running side by side with the native applications. So from the kernel point of view, there's no principal difference between an application running on the system and an operating system service. They're all running at user mode unprotected by isolate isolated by the kernel enforce protection boundaries. And the kernels main job is really to switch between those domains, but also enable communication between them. And you can have virtual machines running legacy stacks. In most deployments of SEO for, we see that there's at least one virtual machine running a Linux Operating guest operating system to support the legacy stack and the critical bits running native on CFO.
S
06:09Speaker 2
And one of the not by far not unique characteristics, but the critical characteristic of SEO for is that it has a capability based access control. So capabilities are a abstraction for the managing access rights to objects, you can think of a capability like a key unboxer particular object, and security oriented operating system designs, general use capabilities. And of course, Mark Miller is part of your team. And he is one of the people who've been working in capability based systems for a very long time. So I assume the idea is familiar. And so what that means in ncfr, in particular is that any components that run off the on top of the SEO for microkernel can only communicate in any way if there is an explicit channel provided by that is access by capability. So if you have the capability to such a channel, then you can communicate and otherwise you cannot. So two components that do not have such a capability autolyzed channel are incapable of communicating. And this is called the key to the really strong isolate, not only isolation, but also the ability to enforce system wide security policies in SEO. in a way that's not possible in a system like Linux, for example, even even if the Linux was correct, there are free and safe which of course, it is not. So no communication on this explicitly authorized. That's a classical property of capability systems. But in ACL force case, it comes with the visual strengths that we know that the kernel by a mathematical proof, we know that the kernel will prevent complications if it's not explicitly authorized. And that gets me to what really defines SEO for its mathematical proof story. So SEO for is implemented in the C language. It's about 10,000 lines of code. And besides the C implementation, there is an abstract model. So that there is a description of the functionality of the kernel in a in a mathematical logic. And what we now i have is this proof of functional correctness, which means that the C implementation is a correct implementation of this abstract model. So in that very strict sense, the C, the implementation of the kernel is bug free with respect to this mathematical model of its functionality. And that's the thing that really made SEO famous It was the first time this was done for any operating system. This correct complete function correct the spirit from a mathematical model to the seed stage. That itself is a very powerful property because you know that the SEO implementation is correct against the more it still leaves you at the mercy of the compiler. And compilers themselves are complex species that are full of bugs. GCC for example, which we routinely use is probably a million lines of code all up it said also despite the proximity, and there is a risk of the compiler will introduce bugs in the compiled binary. And so we have various the proof that the C is correctly translated into the binary and by transitivity, we now know that the binary code which is the thing that actually executes on the silicon, Is this correct translation of the abstract all correct implementation of the abstract model. And I got my thinking out of order so that this comments that by now, the origin of functional correctness group was done 12 years ago. By now there's a few other operating system kernels with functional correctness proofs, they generally in the toy category, there's only one I'm aware of that sort of real world capable. The other side academic toys. But finally, what to me surprising the none of these are capability that is so sad, of course, you're still the only verified operating system kernel with capability based access control. And therefore this ability to reason about secure new foods meant in terms of security policies, etc.
S
10:51Speaker 2
And in particular, the least privileged properties are that every component on this given the access rights, it really needs to know more. Okay, so we have this proof chain from the abstract model down to the binary. That is extremely powerful, because it means you can do all through the reasoning at the level of the abstract model, which is much easier to reason about Dinah seep and the patient. But it by itself, it doesn't guarantee that the abstract model has right properties. And for that, we have through the proof chain on set of proofs from the high level security properties of confidentiality, integrity availabilities. So we have proofs that the colonel as represented by the abstract model is able to enforce the security properties. And again, this is before transitivity, we know that this property holds holds for the actual binary that executes on the silicon. Now, all of these proofs are machine checked. Generally using attractive theorem proving except their binary correctness proof is a tool chain, automated. And that's really important, because the, as I said earlier, the same limitations about 10,000 lines of code. The original functional correctness proof done on ARM v six posesses, was about 180,000 lines of proof script. And that just shows you that if those who have pen and paper groups, they would be completely worthless, because they would be more bugs in the proofs and in the code itself. Only by having these proofs machine checked down in this directive theorem, proving framework which does not allow you to make incorrect proofs. Does this all make sense. And by now this proof, the complete proof base we have for ACL core is well above 1 million lines of proof script. When we originated the functional correctness verse, it was considered the second largest proof ever done. It might be the largest by now, but it's certainly by far the largest maintained proof phase over an evolving system so far has changed a lot in 12 years, since we did the original verification, we keep evolving the kernel, because there is ongoing research to improve it to broaden its applicability. And while we're doing this, we follow we keep following with the verification, things are not allowed to be committed against into mainline, if they change, they break the proofs. So the proofs are being kept updated. And it does there's no other system of similar complexity in terms of proofs that has been evolving in such a fashion. There's a number of limitations still, then even after 12 years, we haven't verified the boot code of the kernel. And this is partially because the it's boring, it's batshit. As they say, in Australia. There's there's no, there's nothing interested it's just mind boggling engineering work. We've kept sort of students, best team members working on it in the background, but it's not complete. So someone would have to actually put money on the table to really compete that it's not a big deal to it's just yeah, we needed funded. And there's a few details that are not model to the same degree of faithfulness. So there's, there's some rather abstract models about the memory management unit and acacias in the system that are not done tied down to the instruction set architecture yet. Some of that has been is in principle, fixed or not in practice. There was a PhD thesis recently that explained how to do the formalization of the translation loop about sulfur, so the MMU so that could be integrated with his work. At the moment, we don't have funding or time for. And the we have the complete story for 32 bit ARM processors. For RISC five, we are close to having the complete proof story this is likely to happen later this year. And x86, which has type the functional correctness. And I forgot to put on this list multi core we have a high performance multi code limitation but no verification. So there is still work to be done.
S
15:30Speaker 2
The question is, so what does this really mean? So one is that, okay, we prove this functional correctness, that big kernel behaviors fully captured by the abstract model. And that means any further properties can be proved at the level of the abstract model. And that's a huge improvement because this is in the math, right mathematical logic, where it's much easier to work with. And in particular, explicitly, or implicitly, pretty much all the general attacks on operating systems are provably impossible in SEO for so there's never going to be an assertion failure in the verified kernel is the kernel provably doesn't be reference null pointers or initialized variables. No, I would have found access. So you can't run any stack smashing attacks on SEO for sidebar, it will never run out of resources, because it's called the verified resource management model. You can't fool it into doing stupid things by giving misformed inputs etc. So basically, the whole range of the typical attack vectors against operating systems are categorically impossible in SEO. So that's not. And it really important for us at the beginning, when we started this project, we did not want to use an academic toys people have been misleading in a way the world by doing verification on academic examples, and then pretending the scales and it didn't in the end, we wanted to build and verify a system that was capable for real world deployment right from the beginning, that was my target. And it worked. So it is already deployed primarily in defense systems in the real world. So this is a example of a secure communication device which people can't plug into a laptop that's deployed in various multiple armed forces. And it's approved for use hot dog secure, are classified as up to a classification secret. In terms of the SEO for microkernel, the redwoods scale to top secret but the packaging would have to be much more tamper proof or top secret device. There's this military cross domain destiel composite data that connects to networks of different classification that can be overlaid onto a single screen that's going into commercialization. Now, there is this device which is about to be deployed in a remote power generation station, which is designed for protecting critical infrastructure from cyber attacks. These are a number of products that I know of, and that I can talk about that are out there. And besides that, there's many more, which is your voice being signed into. And one important point about the real world usability was what we learned from the DARPA DARPA hackers program, where we worked with
S
18:51Speaker 2
project partners in the US on securing real world systems and the important thing there existing real world systems. So this is basically proving incorrect, the long held belief that the system has to be designed for security from the start. And it's impossible to retrofit security into the we disprove that in the heavens program. So what we did there, and as I said, most of the work was done by all of our collaboration partners. We worked with autonomous system both here craft as well as ground vehicles, and for each week had a research vehicle and a military vehicle. So the research vehicle for the autonomous aircraft was this off the shelf drone, where which basically we picked the airframe and replaced everything else. So this was a true green field design. And the land vehicle was this GVR board, which is the US Army, robotics reference platform. And they are we could basically play with completely replace everything. We wanted and write a lot of new code. So this was for developing the technology. And then there were the military vehicles. And these were vehicles that already existed. So they the area one is this unmanned littlebird, which is a standard helicopter airframe, which fully converted for autonomous flight. And that was already flying autonomously. And the on the ride, you have these US Army trucks, they are running around Detroit for ovilus. They also existing system and we retrofitted them for security. And the scary thing, even though these are military vehicles, the red team DARPA, hired as part of the project took about two weeks to completely compromised this military helicopter and be working with our partners. And they said the work was mostly non power partners, because the systems that export controls, we weren't even allowed to look at the code. So we can could only instruct them what to do. They retrofitted these systems to put them on to SEO for extract the critical components into protected sandboxes on SEO for leaving a lot of the legacy code and Linux virtual machines. And in the end, the the hackers couldn't compromise the systems anymore. We the red team was in April, he cabled to break the OB, we even gave them root access on one of the Linux virtual machines on the system. So they weren't on the platform had complete control over this Linux system, could plant fog bombs where they were they wanted, they could not affect the operation of the rest of the system. So that was a incredible success story that was playing way better than we had expected initially. So you can check us out. Seo four is not yet done. I indicated some of the holes that we still have insurance story. But there's still a lot of ongoing research and my own behind adding a little bit of that. One is that this is a success on the alpha program, where SEO for in the whole formal methods framework is being integrated in a repeatable system engineering poses. So these are avionics systems builders that they have, they have established processes and tool chains, etc. And the project partners in the davon case program are integrating Uc ofour and other formal methods into this standard engineering tool chains with the idea of scaling it to really develop knob scale, real world systems. So this is a very applied research, I would say. And then there is time protection, which is a principled approach for preventing climate change. So timing channels have been a are now pretty much mainstream started by the specter attacks, where they can compromise security in systems leading to loss of disclose of encryption keys, etc. With timing protection, tough with time protection, we are building abstractions, operating system abstractions, and tying them to hardware improvements that will allow to provably make timing channels impossible. And we already have working prototypes on that we have hardware improvements that show that this can the necessary changes to the hardware have minimal and no overhead both in terms of chip space as well as performance and runtime that allows us to actually do that and we're working on a formal proof that's on a conforming system, we can eliminate these tiny channels completely.
Get automatic meeting notes
Processing audio...