Sel4: We’re going open source | Hacker News Reader

Sel4: We’re going open source

sel4.systems

185 pointswglb62 comments

This is an awful lot of fanfare for the open sourcing of something that was funded with public money by the government of Australia, using open source tools and technologies. Why isn't it already open source?

In general, I would like to see more software developed with public research funding required to be open source as part of the grant stipulation, ideally from early on. Too often tax-payer money is used to develop software which then ends up being closed source and providing profit to some commercial entity, instead of benefiting, you know, the people who payed for it – the public.

Why isn't it already open source?

Not sure if you are Australian or not, but - unlike the in the US - in Australia there is no assumption that publicly funded work will be in the public domain.

Generally the way it works here is that bodies like Nicta (and CSIRO) are expected to make a return on the investments that are made in them - ie, they are expected to make money somehow. The default way they do that is generally IP licensing.

Personally I think this is very short sighted, but it shouldn't surprise anyone.

This is why one of the best computational algebra softwares magma is only available for absurdly high prices, even though was developed as an academic project.

Yeah, Magma has some of the fastest known eimplementations of some esoteric algorithms. A lot of the core Sage guys seem keen on catching up to Magma, though, particularly originator William Stein who sort of decided to start Sage when his Magma license was taken away for political, not commercial reasons.

Just a little bit more on this: NICTA was originally set up as a research group by the Australian Government with the explicit mandate of commercialising its research.

The OKL4 and seL4 microkernels developed by NICTA were commercialised through the company Open Kernel Labs, which was subsequently acquired by General Dynamics (who thus acquired the IP of both projects).

At NICTA, we are very happy to see seL4 finally being open sourced: we really do want to see our work be used as widely as possible, and open sourcing it is going to be the best way of this happening. (So, in response to the grandparent thread, that is why we are making a big fanfare: we are excited, even if nobody else is.)

Will there be future work with Genode, e.g. is the codebase going to stay focused on ARM or will it also support x86?

http://genode.org/documentation/articles/genode-on-okl4

The seL4 kernel currently supports the ARMv6, ARMv7 and x86 architectures, though the proof only applies to ARMv6.

I am not sure what Genode's plans are. seL4 is a different kernel to OKL4, with a substantially different API, so it will be quite some work to move it across from OKL4 to seL4.

Could someone with expertise in this area share what is really meant by "end-to-end proof of implementation correctness and security enforcement", and the practical implications of it? The words suggest that the kernel is 'proven' to be absolutely secure, which obviously is false (and I don't think the authors are trying to make that claim). So what are the precise implications for confidentiality, availability, and integrity?

Perhaps they've proven that privilege escalation is impossible.

Here they describe it in detail:

http://ertos.nicta.com.au/research/l4.verified/proof.pml

Basically they plugged a lot of the possible holes, but it's not done yet.

Source: I have worked at NICTA, with the seL4 team, on the seL4 project, I've seen the seL4 source code and am (was?) a primary author of the user manual.

What they mean by this is that they have specified certain properties at a high level in a logical reasoning language they call HOL. These properties are things like the kernel will never reference a null pointer, or, the kernel will always run the next runable thread, or no application can access the memory of another application, or, a capability invocation will always terminate.

They then wrote a runable version of the kernel in Haskell (a purely functional language) and they have a mechanically checked mathematical proof that the Haskell code implements these features/properties. They then wrote a (nearly entirely) C implementation of the kernel and, under a relatively small set of preconditions, proved that the the C code exactly (no more, no less) implements the Haskell code, which implements these correctness and security properties.

A nasty side effect of this effort is that the C code is very strange, since it is more or less translated Haskell code, and the kernel code must necessarily be VERY small, about 10,000 lines of code, which is practically nothing for an operating system kerenl (it is a micro-kernel in the truest sense of the word). Another side effect is that the API bears almost no resemblance with "previous" versions such as OKL4.

Thanks; I appreciate you taking the time.

Man, I have so many questions :)

Why not just use the haskell version?

What did you use to check the haskell version?

What did you use to check that C implements what haskell implements?

Edit: I have read http://ertos.nicta.com.au/research/l4.verified/proof.pml, but I'd like to know more about tooling. Like, did you use agda, e.t.c?

I can't answer all of these questions authoritatively, as I have more of a systems focus than a formal methods focus, but I can hopefully point you in the right directions. The various published papers and final release will be the right places to find all the authoritative answers.

1) Why not use the Haskell version? The Haskell version was (is?) "executable", but it ran only against a hardware simulator, never against real hardware. Haskell has a complex runtime which is not (easily) suitable to run directly on Hardware (although one student I worked with did port a subset of the Haskell runtime to work on top of seL4). Using Haskell directly would be slow, and would require the researchers to prove the correctness of the Haskell runtime implementation as well which would be a huge amount of work.

2) What did you use to check the haskell version? I was not directly involved in this. I believe the Haskell used to write the kernel was a subset of the language, they call "literate haskell" which was used to both implement and specify the kernel. This was somehow minimally translated into a dialect of Isabelle called HOL.

3) What did you use to check that C implements what haskell implements? A similar process was used for checking that the C implementation was a refinement of the Haskell. Again, a restrictive subset of the C language a tool was written to translate the C code into HOL (I think). I remember the team lead arguing that the way the C implementation was checked, both the code itself and the translator could be checked for bugs.

AFAIK, The tooling was almost all custom except for relying on Haskell and the Isabel theorem prover. The group had a lot of experience for building and releasing the OKL4 kernel so a lot of the dirty work was already done as well as an excellent "Advanced Operating Systems Course" which whips and tortures undergraduates into systems engineers and ideally PhD students. :-)

Interesting.

I have already seen the approach "Lets design this in haskell and write production code in C" for http://cryptol.net/, but due to limited scope (mostly functions of several hundered bits input and output as customary in crypto-primitives), they were able to check that the implementation adheres to specification automatically. The aim was to allways know that the c code does what it is supposed to, so that programmer can focus on mitigating side-channel attacks :)

I wonder if something similar would be applicable to writing the micro-kernell.

Why not instead write a Haskell DSL which generates a C code for your requirements. ?

<blockquote>All will be under standard open-source licensing terms.</blockquote>

Hmm. Lumping together the mind-bogglingly broad variety of Free/Libre/Open Source licensing options as something 'standard' does not instill confidence.

That said, perhaps they are using something standard, like straight-up Apache, GPL, or BSD.

This will be pretty exciting for anyone learning operating systems. More source to read.

https://en.wikipedia.org/wiki/L4_microkernel_family

Beware, since the source is a translation of Haskell into C, this is not an entry level source tree and is not straightforward to read/understand despite it's small (LOC) size.

If so, it'll still be interesting to see what they've done with Haskell to make a secure operating system from the L4 model--I assume they are also releasing the Haskell source as well, otherwise there would be no point to it all.

There seems to be a lot of utility here for folks developing hardware based public key infrastructure like BitCoin wallets.

Beware of bugs in the above code; I have only proved it correct, not tried it.

https://en.wikiquote.org/wiki/Donald_Knuth

Anyway, here, the Haskell code should be considered the real source code, right?

Does "end-to-end proof of implementation correctness and security enforcement" mean there is zero change of a bug or security flaw?

No.

There may be a flaw in the security model that they correctly implemented.

There are bugs in every ARMv6 ever made, and some of them may allow crashes ore security vulnerabilites.

"In short, the implementation is proved to be bug-free."

Has any smart person looked at their claims enough to vouch for them?

It will be interesting to see once it becomes open source.

My favorite story relating to that is john regher compiler testing effort found a bunch of bugs in a research compiler that was proved to be correct.

[Edit]

Not strictly true. As John noted in comment below:

John Regehr (me) did in fact find something like 11 bugs in CompCert, most of which caused it to emit wrong code. But the bugs were not in the proved part.

actually that story is the opposite of true. John Regher and CSmith fuzzed CompCert and they found no bugs. from the csmith PLDI paper:

"The striking thing about our CompCert results is that the middleend bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task."

John Regehr (me) did in fact find something like 11 bugs in CompCert, most of which caused it to emit wrong code. But the bugs were not in the proved part.

My error.

Sounds interesting -- is there a paper that describes this?

I never wrote up all the details (which seemed somewhat mundane, since the bugs were in unproved code) but see Section 3.1 here:

http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf

Some discussion by smart people at http://www.eros-os.org/pipermail/cap-talk/2014-June/thread.h... ... probably have to wait til after it is open source end of next month to say.

You can download seL4 binaries and a copy of the specification (190 pages, no proof) here:

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

Comprehensive formal verification of an OS microkernel with complete PDF available for download

http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A...

(Mill team)

They have published details of their formal verification on ACM http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A...

They use Isabelle.

So whilst we haven't seen the proof, nor the code, will do have a good idea of what they've done and how they've done it.

Formal verification has been much researched, and its nice to see actual real systems starting to be checked by them. Just the other day I was reading about people doing TLS implementation verification using Coq.

From the paper "Comprehensive formal verification of an OS microkernel": "We still assume correctness of hand- written assembly code, boot code, management of caches, and the hardware"

http://www.nicta.com.au/pub?doc=7371

There's a lot of assuming going on...I'm not saying that what they've done isn't interesting, but as always don't let yourself get carried away.

To be fair. Every operating system assumes these things. At least the seL4 team has made this explicit. Secondly, there is a tiny amount of this code amounting to a few hundred lines of assembly and there are numerous verified hardware projects underway. Furthermore, as time has gone by, many of the original assumptions have been whittled away. This is by far the most robust operating system ever written.

Sure, I agree. There is indeed some work being done in making some of those parts more trustworthy. That being said, it will probably be sometime before that technology is usable by the average person. I'm really interested in seeing what they release.

Source: I have worked at NICTA, with the seL4 team, on the seL4 project, I've seen the seL4 source code and am (was?) a primary author of the user manual.

These claims have been peer reviewed in top formal methods and operating systems journals/conferences and have won some very awards doing so.

In short some very smart, and very qualified people can vouch for them.

Can anyone comment as to how feasible/practical it would be to extend these proofs to a multicore chip?

Very, very hard, if you mean kernel threads running in parallel. However, if the other cores run separate kernel instances (machine partitioning, separate memory and everything) that would be more achieveable. UNSW call this the clustered micokernel approach.

Thanks for that. Kind of what I expected. I wonder if the problem could be simplified if techniques from deterministic/stable multithreading could be incorporated somehow to simplify the formalization (http://dl.acm.org/citation.cfm?id=2566590.2500875)

This might become a good competitor for OpenBSD and the hardened linux.

Well, there's a lot of bits missing - this is a microkernel!

But I've seen seL4 before, and this is a very solid (if slightly weird-looking) foundation to work from.

I hope they choose a good licence; MIT or GPLv3 or GPLv2 or something. (It's a microkernel, so my general impression is GPL wouldn't be intended to spread between kernel components.)

This could be a QNX-killer. Eventually, one day, maybe a worthy replacement for OpenBSD or hardened Linux, but it's got a long way to go. It's ideal for anyone developing embedded hardware, however, and L4 variants are already very widely-used there.

Are you developing an open-source trusted security coprocessor? (I know at least two teams are.) Then this is probably what you want to run on it... of course, we'll want to check it ourselves as a community first, too, just in case.

Anyone from RTOS community know how this relates to INTEGRITY-178B ?

INTEGRITY-178B and seL4 are not related in terms of their source code or origin, though they do both aim at the same target audience (security and/or safety-critical systems).

I don't have a good knowledge of INTEGRITY-178B, but as far as I can tell some differences are:

* INTEGRITY-178B is a static separation kernel. seL4 can be used as a static separation kernel, but also allows for dynamic systems, for instance with processes being created and torn-down dynamically at run-time;

* INTEGRITY-178B has a proof that a model of the code satisfies particular security properties, while seL4 has a proof that the actual C implementation satisfies particular properties;

* INTEGREITY-178B is certified to EAL6+, while seL4 has not undergone any external certification process. (Without having a good knowledge of EAL6+, my suspicion would be that the code-level aspects of seL4 would meet or exceed EAL6+ certification, while the process-level aspects would need work on the seL4 side.)

If someone has worked with INTEGRITY-178B, please correct me if I have made any mistakes.

Thank you for responding that is a good description.

I remember someone from one of the government agencies gave a talk at in college many years ago about INTEGRITY-178B and about this separation kernel idea.

That was maybe 7-10 ago. The idea was pretty neat. And the claim was that the future will belong to more secure OSes based on this separation kernel (microkernel?). And how say every little component -- memory, filesystem, mouse, display are all in userspace. He talked about ok general purpose computer at that time were too slow to operate in that way (so Linux was better and winning because of performance). But just wait some 10 years or so and machines will be so fast that it won't matter.

So since then that story kind of stuck with me that kind of prompted the question.

Hmm, given how compilers & hardware can introduce incorrectness and security vulnerabilities in otherwise valid code, it makes you wonder if anyone can really claim "end-to-end proof of correctness" unless they include the specific compiler & hardware in their proof.

Concerning the compiler, in the link it is written:

"There is a further proof that the binary code that executes on the hardware is a correct translation of the C code. This means that the compiler does not have to be trusted, and extends the functional correctness property to the binary."

(I wonder how that works but it is related to your compiler concern)

Now even though the issue of hardware (say rogue hardware with rigged number generators and whatever backdoors) is probably a real concern, I still think that seL4 and its codebase where hundreds of bugs have been automatically found (and manually squashed) is a big step forward.

On that note: what even is a correct translation of C when it has so many undefined behaviors in it's spec.

What if the code doesn't rely on undefined behavior?

Absence of undefined behavior in the C implementation is of course one of the things covered by the seL4 proof.

They use a formally-specified subset of C described in Harvey Tuch's PhD thesis: http://www.ssrg.nicta.com.au/publications/papers/Tuch:phd.pd...

Love the default bootstrap theme <3

"In short, the implementation is proved to be bug-free."

This reeks of bull shit.

"We still assume correctness of hand- written assembly code, boot code, management of caches, and the hardware"

Sorry, I don't think you can claim you have a mathematical proof of the correctness of your kernel when you assume this much.

And where is this proof? I can't seem to find it anywhere on their web site. The only thing I can find is the publication

"seL4: Formal Verification of an Operating-System Kernel" http://ertos.nicta.com.au/research/l4.verified/pubs.pml

which looks like it just talks about the proof, rather than providing it. Am I just blind?

This looks interesting, but the confidence which they espouse is very suspicious.

This reeks of bull shit

The proof states that the C code of the kernel is a refinement of an high-level "abstract" specification of the kernel. This means that the C code only exhibits behaviours that are also exhibited by the high-level specification. The high-level specification (by construction) doesn't have certain bad behaviours that you often see in C programs: NULL pointer dereferences, buffer overruns, signed integer overflow, etc. Thus this class of bugs is proven to be absent. A good primer is available at: http://www.ertos.nicta.com.au/research/l4.verified/proof.pml

The original proof didn't make any claims about the high-level behaviour of the kernel, such as security. So for instance, the original kernel might have had a bug where you set up a system so that two processes shouldn't be able to communicate with each other, but after some unexpected sequence of API calls they form a communications channel between them.

NICTA in the following years after the initial proof carried out two security proofs: an integrity proof and an information flow proof. These proofs state that the capabilities possessed by a process determine (i) what other processes a particular process can modify; and (ii) what other processes the process can communicate with. Like the original proof, these security proofs (especially the second) have assumptions. In particular, they can only talk about parts of the system that are modelled. Timing channels, hidden CPU state, etc. not modelled by the proof may still allow information flow between processes, for instance.

Sorry, I don't think you can claim you have a mathematical proof of the correctness of your kernel when you assume this much.

You need to assume something. Every operating system kernel makes these assumptions: seL4 is just explicit about them. Some of the assumptions are bigger than others (management of caches is a pain to get right and hard to test, for instance). Some assumptions remain just due to a lack of time, such as proving the initialisation code of the kernel.

Additionally, as time has gone on the assumptions have been reduced. For instance, the work of Thomas Sewell and Magnus Myreen mean that the compiler no longer needs to be trusted: https://www.cl.cam.ac.uk/~mom22/pldi13.pdf

And where is this proof? I can't seem to find it anywhere on their web site.

The proof will be part of the open-source release. It consists of around 200,000 lines of Isabelle/HOL proof script, which is machine-checked. Anyone will be able to inspect/modify/check the proofs after the release.

This means that the C code only exhibits behaviours that are also exhibited by the high-level specification. The high-level specification (by construction) doesn't have certain bad behaviours that you often see in C programs: NULL pointer dereferences, buffer overruns, signed integer overflow, etc. Thus this class of bugs is proven to be absent.

The problem I take with the literature is that it does not say that it is free of certain classes of bugs. The wording implies that it is completely bug-free. As any software developer knows, bug-free software does not exist.

Furthermore,

You need to assume something. Every operating system kernel makes these assumptions: seL4 is just explicit about them.

they claim they have proven that their kernel is completely bug-free. They say they have proved this under the assumption that the assembly code was written correctly. It seems that what they have claimed is: we have proven our kernel is correct with a proof that assumes that the code is written correctly. The logical flaw in this is obvious.

I don't take issue with claims of correctness, given that they are precise about what they have proven. I do take issue with inflated claims ("bug-free" vs. "free of bugs from this specific class of bugs") for marketing purposes.

When people talk about proofs of correctness of software, they don't generally mean some bloke has gone and worked out on paper a formal proof. It means that they have used provably correct methods and then run the whole thing through an automated verifier.

It's not bull shit, it's just hard.

I'm not sure you are aware, but formal verification[1] is a well known and respected field of research. It does work, but it is hard to build practical tools using it. Nevertheless, if something is formally proven correct then for it to be incorrect one of three things must happen:

1) The proof is incorrect (which of course means it is no longer proven)

2) The prover has a bug (most proofs are done automatically). This is possible, but many of the same formal methods are used on the prover, and it is often build on a human-proved proof at the bottom.

3) Mathematics (the whole field) is wrong. This seems unlikely.

In reality, the problem with formally verified software is generally that it must interact with non-verified software (and sometimes hardware - although hardware can be verified too).

The wikipedia page[1] I referenced is worth reading.

[1] http://en.wikipedia.org/wiki/Formal_methods

4) It meets the specification but the specification is incorrect/specifies sub-optimal behaviour.

If you can fix that problem in the general case then you are about to be a very, very rich person.

The prover has a bug (most proofs are done automatically).

Minor point: while many formal verification projects are proven automatically, seL4 is proven in Isabelle/HOL which is an interactive theorem prover. This means that the proofs are actually carried out mostly manually. (The downside is that it takes much longer to carry out proofs; the upside is that you can prove far more sophisticated properties than is possible with the current state-of-the-art automated provers).

You are still right that the proof checker could have a bug, though. Proof checkers tend to be much smaller and simpler than things like SMT solvers, which helps increase confidence in them, however.

Reply on news.ycombinator.com