5 ms·

The issue here is the spec - no runtime errors at the source code level is, as I understand, a completely different specification than end-to-end implementation

The issue here is the spec - no runtime errors at the source code level is, as I understand, a completely different specification than end-to-end implementation correctness. In particular, the Muen Kernel report itself [1] explains: By implementing the kernel in SPARK and proving the absence of runtime errors, we have shown that the kernel is free from exceptions. While these proofs provide some evidence to the correctness claim of the implementation, the application of these particular formal methods do not provide any assurances beyond the error free execution of the kernel. Proving functional properties such as the correspondence of the scheduler to a given formal specification is necessary to further raise the confidence in systems based on the Muen kernel. In other-words, we don't yet have formal confirmation that this thing actually does what we might expect it to - just that its execution is bug-free. [1] http://muen.codelabs.ch/muen-report.pdf http://muen.codelabs.ch/muen-report.pdf

eternalban 11y ago
Exactly. It is exactly equivalent to saying that if a strict FP program compiles it is "bug free" but of course it has little to say about whether the code is 'correct'.
vilhelm_s 11y ago
But in the other direction, it seems that end-to-end implementation correctness implies absence of run-time errors. The seL4 authors write[1]: > IMPLICATIONS [...] a functional correctness proof already has interesting implications for security. If the assumptions listed in Sect. 5.5 are true, then in seL4 there will be: No code injection attacks [...] No buffer overflows [...] No NULL pointer access [...] No ill-typed pointer access [...] No memory leaks [...] No non-termination [...] No arithmetic or other exceptions [...] No un-checked user arguments [...] Aligned objects [...] Wellformed data structures [...] And this was already done in 2009. So I don't think Muen is the first microkernel to prove absence of run-time errors. (Maybe they claim that Muen is the first open source run-time-error-free microkernel in the sense that they did the verification after seL4, but before seL4 was open-sourced?) [1] http://ssrg.nicta.com.au/publications/nictaabstracts/3783.pdf http://ssrg.nicta.com.au/publications/nictaabstracts/3783.pd...
- hga 11y ago
  I would guess so, seL4 was open sourced in August 2014 and the first public preview of Muen was December 2013, per a quick check with Google. On the other hand, I've read that if you want to do serious SPARK/Ada work, you've got to buy AdaCore's tools or benefit from their academic program. seL4's verification down to binary was done using generic GCC (a clever way was found to meet the higher level proofs with stuff generated from the binary; they first tried CompCert (a verified C compiler that is free for non-commercial use) but I gather that suffered from an impedance mismatch).
  - nickpsecurity 11y ago
    Misleading. AdaCore provides Ada and SPARK IDE's in full under GPL if you release your software under GPL: http://libre.adacore.com/comparisonchart/ http://libre.adacore.com/comparisonchart/ Lots of free guides, tips, libraries, etc. You get way better tools in terms of testing, inspection, analysis, etc if you buy them. No doubt. The base platform, good enough for Muen or IRONSIDES DNS, is free. You can replicate their work easily plus create safer variants of established software such as Nginx, etc. Whereas seL4 relies on Haskell, Isabelle, several proof frameworks/tools, C, and GCC. They achieved a lot more but with a lot more tools, time, and expertise. Those of us that were interested couldn't even check the verification stuff, especially the C-related tech, until late 2014. Using them would be... non-trivial to say the least. :) Good that they open-sourced as that will allow (is allowing) others to build on the work. I know it's already getting integrated into Genode OS.
    - hga 11y ago
      As I was told in a HN discussion that non-educational "for GPL" version doesn't supply the same runtime, and the run time supplied is not very good. Maybe it's OK, but with all those restrictions and limitations it just didn't sound like an ecosystem I want to mess with. Plus I prefer to be able to develop and release software with less restrictive open source licenses. WRT seL4 vs. Muen, I wouldn't be surprised if seL4 does less for you, it's only 9,000 lines of C code, and some of it is artifacts from the manual Haskell -> C translation.

eternalban 11y ago

Exactly. It is exactly equivalent to saying that if a strict FP program compiles it is "bug free" but of course it has little to say about whether the code is 'correct'.

vilhelm_s 11y ago

But in the other direction, it seems that end-to-end implementation correctness implies absence of run-time errors. The seL4 authors write[1]: > IMPLICATIONS [...] a functional correctness proof already has interesting implications for security. If the assumptions listed in Sect. 5.5 are true, then in seL4 there will be: No code injection attacks [...] No buffer overflows [...] No NULL pointer access [...] No ill-typed pointer access [...] No memory leaks [...] No non-termination [...] No arithmetic or other exceptions [...] No un-checked user arguments [...] Aligned objects [...] Wellformed data structures [...] And this was already done in 2009. So I don't think Muen is the first microkernel to prove absence of run-time errors. (Maybe they claim that Muen is the first open source run-time-error-free microkernel in the sense that they did the verification after seL4, but before seL4 was open-sourced?) [1] http://ssrg.nicta.com.au/publications/nictaabstracts/3783.pdf http://ssrg.nicta.com.au/publications/nictaabstracts/3783.pd...

hga 11y ago
I would guess so, seL4 was open sourced in August 2014 and the first public preview of Muen was December 2013, per a quick check with Google. On the other hand, I've read that if you want to do serious SPARK/Ada work, you've got to buy AdaCore's tools or benefit from their academic program. seL4's verification down to binary was done using generic GCC (a clever way was found to meet the higher level proofs with stuff generated from the binary; they first tried CompCert (a verified C compiler that is free for non-commercial use) but I gather that suffered from an impedance mismatch).
- nickpsecurity 11y ago
  Misleading. AdaCore provides Ada and SPARK IDE's in full under GPL if you release your software under GPL: http://libre.adacore.com/comparisonchart/ http://libre.adacore.com/comparisonchart/ Lots of free guides, tips, libraries, etc. You get way better tools in terms of testing, inspection, analysis, etc if you buy them. No doubt. The base platform, good enough for Muen or IRONSIDES DNS, is free. You can replicate their work easily plus create safer variants of established software such as Nginx, etc. Whereas seL4 relies on Haskell, Isabelle, several proof frameworks/tools, C, and GCC. They achieved a lot more but with a lot more tools, time, and expertise. Those of us that were interested couldn't even check the verification stuff, especially the C-related tech, until late 2014. Using them would be... non-trivial to say the least. :) Good that they open-sourced as that will allow (is allowing) others to build on the work. I know it's already getting integrated into Genode OS.
  - hga 11y ago
    As I was told in a HN discussion that non-educational "for GPL" version doesn't supply the same runtime, and the run time supplied is not very good. Maybe it's OK, but with all those restrictions and limitations it just didn't sound like an ecosystem I want to mess with. Plus I prefer to be able to develop and release software with less restrictive open source licenses. WRT seL4 vs. Muen, I wouldn't be surprised if seL4 does less for you, it's only 9,000 lines of C code, and some of it is artifacts from the manual Haskell -> C translation.