51–60 of 151 posts
I haven’t fully given up on the hope that a fully verified kernel eventually catches on. It would be basically impossible to verify all of Linux at this point, but I could see seL4 eventually getting traction in something like the smartphone market. A guy can dream, at least.
But to my knowledge, not for the more general user facing OSes.
Earlier quoted context omitted.
Any government can get RCE on any OS with the change in their couch. Formal verification of process isolation is REALLY important when lives depend on it. That's a huge value add! My main concern is speed and the lack of capability based security. seL4 is faster than Linux by a mile and I'm guessing that this is much slower. You can put a POSIX layer on seL4 but POSIX is inherently flawed too. MAC separates privilege…
> Any government can get RCE on any OS with the change in their couch. Do you really believe that? That seems extremely implausible based on just simple observations like all governments using COTS OS for military/intelligence work or standard OS:es being used for critical infrastructure like power/water/finance/transportation. If your statement was even remotely true then why is this not used in conflicts to devasta…
> If your statement was even remotely true then why is this not used in conflicts to devastating effect?
It has been, it continues to be.
Where have you been?
Building new operating systems seems so ambitious to me. Radiant Computer ( https://radiant.computer/ ) was also recently posted. What other exciting projects like these exist?
LionsOS[1] is its static scenario building framework, with some dynamic scenario support.
Genode[2] is an independent OS construction kit that can also use the seL4 kernel. Their general purpose OS, Sculpt, just had a very interesting multi-kernel release[3].
The systems group at ETHZürich is building Kirsch[4], an effort with seL4 and CHERI.
Managarm[5] is also building something of interesting architecture with some Linux software compatibility.
1. https://trustworthy.systems/projects/LionsOS/
3. https://genodians.org/alex-ab/2025-11-02-sculpt-multi-kernel
SPARK’s “ask about pricing” stickers indicate this is “free” software that’s a different kind of free.
Commercial support is not free, and the pricing for that is almost always something you have to ask for. Hard to see how this is piece of free software stands out.
I haven’t fully given up on the hope that a fully verified kernel eventually catches on. It would be basically impossible to verify all of Linux at this point, but I could see seL4 eventually getting traction in something like the smartphone market. A guy can dream, at least.
There is an NDA related company called ironclad as well. Beware the trademark/copyright terrorists. That said, I am huge fan of works like this. But in practice, the security layer that betrays all of this tends to be the firmware layer. My dream is to have something like the Framework computer use verifiably secure EFI firmware, as well as similarly verified and audited firmware for every hardware component.
As far as I know formal verification is another testing method and as as such it's is as good as the quality and the extent of the "verification" (aka tests).
Best way to verify that I know of is Fuzzing + testing.
Earlier quoted context omitted.
> Any government can get RCE on any OS with the change in their couch. Do you really believe that? That seems extremely implausible based on just simple observations like all governments using COTS OS for military/intelligence work or standard OS:es being used for critical infrastructure like power/water/finance/transportation. If your statement was even remotely true then why is this not used in conflicts to devasta…
Yes, I believe that. > If your statement was even remotely true then why is this not used in conflicts to devastating effect? It has been, it continues to be. Where have you been?
"Formally verified" what does that means? As far as I know formal verification is another testing method and as as such it's is as good as the quality and the extent of the "verification" (aka tests). Best way to verify that I know of is Fuzzing + testing.
It is a method where a computer verifies a proof that the program adheres to its specification for _all_ inputs (subject to whatever limitations the particular method has).
Types are the simplest kind of formal verification, and with sufficiently advanced dependent type-systems, can be used to prove that programs obey arbitrarily complex specifications. However, this can be extremely laborious and requires significantly different skills than normal programming, so it is very rarely done in industry