[mantraxC]

Hmm, given how compilers & hardware can introduce incorrectness and security vulnerabilities in otherwise valid code, it makes you wonder if anyone can really claim "end-to-end proof of correctness" unless they include the specific compiler & hardware in their proof.

[TacticalCoder]

Concerning the compiler, in the link it is written:

"There is a further proof that the binary code that executes on the hardware is a correct translation of the C code. This means that the compiler does not have to be trusted, and extends the functional correctness property to the binary."

(I wonder how that works but it is related to your compiler concern)

Now even though the issue of hardware (say rogue hardware with rigged number generators and whatever backdoors) is probably a real concern, I still think that seL4 and its codebase where hundreds of bugs have been automatically found (and manually squashed) is a big step forward.

[Avshalom]

On that note: what even is a correct translation of C when it has so many undefined behaviors in it's spec.

[cc_]

They use a formally-specified subset of C described in Harvey Tuch's PhD thesis: http://www.ssrg.nicta.com.au/publications/papers/Tuch:phd.pd...

[wmf]

What if the code doesn't rely on undefined behavior?

[regehr]

Absence of undefined behavior in the C implementation is of course one of the things covered by the seL4 proof.