3 ms·
I'm setting up a system with SeL4. None of the systems you're suggesting have formal proofs of correctness, and this one not only has such proofs, but is writt
by microcolonel 12y ago
I'm setting up a system with SeL4.
None of the systems you're suggesting have formal proofs of correctness, and this one not only has such proofs, but is written in C.
- geofft 12y agoWhat is the process for patching seL4? How does e.g. adding a parameter to an existing function affect the proof, and what's the process for proving additional predicates?
- microcolonel 12y agoThe proofs are publicly available, though I can imagine there would be significant... overhead involved in adding functions to the system.