Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Sel4: We’re going open source

sel4.systems

Post reply on HN
Print view View original

31–40 of 65 posts

Re: Sel4: We’re going open source

#31

Post by orbifold »

nl wrote: post #30
StefanKarpinski wrote: post #24

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 devel…

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 genera…

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.

Re: Sel4: We’re going open source

#32

Post by jordigh »

orbifold wrote: post #31
nl wrote: post #30

Earlier quoted context omitted.

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 genera…

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.

Re: Sel4: We’re going open source

#33

Post by dead10ck »

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

Re: Sel4: We’re going open source

#34

Post by daveasdf »

dead10ck wrote: post #33

"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 fi…

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.

Re: Sel4: We’re going open source

#35

Post by deadgrey19 »

hackuser wrote: post #26

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…

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.

Re: Sel4: We’re going open source

#36

Post by daveasdf »

nl wrote: post #30
StefanKarpinski wrote: post #24

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 devel…

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 genera…

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

Re: Sel4: We’re going open source

#37

Post by deadgrey19 »

sj4nz wrote: post #8

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.

Re: Sel4: We’re going open source

#38

Post by deadgrey19 »

luckydude wrote: post #2

"In short, the implementation is proved to be bug-free." Has any smart person looked at their claims enough to vouch for them?

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.

Re: Sel4: We’re going open source

#39

Post by deadgrey19 »

moblahbl4hblah wrote: post #22
luckydude wrote: post #2

"In short, the implementation is proved to be bug-free." Has any smart person looked at their claims enough to vouch for them?

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.

Re: Sel4: We’re going open source

#40

Post by adamgravitis »

dead10ck wrote: post #33

"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 fi…

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.

Post reply on HN