26 ms·
Neat, I didn't know about seL4. Can you point me to how they define the proof for it?
by dogprez 7y ago
Neat, I didn't know about seL4. Can you point me to how they define the proof for it?
- monocasa 7y agoThey've done a really good job documenting it in their papers and online docs, but the general flow is to verify equivalence of the generated binary and the formal specification, then to prove properties like memory safety of the formal spec. I'd start here if you want to learn more: https://sel4.systems/Info/FAQ/proof.pml https://sel4.systems/Info/FAQ/proof.pml Let me know if you have any other questions.
- reirob 7y agoFOSDEM speach video [1] about the status of seL4, I really enjoyed. [1]: https://fosdem.org/2020/schedule/event/uk_sel4/ https://fosdem.org/2020/schedule/event/uk_sel4/