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

51–60 of 65 posts

Re: Sel4: We’re going open source

#51

Post by dead10ck »

daveasdf wrote: post #34
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…

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.

Re: Sel4: We’re going open source

#52

Post by nl »

josephlord wrote: post #44
nl wrote: post #42

Earlier quoted context omitted.

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

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.

Re: Sel4: We’re going open source

#53

Post by hackuser »

deadgrey19 wrote: post #35
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 thr…

Thanks; I appreciate you taking the time.

Re: Sel4: We’re going open source

#54

Post by AlyssaRowan »

fsiefken wrote: post #29

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.

Re: Sel4: We’re going open source

#55

Post by aidenn0 »

pkaye wrote: post #49

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.

Re: Sel4: We’re going open source

#56

Post by a-saleh »

deadgrey19 wrote: post #35
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 thr…

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?

Re: Sel4: We’re going open source

#58

Post by psibi »

deadgrey19 wrote: post #35
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 thr…

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

Re: Sel4: We’re going open source

#60

Post by moblahbl4hblah »

deadgrey19 wrote: post #39
moblahbl4hblah wrote: post #22

Earlier quoted context omitted.

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.
Post reply on HN