WingNews logo WingNews
top | item 10146662

(no title)

Zuph | 10 years ago

"The Muen Separation Kernel is the world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level."

This doesn't really jibe with seL4's claim: "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is now open source." http://sel4.com/

discuss

order

c_moscardi|10 years ago

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

vilhelm_s|10 years 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.pd...

eternalban|10 years 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'.