3 ms·
It is interesting to look at the SKPP and what a conforming implementation ensures against seL4, which has been formally verified to be correct. SKPP requires
by jnwatson 3y ago
It is interesting to look at the SKPP and what a conforming implementation ensures against seL4, which has been formally verified to be correct.
SKPP requires non-interference but not actual correctness, whereas with seL4 it actually is shown that a kernel call meet some formal requirement.