This link to the GitHub repository doesn't give a lot of the context about why this is exciting.
As others have mentioned, seL4 is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement." But for many years it was proprietary, and only available under commercial terms. The paper was published in 2009, so it's been five years that it was proprietary.
As of today at noon, the kernel was released under GPLv2 and userland under two-clause BSD. That is exciting.
Maybe they have automatic theorem prover running on Jenkins and they just refuse to merge changes which would be proven to be wrong? Anyway, I'm going to read more about what and how they did, it's fascinating to see a non-trivial software system proven correct.
Yes, that's how they did it. Quoting from the paper:
"Note that we have integrated all proofs into an automated proof checking suite, similar to an automated regression-test suite, but using machine-checked formal proofs instead of executable tests. This provides an automatic check, after each commit into the version control system, of the state of all the existing formal proofs, and identifies which specific portions of the proof must be re-established."
> Maybe they have automatic theorem prover running on Jenkins and they just refuse to merge changes which would be proven to be wrong?
Yes, that's the plan.
Internally this is how we have been operating since 2009, when the proof was first completed: You don't push a change to the verified kernel branch unless you are willing (or are able to convince someone else) to do the proof updates.
We don't yet have a regression website publicly available, but it's on the short-term roadmap.
There was also KSOS which had formal proofs both of the design and that the code conformed to the design.
There is a whole batch of TE based kernels that are descendants from Secure Ada Target/FLASK: SCOMP, LOCK, DTOS, Trusted MACH, TrustedBSD, and of course Sidewinder made a big deal about their firewalls using a provably secure kernel which was based on that work. The NSA even opensourced the Tokeneer project: http://www.adacore.com/sparkpro/tokeneer
Then there is MITRE, UCLA's DSU, AIM, etc.
I could swear there was at least once SELinux vendor that claimed it was providing the "only" provably secure kernel.
As others have mentioned, seL4 is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement." But for many years it was proprietary, and only available under commercial terms. The paper was published in 2009, so it's been five years that it was proprietary.
As of today at noon, the kernel was released under GPLv2 and userland under two-clause BSD. That is exciting.