A Separation Kernel is a small specialized microkernel that provides a sand-boxed execution environment for a given set of processes (also called \subjects"). The subjects may communicate only via declared memory channels, ...