3 ms·
It's worth noting that seL4 is a variant of L4, a very small microkernel. Proving the microkernel secure is interesting, and maybe useful; but a real OS has a
by metageek 16y ago
It's worth noting that seL4 is a variant of L4, a very small microkernel. Proving the microkernel secure is interesting, and maybe useful; but a real OS has a lot of other pieces, which may introduce their own insecurities.