seL4 is the world's first (and still only real-world suitable) operating system (OS) kernel with a machine-checked, formal (mathematical) proof of implementation correctness. It has further proofs of security enforcement (the CIA properties of confidentiality, integrity and availability). It is also, the only protected-mode OS (as far as the open literature goes) with a complete and sound worst-case execution-time analysis, the key to supporting hard real-time applications.
Much has happened since I last talked about seL4 at FOSDEM 4 years ago, half a year after it had been open-sourced (GPL). In the meantime it has flown a full-size helicopter in autonomous mode while withstanding a cyber-attack (which easily succeeded when the chopper was running on Linux), driven autonomous trucks, and flown in space. It's in commercially developed security-critical systems in use in multiple defence forces and is making its way into commercial safety-critical systems.
Arguably, seL4's greatest weakness is a spartanic development environment and a paucity of components running on top, at the moment it's mostly BYO Ethernet driver and file system. We, the developers at Data61 have to accept some blame for that: we weren't sufficiently proactive in encouraging community contributions. Note that this was not because we don't want them, but simply because we were too busy.
We're in the process of changing that, in collaboration with the DARPA-funded US seL4 Center of Excellence, which is focussed on providing open-source tools and components on top of se4, but also provide development services to commercial users. On our end we are working on better documenting what is there, and what is maintained and by whom. We hope to encourage people to adopt existing userland components/tools and contribute further ones. A major enabler of this is a device-driver framework that defines driver interfaces and protocols. We hope to release this soon. The DARPA-sponsored first seL4 Summit held in Washington in Nov'18 with 140 attendees demonstrated the growing ecosystem and user base, including companies building frameworks for medical devices and autonomous vehicles. I hope this talk will also help to build the community.
On the research side, seL4 has made great progress in the past 4 years. It has been enhanced by a new scheduling model with capability-based control over time, arguably the first and only OS with a principled treatment of time as a resource, and the first able to support mixed-criticality real-time systems without sacrificing utilisation. This enhancement is presently undergoing verification, and lives in the MCS branch until verification is completed, after which it will become the mainline version.
The kernel's correctness and security proofs have grown to about 1 million lines (all open source) and have been maintained over ten years of evolution of the code base, now also including functional correctness on the x86 architecture. A RISC-V port is available and is undergoing formal verification as well. This is by far the larges, maintained proof base in the world, and has led to the new discipline of proof engineering to manage maintenance and evolution.
There is further work on pushing the mathematical guarantees into userland, especially the CAmkES component architecture and the Cogent language system, aimed at producing systems components (drivers, file systems, network stacks) that can be verified at a cost that is not far from that of traditional quality-assurance processes. Both frameworks are also open source (tools are GPLed while libraries are BSD). CAmkES is mature and in routine use for building secure systems, Cogent is still rapidly evolving, but is increasingly used by externals.
Finally we are working on ways for preventing information leakage through timing channels, considered an unsolvable problem by most.
