A recently developed high-performance OS microkernel supports the capability security model and comes with a formal specification and machine-checked proof: it’s called seL4.

• Uncategorized