Try the first two to be certified to high-assurance security: http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf http://www.cse.psu.edu/~trj1/cse443-s12/docs

Try the first two to be certified to high-assurance security: http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf The MLS model was too difficult to adapt to commercial use. Biba was good for stopping malware from overwriting files. They still preferred something more flexible. SCC then invented type enforcement in another high-assurance system: https://web.archive.org/web/20160311233659/http://www.cyberdefenseagency.com/publications/LOCK-An_Historical_Perspective.pdf https://web.archive.org/web/20160311233659/http://www.cyberd... Flask architecture was combining that tech with a microkernel. SCC, acquired by McAfee, added type enforcement to a BSD OS for their Sidewinder firewall. The next work by Mitre was proof-of-concept for OSS by adding it to Linux. That and a pile of incremental additions is called SELinux. I'm sure you'll find the LOCK design a lot cleaner as it was originally intended. ;) Also worth noting are the KeyKOS system (esp with KeySAFE), the capability-security machines, and one language-based mechanism: http://www.cis.upenn.edu/~KeyKOS/ http://www.cis.upenn.edu/~KeyKOS/ http://www.cs.washington.edu/homes/levy/capabook/index.html http://www.cs.washington.edu/homes/levy/capabook/index.html http://www4.cs.fau.de/Projects/JX/ http://www4.cs.fau.de/Projects/JX/ These collectively should keep you busy for a while. They're the kind of thing worth imitating or building on.