5 ms·

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

wglb 12y 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 12y 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."
  - regehr 12y ago
    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.
    - wglb 12y ago
      My error.
    - chubot 12y ago
      Sounds interesting -- is there a paper that describes this?
      - regehr 12y ago
        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 http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf
mlinksva 12y ago
Some discussion by smart people at http://www.eros-os.org/pipermail/cap-talk/2014-June/thread.html#16120 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 12y 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/ http://ssrg.nicta.com.au/software/TS/seL4/
tommi 12y ago
Comprehensive formal verification of an OS microkernel with complete PDF available for download http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A...
willvarfar 12y ago
(Mill team) They have published details of their formal verification on ACM http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml 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.
blahbl4hblahtoo 12y 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 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.
moblahbl4hblah 12y 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 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.
- deadgrey19 12y 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.
  - moblahbl4hblah 12y ago
    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.
deadgrey19 12y 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.

wglb 12y 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 12y 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."
- regehr 12y ago
  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.
  - wglb 12y ago
    My error.
  - chubot 12y ago
    Sounds interesting -- is there a paper that describes this?
    - regehr 12y ago
      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 http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf

mlinksva 12y ago

Some discussion by smart people at http://www.eros-os.org/pipermail/cap-talk/2014-June/thread.html#16120 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 12y 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/ http://ssrg.nicta.com.au/software/TS/seL4/

tommi 12y ago

Comprehensive formal verification of an OS microkernel with complete PDF available for download http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A...

willvarfar 12y ago

(Mill team) They have published details of their formal verification on ACM http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml 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.

blahbl4hblahtoo 12y 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 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.

moblahbl4hblah 12y ago

deadgrey19 12y 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.
- moblahbl4hblah 12y ago
  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.

deadgrey19 12y 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.