seL4 is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement" originally developed (as far as I know) at UNSW, further developed at NICTA.
This is excellent. While I'm still unsure about the seL4 model being the best for a secure system (a topic for another day), it's wonderful to see this development.
I hope "someone" will port this to RISC-V (32- or 64-bit).
Is http://ssrg.nicta.com.au/software/TS/seL4 out of date or is the license really not open source (OPEN KERNEL LABS and National ICT Australia Limited (Licensors) NON-COMMERCIAL LICENSE AGREEMENT)?
"General Dynamics C4 Systems and NICTA are pleased to announce the open sourcing of seL4, the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. It is still the world's most highly-assured OS.
What's being released?
It includes all of the kernel's source code, all the proofs, plus other code and proofs useful for building highly trustworthy systems. All is under standard open-source licensing terms — either GPL version 2, or the 2-clause BSD licence.
When is it happening?
The release happened at noon of Tuesday, 29 July 2014 AEST (UTC+10), in celebration of International Proof Day (the fifth aniversary of the completion of seL4's functional correctness proof)."
EDIT: The original link should probably be updated to http://sel4.systems/ as it has the link to the Github page prominently displayed there.
The fundamental issue is that, IMhO, security classification needs to be attached to the data at the lowest level -- OS level is simply to coarse. Take for example an encrypted channel. At the OS level the channel is treated opaquely whereas at the programming language level, after decryption the authenticated data can be assigned both a different level of secrecy and trust, and it can be data dependent. Strong type systems can ensure that secret data is never accidentally leaked, nor untrusted data used in a trusted context. (For a real-life simple subset of this, see tperl).
It may be possible to build such a system on top of seL4, but seL4 isn't sufficient.
I do intend on working on this eventually. Incidentally, D. J. Bernstein recently shared a similar complaint about the state of security - the models we use have practically not advanced since the 1950es.
I'm not sure who submitted the link (I don't think it was anyone from the seL4 team), but I inserted the http://sel4.systems/ link into the repo's README file, which will hopefully help a little.
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.
Can someone explain to me what it means for a kernel to have an end-to-end proof of implementation? Does it just mean that the kernel is implemented bug-free? That it will never panic?
It's great to see more and more stuff come out of NICTA. For those who are unaware, it is a government funded research institution in Australia. A big difference from other research institutions is that they are especially focussed on commercially viable research (rather than purely theoretical stiff - although I'm sure they do some work on that too). It is a model that has been used for quite some time on Aus, with the CSIRO doing the same thing for more general (I.e. not specifically ICT) research. The CSIRO has done some beautifull research which forms the backbones of technology such as WiFi. So, putting aside recent budgetry and financial issues, it is great to see stuff like this being released by them. Here's to many more years of fruitful research.
AFAIK the beaglebones load their entire executable environment, including bootloader, from removable flash media - there shouldn't be any bravery required to test out experimental software (even bootloaders and firmware) because you can always just swap out the entire card. There's no bricking them.
Is there any recent benchmark of an L4 implementation with servers compared to a modern monolithic Linux or *BSD kernel? I'm still thinking there's huge untapped potential in microkernels and I wonder how the "state of the art" stacks up against modern monolithic kernels on processors with a lot of cache.
You seem to be misunderstanding the kind of security this is about. It's not about taking away control by the owner, just about preventing ways of control by third parties that you as owner didn't intend to give.
> TC is controversial as the hardware is not only secured for its owner, but also secured against its owner.
Whereas here if you're not happy with what the OS does, you can wipe it and still have full control over the hardware. And the OS is OpenSource, accessible to the hardware owner to modify if some kind of control it asserts isn't satisfying.
Not the parent commenter, but: A proven kernel could be seen as taking control away on devices where root access cannot be legitimately obtained. I guess some might perceive it as scary given many people in tech circles root their phones (and similar devices), when root access is normally obtained through OS-level security bugs, and it is often (though I think somewhat decreasingly?) used to install third-party OSes on such devices.
Agreed, although the blame then still lies with the device the secure kernel is running on, or the company that produces it, or the client for choosing to buy it.
I guess you can say that proven software is power, and power can be misused.
Formally-proven-correct code + Haskell + literate programming = https://github.com/seL4/seL4/blob/master/haskell/src/SEL4/Ke...