3 ms·
seL4 actually has an end-to-end proof, which proves that the final compiled binary matches up with the formal specification. There are not many places that bugs
by lifthrasiir 3y ago
seL4 actually has an end-to-end proof, which proves that the final compiled binary matches up with the formal specification. There are not many places that bugs can be shifted---probably the largest one at this point is the CPU itself.
- hnfong 3y agoThe bugs are shifted into the spec, or the proof.
- snvzz 3y agoNot really shifted. If you think about it, a bug in the proof will require a bug in the code. This visibility is a good thing. Overall, note that the critical code, such as the microkernel itself, is small (kLoC wise) to begin with, which minimizes the odds a bug will go undetected for long.