The seL4 microkernel | Hacker News Reader

The seL4 microkernel

github.com

194 pointsgioele43 comments

Please note that the formally proven model has been implemented also in Haskell, not only in C.

Formally-proven-correct code + Haskell + literate programming = https://github.com/seL4/seL4/blob/master/haskell/src/SEL4/Ke...

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.

The original project home page is at http://ssrg.nicta.com.au/projects/seL4/ and the new page is at http://sel4.systems/

Downloads at http://ssrg.nicta.com.au/software/TS/seL4/

Thanks, the given link couldn't have contained less information if it tried

The FAQ[1] has a hell of a lot of info about what seL4 does and does not do.

[1] http://sel4.systems/FAQ

Which is not referenced from the linked article. What is the point of posting something with all but no information?

They should have submitted http://sel4.systems/ as the link, instead of the github link.

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.

Oh, I didn't realise the linked article wasn't the actual seL4 website.

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)?

It is out of date. The most of kernel is under GPLv2.

I think the OP was trying to point out that it officially got open-sourced today.

From http://sel4.systems/ :

"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.

Just found a great summary about what is proved to be secure and what is assumed: https://news.ycombinator.com/item?id=8100033

Can you explain why you are unsure the seL4 model is the best for a secure system?

I guess today _is_ another day.

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.

You should have a look at the literature on capability security, especially http://www.erights.org/elib/capability/duals/myths.html

There was hardly any computer security in the 1950s: it was before time sharing and networking. Your cynicism is over-done.

Something about L4 here: http://en.wikipedia.org/wiki/L4_microkernel_family

I hadn't heard about it before

The paper they published based on their findings, "Improving IPC by kernel design"[0], is pretty #cool and worth reading.

[0] http://www.scs.stanford.edu/nyu/04fa/sched/readings/l3.pdf

Maybe this is a bad place to ask, but why the virtualization requirement for running Linux on top? Is there for security reasons?

There are (have been?) other L4/Linux projects and they didn't require this.

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.

"The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement."

And as soon as one person makes a commit, that proof is invalid right?

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.

I sear this is like the sixth distinct solution I've seen claiming to be the first of those...

> I sear this is like the sixth distinct solution I've seen claiming to be the first of those...

Could you please name the other five?

I'm not so good at names. Let's see if Google can help me...

People have been talking about this stuff for decades. I found a paper from 1975 right in the top of my search results: http://csrc.nist.gov/publications/history/neum75.pdf. That eventually became PSOS.

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.

There was also HYDRA...

Anyway, there are lots.

There was a project way back when to port Darwin to L4: http://www.ertos.nicta.com/software/darbat/

along with the accompanying rumor that Apple would be “lifting” Mach's layer in XNU to run on top of L4. That was before the iPhone, of course.

I was always fascinated by the talks of L4 being specifically designed to avoid scrubbing your L1/L2 cache on operations such as IPC.

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 won't. See here: http://sel4.systems/FAQ/#verif

It's actually a very impressive piece of work, I can't wait to read about the details of how it was done.

Then go read http://www.nicta.com.au/pub?id=7371 :)

I don't suppose anyone has, or know where to find, a generated pdf of the extensive Latex documentation? My own pdflatex skills are failing me. :/

Conveniently enough, I just generated myself a pdf of it: [link redacted]

Thanks

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.

From the supported platforms it looks like it should work on a BeagleBone Black (arm, am335x, armv7-a, cortex-a8)--anyone been brave enough to try?

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.

Yep, they can either load from removable flash (microSD) or from onboard eMMC flash storage, selectable by switch on boot.

Students at UNSW doing Advanced Operating systems use a SabreLite board running seL4. They're pretty similar so you should be able to get it working.

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.

An OS that is proved to be essentially perfectly secure? For some reason this brings up thoughts of trusted computing, and not in a good way...

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.

From https://en.wikipedia.org/wiki/Trusted_computing:

> 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.

Reply on news.ycombinator.com