SeL4 Design Principles | Hacker News Reader

SeL4 Design Principles

microkerneldude.wordpress.com

146 pointssnvzz18 comments

Has anyone attempted attacking SeL4 seriously? What were the results?

Having some experience with formal verification, I have a deep mistrust of the proofs.

It is so easy to mistake a proof of the property you want with the proof of a property you've written, or even with a minor misstatement of the environment

I remember watching a talk where a formal methods researcher was talking about how, with the help of some grad students, they rebuilt one of Boeing's helicopter drone's flight control systems to use sel4 in a collaboration with DARPA. From memory the external security researchers could easily compromise the existing software, but failed to penetrate into the formally verified sel4 rewrite, even when they were given backdoor access to one of the subsystems as a helping hand. Every time they tried to escape the subsytem, seL4 would reboot them, leading the security researchers to say that it was the most secure flight control system they'd ever tested.

I'll see if I can dig it up - feel free to take it skeptically, I don't know how easy this experience was to reproduce. It was a pretty cool case study, however.

Edit:

This was the one! "Kathleen Fisher - From quadcopters to helicopters" https://www.youtube.com/watch?v=TH0tDGk19_c

Here's a mirror of an article from the ACM with more details: https://sudonull.com/post/3016

I believe this was the HACMS program. Data61 has some more information: https://ts.data61.csiro.au/projects/TS/SMACCM/

It may be worth mentioning that it isn't the kernel that rebooted the system but some monitoring thread.

I think one of the big things here is that the refinement proofs from the models for isolation, IPC fast path, capability access control, and scheduling to C source to binary are strongest when the kernel is built with a particular configuration on particular hardware. When all of these are satisfied and you are on a trusted platform, you have very very strong guarantees that what is modeled is what you get. But it's not like this is hidden. They have make it pretty clear what the verified platforms and configurations are[1].

You should take a look at the verification chain though[1]. It is fairly extensive. It's not like they proved just a small part of a system in a general way.

1: https://docs.sel4.systems/Hardware/

2: https://github.com/seL4/l4v

Even the non-formally-verified L4 operating systems are no fun to bughunt in. It's just a very clean, simple design without a lot of attack surface. You end up looking at what people build on top of it instead.

Yeah, that's by far the most likely. Note that one of Gernot's non-goals is "Stopping you from shooting yourself in the foot": this is to be taken seriously. The userland libraries provided by SeL4 have no proof evidence at all, and IME look and feel like any other C codebase. It's very likely that they the same class of security problems. Further, it's /very/ difficult to build anything on SeL4 without using said libraries (ease of use is another non-goal, remember?), so I'd expect many real systems to be built on them and thus share some class if issues among them.

I looked into SeL4 some years back for a potential project and along the way learned a reasonable bit about it. I recall that one of the things they were trying to do was to verify not just the design but that the compilation outputs match the designed outputs.

Yep... I’ve checked the site and confirmed my fuzzy recollections. https://sel4.systems/Info/FAQ/proof.pml has a pretty good summary that also has a nice TLDR explaining just what they are proving. “The binary code of the ARM version of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more.”

The RISC-V proof is very close to being completed too. Gernot talked at the RISC-V Summit 2019: https://www.youtube.com/watch?v=2IXBoVIUuVI

What the sel4 people have achieved is to separate a very small part of the OS and verify it (supposedly - there are some arguments over this).

But is the entire system secure if you use sel4?

Not necessarily. I fact it may be less secure than vanilla Linux because (1) you need to implement more yourself (2) the distributed approach makes your system more susceptible to certain classes of vulnerabilities (e.g. higher risk for race conditions) and (3) the sel4 security proofs apply to a very specific environment and usage and you could unknowingly break any one of them.

I haven't worked with L4, but have worked with other microkernels.

There are parallels between secure kernels and real-time kernels. If you randomly build a system on top of a real-time kernel, you don't have a real-time system. If you randomly build a system on top of a secure kernel, you don't have a secure system.

However, if you want to build a real-time system, and understand what that requires, you will use a real-time kernel (assuming you have use for a kernel).

If you use a verified kernel (or any component for that matter) and accidentally break the requirements for the security proofs, then you weren't going to be successful building a secure system anyways, because you aren't doing enough systems security analysis. If you are going to do the security analysis, the pre-existing analysis of your kernel is something you can re-use, and your analysis will include evidence that you have met the requirements for reusing that analysis.

Similarly in real-time systems if you use a real-time kernel but don't do some sort of time-based analysis (e.g. rate monotonoic analysis), you won't end up with a real-time system. However, those sorts of analyses are not possible with a kernel that lacks proper real-time features.

seL4 does very little, but it provides the fundamental pieces that a secure system can be built on; The capability model maps very well to this problem space.

Trying to build a secure system on a kernel that is not secure is a hopeless effort. An example such kernel is Linux, with over a million LoC running in supervisor mode. There's no use trying to make that secure. It only takes a single bug in Linux's code to compromise the whole.

Linux is not running millions lines of code, this is a very dishonest statement!

The Linux core is very small. The millions lines are mainly drivers and support for different architecture.

You can compile a minimal Linux kernel (there is even a kernel configuration for that) and put certain drivers in user-space. Still not as small as sel4 but quite close to it's commercial siblings.

> Linux is not running millions lines of code ... the millions lines are mainly drivers and support for different architecture.

But it's pretty easy to reach into the kernel and access buggy drivers and plenty of other non-essential kernel code (file systems, networking, SMB, etc).

> You can compile a minimal Linux kernel (there is even a kernel configuration for that) and put certain drivers in user-space. Still not as small as sel4 but quite close to it's commercial siblings.

But it still means that any exploit in driver code == total system compromise.

Even after configuring and building a linux kernel for your hardware, it's going to be over one megabyte object code.

What's dishonest is pretending it can be compared with a microkernel's, nevermind seL4, size.

It takes a lot to get a program up and running, since you have to do all the memory and capability setup. I always thought the most practical use for it was as a hypervisor, protecting your different VMs and having strict proofs for their communication and memory regions.

seL4 probably isn't the best target for an attack. Attacking the underlying hardware, or the application running on top of seL4 is going to be easier, as both of them is going to be more complex and likely to not be formally verified.

For "higher level abstraction layers" improving the "ease of use" mentioned in the article, see e.g. https://genode.org/ (not affiliated, just a fan)

And if you want to try it, it's a good time to, as they have just released a new version of Sculpt, a general-purpose system built on Genode.

Reply on news.ycombinator.com