10 Years SeL4: Still the Best, Still Getting Better
microkerneldude.wordpress.com
microkerneldude.wordpress.com
Obviously, formally verifying a modern web browser with a javascript engine and everything is a whole other undertaking, so I'll leave that aside. But the notion of using a very secure kernel as the base OS is appealing. Even if a hostile site broke out of the web browser, SeL4 should keep it sandboxed. Presumably, SeL4 could enforce isolation between different browser tabs. Is this something we can look forward to in the future, or are the performance expectations of modern javascript heavy web sites out of line with what SeL4 is likely to deliver?
Anyway, there are plenty of other applications beside the web, so glad to see that SeL4 is being used in real world deployments.
(One exception to this is QNX which was killed off by weird business decisions.)
Or the new userspace device driver model introduced by Catalina. As per WWDC, for every new user space driver API, the old kernel one will be automatically marked as legacy and removed after one OS release, with the long term roadmap to replace all the kernel API extensions.
Just like Windows 10 increases the amount of sandboxing with each bi-annual release.
Its a step forward in kernel upgradability, but it also takes the pressure off vendors like Qualcomm and ARM to upstream their patches. I hope the kernel continues making significant changes that break out of tree, proprietary drivers.
The harder it is for these players to act in bad faith, the sooner they'll collaborate with the kernel developers and mainline their code.
And as proven by FOSS drivers that eventually got purged from kernel tree, having source available is meaningless if everyone just lets the code rotten to the point of being purged.
As for pressuring vendors, the source code is available, and the license allows them to never upstream, it isn't as if Joe and Jane know what that is when buying a new phone.
Two. Linux? Who's counting anyway.
Eventually the community will write their own drivers (as has happened with Mali) and the respective vendor will have a reckoning internally (like what happened with AMD's GPU driver) whereby those advocating for wasting money on out of tree code leave the organization with egg on their face for bilking the company out of significant R&D cash.
It is very hard to claim that its worth it to develop a proprietary driver when a comparable performance driver already exists for your hardware in-tree. The in-tree driver will almost certainly be easier to use & break less often than out of tree code that the kernel devs don't think or care about breaking.
Are you sure? The latest version is only ~2 years old, and they still seem to be hiring: https://bb.wd3.myworkdayjobs.com/QNX
https://news.ycombinator.com/item?id=9962444
One or more might be integrated into seL4. Alternatively, components in something like IBOS might be done with higher assurance like seL4 or Muen.
Running a web browser directly on a microkernel is a reasonable thing to do, and it's likely that Fuchsia will end up doing it, but it will involve a lot of work.
The performance expectations of JS generally do not have anything to do with the operating system, but as explained in the post, when it comes to fundamental OS services, seL4 is more than an order of magnitude faster than even other microkernels, much less FreeBSD, Linux, or Microsoft Windows.
Microkernels generally need higher performance for those things because operations such as read(), which involve just a system call on a monolithic kernel, with context switches into and out of the kernel, involve a full context switch to a separate server process and back on a microkernel.
This seems to imply that seL4 is faster than FreeBSD, Linux, Windows is this what was intended to be conveyed?
That said I don't think data exists to show that SeL4 is faster than mainstream OS kernels just much faster than research microkernels which have always been much much slower than mainstream monolithic kernels.
In fact one would reasonably suppose that it would be measurably slower due to increased overhead. This may well be well worth it but this doesn't mean we ought to engage in speculation not backed by data.
The way that microkernels are sometimes slower is, as I said above, on operations that monolithic kernels implement internally, but microkernels leave to userspace processes. For example, ping-pong IPC is something you can measure on L4, and reliably get orders of magnitude better performance than on Linux. But creating a file isn't, because L4 itself doesn't have files—you can implement them in userspace, and that can be done with varying degrees of extra overhead. It might still come out about even with Linux (I think I've seen some results to that effect) but it probably won't be orders of magnitude faster.
The part of your comment I agree with is that measuring performance is complicated.
Seems to be a pretty broad claim without anything to back it up.
First, by omitting the immediately previous qualifier from your quote: "when it comes to fundamental OS services, seL4 is more than an order of magnitude faster...". This omission turns my correct claim into a plausibly false one, one which I have specifically disclaimed, in detail, in three separate comments in this thread already, in order to avoid the kind of confusion that could reasonably produce reactions like yours. The "benchmarks of software performing an actual useful task on both a mainstream OS and SeL4" you ask for are relevant to the plausibly false claim, but not to the correct claim I was actually making.
Second, you falsely claim that I am saying things without anything to back them up. This would be a legitimate criticism if I were talking about performance numbers for some kind of trade secret software, but in fact (with the exception of Microsoft Windows) all of the operating systems discussed here (seL4, FreeBSD, Linux, plausibly Fiasco.OC and Mach) are open source and have abundant published benchmarks, including many in the seL4 papers published by the dude whose blog post we are discussing. There is a very great deal of freely available evidence.
In short, you are lying about what I am saying, and you are lying about the available evidence for evaluating its veracity. Therefore I think the presumption of good faith on your part in this conversation can be soundly dismissed.
I'm not lying about what you said. I even copied the longer section of your quote in the prior post aside from the entire thread being right above on my device and yours.
I'm also not lying about the availability of evidence to prove your claim just asking you to provide a link to such.
You spoke with authority and then get upset and wave your hands about yelling LIAR when asked for supporting links.
Perhaps begin again respectfully or cease discussing.
Also, I would like to know why Google didn't go for seL4 and instead created Fochsia?
I wanted to mention that we wanted to see if we can use L4 for isolating our network filter from Linux kernel (trustability) but instead we opted for bitvisor (much simpler code base but not verified).
We have a little operating system, or enough of one to facilitate building the rest of our product atop of it, that goes along with seL4. We'd planned to open source parts of it fairly soon, but prioritizing hiring a few more folks (BD, PM, Eng.) has put that effort on-hold temporarily.
Building things with seL4 is easy to do wrong, despite being given a variety of very low-level verified primitives to work with. You still need to put it all together just right. CAmkES is supposed to make this easier, but our experience with it wasn't very good, so we took the hard road and created a Rust-based application framework to go over the top of everything.
This was our main stopper. seL4 would benefit greatly to teach how everything can be fit together, and where everything can be expected to go.
Basically by providing setup, resource management, and communication abstractions that you just can't get wrong because doing something dumb that would be entirely nuts and/or would result in difficult to deal with run-time errors (as the kernel enforces some of its guarantees) ends up being rejected by the compiler ahead of time.
We have some self-driving car customers, but that's just because they're gluing together really complicated systems from lots and lots of diverse components, so they're great use cases.
Our goal is much broader scoped beyond AV and is more akin to creating new classes of CAE tools for SISoS & CPS designers/engineers.
"Can you build actual systems with it?" https://www.youtube.com/watch?v=lRndE7rSXiI&t=22m
The whole talk is well worth a watch.
I am not aware of any other capability based and verified micro kernel in level of [se]L4.
But Google may have other reasons to reinvent their kernel (though they're not starting from scratch; Zircon evolved from the Little Kernel by Travis Geiselbrecht). They may have decided that the flexibility of inventing a new microkernel for their exact requirements and moving fast with it would be more productive than reusing an existing one. Building on the careful verification process of seL4 is presumably quite time-consuming, and might get in the way.
When NeXT/Apple started using the Mach kernel, it ended up being heavily rewritten to support Apple's requirements, and they never adopted the microkernel design. Google may have seen a seL4 dependency as being a similar kind of burden.
seL4 is also GPLv2, I believe. Might also be a blocker for Google.
It will probably be like any other modern OS, but designed to be a modern OS from the beginning.
Which might save Google 0.1% in electricity costs.
Unlike the current situation with the Android ecosystem right now, where a newly released product is lucky to get even a few security updates in a year or so, and have effectively had support dropped after that.
Compare that to the ChromeOS ecosystem, where Google guarantees 5 years of support from the time the first production on a platform was released.
I don't think they only wanted to reinvent the wheel and I don't think trustability was one of the motivations of their design!
"Another fork of L4-embedded is what now runs on the Secure Enclave of all Apple iOS devices."
All Apple iOS devices is pretty big.
There is hypervisor support, sort of. Insofar as there's enough there to build your own hypervisor (we ended up needing to do something like this), and there's a sample VMM for a very specific host and guest target combination available that's created via CAmkES.
Making an seL4-based hypervisor truly cross-architecture capable as well as generalizable for different host and guest target configurations is a non-trivial, painstaking, arduous task. In fact making anything on seL4 truly cross-platform isn't easy. The kernel doesn't provide much in the way of unifying abstractions over the architecture differences. The different architecture details are mostly thrust onto you to figure out what kind of abstractions you want to make.
The MCS (mixed criticality support) stuff in seL4 getting mainlined should make it theoretically possible to invent/create a hypervisor that enables you to run MCU oriented RTOSes & applications in an isolated context atop non-HRT hardware. Data61 has mentioned that they're going to take a whack at making some part of an AUTOSAR stack that runs in a context like this, but I have no idea how far along that is. Separately, we're looking at leveraging the same underlying capability for a variety of different adjacent purposes.
That said, there are a variety of supported platforms you can already build seL4 for: https://docs.sel4.systems/Hardware/, our experience has been that some work better than others. It's possible to run in QEMU as well to get started.
It even has proof of worst case time (WCET), which to my knowledge no other non-trivial RTOS does have.
I'm very confused now.
Keeping in mind I'm not an expert on this, I dug up these papers when I was vaguely looking, they may be useful to you:
"Improving Interrupt Response Time in a Verifiable Protected Microkernel" https://ts.data61.csiro.au/publications/nicta_full_text/5391...
"To Preempt or Not To Preempt, That Is the Question" http://ts.csiro.au/publications/nicta_full_text/5859.pdf
Thus interrupt latency is guaranteed to be very low, even if the interrupt happens while the microkernel is running.
It is my intuition that the "it's not a RTOS" has to come from something else, like some non-implemented API that's expected in an RTOS or the like. The required services might actually be implementable as non-privileged tasks.