Wish I had this years ago. Security kernels & their successors, separation kernels, were only OS kernels to ever survive pentesting by NSA & other TLA’s. That’s for both code injection & covert/side channels. They became de facto standard in high-assurance security for isolating apps or VM’s on untrustworthy CPU’s until get we get secure ones. This paper is packed with info on many (maybe all) implementations from FOSS to industry. It covers the different types of kernels, many examples, what formal methods were used for verification, tables for attribute comparisons, limitations, and areas for more work. Splendid survey.