News for hackers. Stuff that matters.

A comment on L4Linux – Linux running on the L4 microkernel. Parent comment

Re:L4Linux – Linux running on the L4 microkernel by j16sdiz on Saturday January 19, 2019 @12:18AM (#18945480)
seL4 is bug free in theory, not in paratice. It have been proved to follow the spec, but the spec can have error. Missing workaround for hardware bug can bite too.

"Beware of bugs in the above code; I have only proved it correct, not tried it." -- Donald Knuth on the van Emde Boas construction of priority deques (1977)

[ Parent | on HN ]
Re:L4Linux – Linux running on the L4 microkernel by sanxiyn on Saturday January 19, 2019 @03:51AM (#18946054)
After proving the full functional correctness (that machine code implements spec), they did additional security proofs against the spec, including confidentiality and integrity. If you accept their TCB(no hardware bugs etc), the entire proof is incredibly strong.
[ Parent | on HN ]