2 ms·
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 t
by j16sdiz 8y ago
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)
- sanxiyn 8y agoAfter 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.