It has proofs that verify its correctness.
It's time to get real about OS security
Aiden Phillips
Connor Price
where "fully" means "as far as the model we are using allows it."
Before side channels for example became a thing no one was thinking about them in their proofs. You cannot protect yourself against the unknown unknowns.
Charles Martinez
The security of such a kernel can be proven at all levels, even down to the fundamentals of security in terms of Confidentiality, Integrity, and Availability. It goes down to an abstract specification model (haskell I believe), then into its standard C/ASM implementation, with functional correctness checks done to ensure that it conforms. SeL4 even goes a step deeper and confirms the correctness of the translation from C to binary: that the compilation was done correctly and didn't create any inconsistencies.
As of now, this model does not account for system initialization, low-level MMU model, caches, multicore, and covert timing channels, but it does make the following provably impossible.
That's a lot more than you can say for other kernels. Others of this type tend to not only be slower, but offer no guarantees of functional correctness or translation correctness, no isolation of trusted/untrusted processes, only estimates for worst-case latency bounds, no guarantees of storage channel freedom, possibly a high timing channel prevention overhead, and limited mixed-criticality support
Carson Walker
Ya know, this sort of system would make a great hypervisor as well. It could run virtual machines and make IPC calls with them. With seL4's isolation, it would be secure as well, as it would keep the bloated, legacy code away from newer, more safely designed code.
Noah Reed
An interesting point that an user made here was about the military
That's because this stuff is actually already being used and researched by the Department of Defense's agency DARPA, as part of their High Assurance Military Systems Program. They can both retrofit their existing systems with this newer, more secure platform, such as with Boeing unmanned Little Birds or the US Army's autonomous trucks, as well as develop new technology such as drones and intelligent ground vehicle bots (which are kinda cute tbqhfam)
Cooper Gomez
Do remember that you don't prove things secure, but rather prove invariants hold. For example, we could prove that there are no buffer overflows or that superuser only functions can not be run by regular users.
Xavier Green
The examples section is where I'm a bit too brainlet to explain, but there is quite an interesting diagram here at third pic related showing how this virtualization idea from earlier plays into the design of a HACMS UAV. Certain components that haven't been implemented in a trusted manner such as camera and Wi-Fi are contained in a separated Linux instance, while others such as crypto implementation and drivers for radio and controller area network are run natively directly on seL4.
Jack Campbell
Putting it all together. This is true military-grade security, which is being worked on in the US, UK, Australia, and Canada.
Caleb Bennett
Contribution to seL4
Alexander Brown
It doesn't matter how secure OS will you do, because your (((Intel))) CPU has another CPU inside it with botnet closed operating system, that spies on you and sends your keystrokes to Israel