5 ms·
Great, cudos. They just seemingly discarded the part about peer-review. Where is the spec and the code? Given that I would believe this claim (which I don't) th
by udoprog 16y ago
Great, cudos. They just seemingly discarded the part about peer-review.
Where is the spec and the code? Given that I would believe this claim (which I don't) there has to exist means for independent third parties to verify this. Otherwise it's just a pissing contest in space.
- lsf 16y agoHere you go: http://ertos.nicta.com.au/software/seL4/ http://ertos.nicta.com.au/software/seL4/ Contains kernel and spec. Free for non-commercial use.
- limmeau 16y agoA peer-reviewed paper on seL4 on an ACM conference: http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_09.abstract http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEK... (I don't trust the Hindustan Times to get software verification details correct any more than I trust the Badische Zeitung to pick the right operation mode for a block cipher).
- udoprog 16y ago"The proof assumptions mean that there may be faults remaining in the kernel that could be classified as implementation faults below the level of C. They will not be faults that are properly visible on the level of the C programming language (which is our main claim of correctness), but they could still be serious faults that make the seL4 kernel misbehave." -- http://ertos.nicta.com.au/research/l4.verified/proof.pml http://ertos.nicta.com.au/research/l4.verified/proof.pml This just seems to be a case of someone running their mouth a bit too liberally and Hindustan Time jumping the gun. The actual project, which unfortunately is quite proprietary, has a much better overview of the whole ordeal. I would however like to se how their 1:1 strict C/haskell conversion actually looks (and why they decided against just modifying the something like the ghc :P). You were right in not trusting the paper.