Sel4: We’re going open source
sel4.systems
Sel4: We’re going open source
1–10 of 65 posts
Re: Sel4: We’re going open source
#2"In short, the implementation is proved to be bug-free."
Has any smart person looked at their claims enough to vouch for them?
Re: Sel4: We’re going open source
#3"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.
Re: Sel4: We’re going open source
#4"In short, the implementation is proved to be bug-free." Has any smart person looked at their claims enough to vouch for them?
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.
Re: Sel4: We’re going open source
#5"In short, the implementation is proved to be bug-free." Has any smart person looked at their claims enough to vouch for them?
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:
Re: Sel4: We’re going open source
#6"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 par…
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."
Re: Sel4: We’re going open source
#7Is it too cynical to assume that a major defense contractor like GD has already integrated a hidden door for the NSA?
Re: Sel4: We’re going open source
#8This will be pretty exciting for anyone learning operating systems. More source to read.
Re: Sel4: We’re going open source
#9"In short, the implementation is proved to be bug-free." Has any smart person looked at their claims enough to vouch for them?
Comprehensive formal verification of an OS microkernel with complete PDF available for download
http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A...
Re: Sel4: We’re going open source
#10Earlier quoted context omitted.
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 par…
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.