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'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
It may be worth mentioning that it isn't the kernel that rebooted the system but some monitoring thread.
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.
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.”
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.
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.
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.
What's dishonest is pretending it can be compared with a microkernel's, nevermind seL4, size.
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.
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.