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

11–20 of 65 posts

Re: Sel4: We’re going open source

#11

Post by willvarfar »

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?

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

Re: Sel4: We’re going open source

#13

Post by wglb »

regehr wrote: post #10
munin wrote: post #6

Earlier quoted context omitted.

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

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.

Re: Sel4: We’re going open source

#15

Post by mantraxC »

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.

Re: Sel4: We’re going open source

#16

Post by chubot »

regehr wrote: post #10
munin wrote: post #6

Earlier quoted context omitted.

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

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.

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

Re: Sel4: We’re going open source

#17

Post by TacticalCoder »

mantraxC wrote: post #15

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.

Re: Sel4: We’re going open source

#18

Post by regehr »

chubot wrote: post #16
regehr wrote: post #10

Earlier quoted context omitted.

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.

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

Re: Sel4: We’re going open source

#19

Post by Avshalom »

TacticalCoder wrote: post #17
mantraxC wrote: post #15

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

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

Re: Sel4: We’re going open source

#20

Post by webmaven »

All will be under standard open-source licensing terms.

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.

Post reply on HN