Re scalability of verification: you don't have to verify everything to get a massive security/safety boost. A well-structured system has a small trusted computing base (TCB), and if you get that right, your system can be pretty secure even if parts of the TCB remain unverified. Eg drivers and network stacks are outside the TCB if you encrypt all data, they can only threaten availability. This was just demonstrated pretty well with AMNESIA:33: for an seL4-based OS, it's just a minor issue, not a critical vulnerability: https://hensoldt-cyber.com/2020/12/08/how-amnesia33-does-aff.... This confirms my analysis from a few years ago, looking at critical exploits in Linux and how seriously they'd be in an seL4-based OS (hint: mostly not at all): https://ts.data61.csiro.au/publications/csiro_full_text//Big...
In a past life, I pushed hard for more investment in seL4 for certain defense applications. The nuance isn't to be underestimated though – I can say from experience that it's often a hard sell to folks that aren't already versed in the ins and outs of formal methods, security, kernels/operating systems, etc. There are plenty of lower hanging fruit (like networking hardware) than the applications I worked on, yet commercial adoption still seems low. Maybe this is due to that nuance. To the credit of the folks at Trustworthy Systems and UNSW, they've done a great job producing literature that outlines the business case in a manner palatable to decision makers. This paper [0] in particular came in handy to me many times.
We had very similar 'discussions' about using Ada (or other 'safe' language) and/or TCSEC rated systems for security sensitive systems in the 80s and 90s. With abundant rationales for why that was a good idea. We've ended up with (mostly) C/C++ and COTS OSes, hopefully dressed up with a STIG (or similar) to close the really blatant holes.
I don't think the market has reached the point where the overhead of these technologies has been offset by the pain of endless security incidents. I don't even think we're close to being willing to take on a 'better way (YMMV)' instead of 'move fast and break things (no matter the cost to the consumer)'.
What will it take for there to be a sel4 router/firewall I can build/buy? Anything directly connected to the internet needs these kind of security guarantees.
The two big things are a network stack that can act as a router (SeL4 has no network stack at all) and drivers. I;d imagine that a decent portion could be ripped from another open source operating system and run in userspace in SeL4 and get some benefits, but I'm not aware of any real effort to do that. Otherwise the usual way to use SeL4 as a hypervisor and just run linux under itm which gets you some benefits but probanly not the ones you'd want for a router to be as secure as possible.
This. Unfortunately, we haven't progressed much beyond Windows NT getting a TCSEC rating: first, remove networking. And then the floppy/cdrom. Then go down the list of other things you can't have.
Simpler versions of such devices exist, eg HENSOLDT Cyber markets a secure VPN gateway that is built on seL4. Over the years we've been in on-and-off discussions with vendors of networking equipment, it's always a battle between those in the company who take security seriously and those resisting any rocking of the boat. Having said that, we're presently in such a discussion again and it's looking promising so far.
However, it's entirely possible that someone has already done it and is not talking about it...
Is there a use case for a microkernel firewall? If you compromise just the tcp/ip stack, you can send and receive arbitrary packets, which is exactly what you would use a root exploit on a monolithic kernel to do.
> This whitepaper provides an introduction to and overview of seL4. We explain what seL4 is (and is not) and explore its defining features. We explain what makes seL4 uniquely qualified as the operating-system kernel of choice for security- and safety-critical systems, and generally embedded and cyber-physical systems. In particular,we explain seL4’s assurance story, its security- and safety-relevant features, and its benchmark-setting performance. We also discuss typical usage scenarios, including incremental cyber retrofit of legacy systems.
reading through the paper I made a couple observations that (to me) stuck out as a bit "opinionated":
(here they talk about seL4 capabilities which are different to <linux/capabilities.h>)
> The confused deputy problem is the “killer app” for capabilities, as the problem is un-solvable with ACLs. Hence, next time someone is trying to sell you a “secure” OS, not only ask whether they have a correctness proof for the OS, but also whether it uses capability-based access control. If the answer to either questions is “no”, then you’re being offered snake oil
bit before that there is also a "shout-out" to SELinux:
> While in some ways more secure than standard Linux, seLinux suffers from the same problem as standard Linux: a huge TCB, and correspondingly huge attack surface. In other words, seLinux is an add-on to a fundamentally insecure operating system and thus remains fundamentally insecure. In contrast, seL4 provides bullet-proof isolation from the ground up.In short, seLinux is not suitable for truly security-critical uses, while seL4 is designed for them.
and containers:
> A typical scenario is that a user wants to run an untrusted program (downloaded from the internet) to process a particular file but wants to prevent the program from accessing any other files the user has access. This is called a confinement scenario, and there is no clean way to do this in Linux, which is the reason people came up with heavyweight workarounds (I like to call them hacks)such as “chroot jails”, containers etc
some of it I think is justified if they see themselves competing for the hypervisor and hard RTOS markets.
Also they seem to distance themselves from Genode, which IMO serves a very different purpose (composability):
> Genode is in many ways a more powerful and general framework, that supports multiple microkernels and already comes with a wealth of services and device drivers, especially for x86 platforms. It is arguably more convenient to work with than CAmkES, and is certainly the way to get a complex system up quickly. However, Genode has drawbacks: 1. As it supports multiple microkernels, not all as powerful as seL4, Genode is based on the least common denominator. In particular, it cannot use all of seL4’s security and safety features. 2. It has no assurance story.
here a whole post by Norman Freske's in praise of seL4 back in 2016 (he is maintainer of Genode and did some talks that year at FosDem):
As much as I want seL4 succeed I wonder if they will reach critical adoption levels. One of the challenge in Linux is managing complexity of all these policies. SELinux done right is a continuous effort (and of course it's huge because user-space is huge). seL4 not even manages the memory for you, it's all in user-space (e.g. a Linux Guest OS). It's therefore a bit of a privileged statement and unfair comparison.
The "seL4 capabilities" and Linux (capabilities.h) are apples and oranges.
User-land Linux is a constantly moving target, you don't have that on a unique network or industrial appliance.
Imagine the tears (from users and maintainers) if Linux distributions started to enforce firejail policies and that every systemd.service file came with a correct list of "allowed system calls". No distribution would do that because the work involved would be massive and continuous and all but those who care about endpoint security would leave (what % would that be idk but I think it is massive).
Thanks for featuring my white paper. Some responses to some of the comments.
"Opinionated": guilty as charged. However, I claim that the opinions are well-grounded in fact.
Deployments: There are seL4-based devices in regular use in several defence forces. And it's being built in to various products, including civilian, eg critical infrastructure protection. And much we only hear anecdotally – that's open source...
i've been working on and off (mostly off) on https://robigalia.org/ for five years now, and interned with the sel4 verification team. feel free to swing by freenode#robigalia if you you want to chat sel4 or trustworthy software, there's a small group collected over the years that would love to answer your questions :)
What’s your opinion on the scalability of formal methods? Isn’t it still the case that basically formal verification is impossible to do for larger code bases (like at least 10-100x that of sel4 in lines of code) and even sel4 took many many years and experts?
current tools, verifying C code like seL4? never going to happen. but i'm hopeful about new techniques, things like the work Amal Ahmed http://www.ccs.neu.edu/home/amal/ is doing. you don't need to formally verify the entire codebase for basic properties like "can compose with the sel4 proofs" if your runtime/compiler/language/OS is all participating. right now you have to fight against the fact that none of the software of interest is well-understood mechanically by other software.
Thanks for posting. ~yearly I look at your site (idly, not likely to have anything to contribute) because Robigalia sounded very interesting when first discussed here at https://news.ycombinator.com/item?id=10848890
ty for the kind words! i'm hoping 2021 will bring a working demo of some basic goals :) the rust ecosystem has moved a long way since 2015, async/await finally being everywhere is a gamechanger because almost everything is async/await for us!
Really interesting to see progress on the provable correctness and security of software. Pages 11-12 state there is always an inevitable gap between the formal methods and the real world, but this nevertheless sounds a lot better than the hand-wavy, buggy C that gets written today.
In terms of security, the answer is a clear yes. Xen is kernel of 100+kSLOC of unverified code, while seL4 is verified. On top of that, Xen has Dom0 and thus a complete Linux system in its TCB.
What Xen has over seL4 is the management/admin framework.
But there is a project to port Qubes to seL4, waiting for the funding to be cleared.
Can't help thinking, though, that we will still need something for administration. NixOS would seem a better choice than Fedora 18 (or whatever Qubes is on) for that.
current users aren't very loud about it. RTI is implementing DDS for sel4. productionization is still early days. DARPA is pushing for it. you might look at the speakers, sponsors, and attendees of the sel4 conferences and workshops :)
Self driving cars via driveghost.com: "Ghost has assembled a team of leading experts in formal methods, an approach to software development that makes it possible to build complex software systems that can be proven to run without bugs or errors. Unlike existing systems built on error-prone platforms, Ghost will be the first to bring formal methods to the roadways with the world's only formally verified runtime built for your car, delivering you bug-free driving and unparalleled safety behind the wheel."
Seems like a dumb approach that only marketing would come up with.
The challenge is SDC is AI, not correctness of the kernel that the AI stack runs on. Is an SDC based on a formally verified OS but using logistic regression safe?
