I'm not so good at names. Let's see if Google can help me... People have been talking about this stuff for decades. I found a paper from 1975 right in the top

I'm not so good at names. Let's see if Google can help me... People have been talking about this stuff for decades. I found a paper from 1975 right in the top of my search results: http://csrc.nist.gov/publications/history/neum75.pdf http://csrc.nist.gov/publications/history/neum75.pdf. That eventually became PSOS. There was also KSOS which had formal proofs both of the design and that the code conformed to the design. There is a whole batch of TE based kernels that are descendants from Secure Ada Target/FLASK: SCOMP, LOCK, DTOS, Trusted MACH, TrustedBSD, and of course Sidewinder made a big deal about their firewalls using a provably secure kernel which was based on that work. The NSA even opensourced the Tokeneer project: http://www.adacore.com/sparkpro/tokeneer http://www.adacore.com/sparkpro/tokeneer Then there is MITRE, UCLA's DSU, AIM, etc. I could swear there was at least once SELinux vendor that claimed it was providing the "only" provably secure kernel. There was also HYDRA... Anyway, there are lots.