Sel4: We’re going open source

http://sel4.systems/

by wglb • 12 years ago

185 62 12 years ago

sel4.systems

luckydude• 12 years ago

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

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

wglb2• 12 years ago

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.

munin• 12 years ago

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

mlinksva• 12 years ago

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.

cottonseed• 12 years ago

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

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

tommi• 12 years ago

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

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

willvarfar• 12 years ago

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

moblahbl4hblah2• 12 years ago

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.

deadgrey195• 12 years ago

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.

deadgrey195• 12 years ago

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.

sj4nz2• 12 years ago

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

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

deadgrey195• 12 years ago

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.

sj4nz2• 12 years ago

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.

UweSchmidt• 12 years ago

Love the default bootstrap theme <3

zmanian• 12 years ago

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

mantraxC• 12 years ago

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.

TacticalCoder• 12 years ago

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.

Avshalom• 12 years ago

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

webmaven• 12 years ago

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

StefanKarpinski• 12 years ago

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.

nl3• 12 years ago

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.

orbifold• 12 years ago

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.

daveasdf5• 12 years ago

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

hackuser2• 12 years ago

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?

pron• 12 years ago

Perhaps they've proven that privilege escalation is impossible.

hershel• 12 years ago

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.

deadgrey195• 12 years ago

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.

hackuser2• 12 years ago

Thanks; I appreciate you taking the time.

a-saleh2• 12 years ago

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?

psibi• 12 years ago

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

fsiefken• 12 years ago

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

AlyssaRowan• 12 years ago

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.

dead10ck2• 12 years ago

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

daveasdf5• 12 years ago

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.

dead10ck2• 12 years ago

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.

adamgravitis• 12 years ago

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.

nl3• 12 years ago

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

josephlord• 12 years ago

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

daveasdf5• 12 years ago

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.

rdtsc2• 12 years ago

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

daveasdf5• 12 years ago

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.

rdtsc2• 12 years ago

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.

pkaye• 12 years ago

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

aidenn0• 12 years ago

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.

anonymousDan2• 12 years ago

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

angry_octet• 12 years ago

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.

anonymousDan2• 12 years ago

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)

mkesper• 12 years ago

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?

Sel4: We’re going open source

Related Stories