Obligatory mention of early attempt to really understand and address subversion as a threat plus a follow-up by pioneers that built on that: http://seclab.cs.u

Obligatory mention of early attempt to really understand and address subversion as a threat plus a follow-up by pioneers that built on that: http://seclab.cs.ucdavis.edu/projects/history/papers/myer80.pdf http://seclab.cs.ucdavis.edu/projects/history/papers/myer80.... https://apps.dtic.mil/dtic/tr/fulltext/u2/a435312.pdf https://apps.dtic.mil/dtic/tr/fulltext/u2/a435312.pdf The current state-of-the-art in both formal methods, automated analyses, and test generators can get us pretty close to their goals with such designs, too. Way less cost-prohibitive than it used to be. Although, high-assurance security today has moved far away from security kernels they advocated to focus on securing hardware/software and distributed systems in ways that allow expressing more flexible and useful policies. The design and assurance methods of the past still work, though. Stuff like Rust, SPARK Ada, RV-Match, Why3, and CompCert handle more code-level problems than older methods, too.