It was proven impossible to fully secure by high-assurance engineers back when INFOSEC was being invented. UNIX was much smaller back then. Project such as UCLA Secure UNIX and products such as Trusted Xenix were still unable to reach high assurance due to problems baked into the architecture and UNIX principles themselves. Even with API changes, they still had problems with covert channels. That led the inventors of INFOSEC to abandon UNIX for secure applications in favor of clean-slate, security kernels with user-mode or deprivileged layers for legacy, UNIX apps. Anything truly trustworthy runs directly on the security kernel.
re secure OS's
Probably INTEGRITY-178B or Turaya with Linux VM's for now. Maybe SourceT for network appliances. They're sold for nice sums of money to militaries, governments, and companies with nice budgets. GenodeOS is working toward a FOSS version of Nizza architecture.
Two of the original, high-assurance systems are still around for OEM license from BAE (STOP) and Aesec (GEMSOS). We've learned a lot of ways to break stuff since then. Who knows what current level of assurance is. ;)
Finally, there's CPU's designed to do isolation, reliability, and so on at the gate level. Rockwell-Collins uses one in their guards and crypto appliances. Sandia has a high-assurance Java CPU. Industry also sells Java CPU's for embedded that might be converted into some safe execution platform combined with something like JX. Call these building blocks for secure OS rather than the OS itself.
It was proven impossible to fully secure by high-assurance engineers back when INFOSEC was being invented. UNIX was much smaller back then. Project such as UCLA Secure UNIX and products such as Trusted Xenix were still unable to reach high assurance due to problems baked into the architecture and UNIX principles themselves. Even with API changes, they still had problems with covert channels. That led the inventors of INFOSEC to abandon UNIX for secure applications in favor of clean-slate, security kernels with user-mode or deprivileged layers for legacy, UNIX apps. Anything truly trustworthy runs directly on the security kernel.
re secure OS's
Probably INTEGRITY-178B or Turaya with Linux VM's for now. Maybe SourceT for network appliances. They're sold for nice sums of money to militaries, governments, and companies with nice budgets. GenodeOS is working toward a FOSS version of Nizza architecture.
http://www.ghs.com/products/safety_critical/integrity-do-178...
https://os.inf.tu-dresden.de/papers_ps/nizza.pdf
http://www.perseus-os.org/content/pages/Architecture.htm
https://secure64.com/secure-operating-system/
Two of the original, high-assurance systems are still around for OEM license from BAE (STOP) and Aesec (GEMSOS). We've learned a lot of ways to break stuff since then. Who knows what current level of assurance is. ;)
http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf
There's also language-based approaches being investigated that could be done in something more trustworthy than Java:
http://www4.cs.fau.de/Projects/JX/
Finally, there's CPU's designed to do isolation, reliability, and so on at the gate level. Rockwell-Collins uses one in their guards and crypto appliances. Sandia has a high-assurance Java CPU. Industry also sells Java CPU's for embedded that might be converted into some safe execution platform combined with something like JX. Call these building blocks for secure OS rather than the OS itself.
http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf
https://www.ajile.com/index.php?option=com_content&view=arti...