4 ms·
The paper is talking about rigorous formal mathematical proofs of correctness like in the sense of of the seL4 kernel (https://sel4.systems/Info/FAQ/ https://se
by seanwilson 11y ago
The paper is talking about rigorous formal mathematical proofs of correctness like in the sense of of the seL4 kernel (https://sel4.systems/Info/FAQ/ https://sel4.systems/Info/FAQ/) where they have confirmed the kernel is completely free of bugs such as buffer overflows, null pointer exceptions, use-after-free, etc.
- ktRolster 11y agoOf course, there might be bugs in the specification (the proof the made was that the kernel matches the specification)
- seanwilson 11y ago> Of course, there might be bugs in the specification (the proof the made was that the kernel matches the specification) Nothing is perfect, but this approach catches more bugs than any other technique. Also, some specifications are simple to specify e.g. it's not hard to specify that an array index must be within the bounds of the array and if you did get this wrong you'd notice quickly as you'd be unable to prove obvious facts are correct.
- ktRolster 11y agobut this approach catches more bugs than any other technique Have you seen the specification for sel4? It's fairly complex.