Yes, I've seen some of the work that's been done on trying to create a OS that can be mathematically proven to be secure, but I just don't buy it. Sure you can use some set theory and various other things to try to show how mathematically the system is bounded within the secure states, but all of that goes out the window once you move beyond a non-trivial set of functionality
Buy it or not, formal verification is becoming an increasingly important aspect of all software, especially OS design and construction. The seL4 project at NICTA is a prime example. It is complete and non-trivial operating system kernel that provides unbreakable guarantees of process isolation and containment as verified formally. L4, a close relative of seL4 is already deployed on hundreds of thousands of mobile phones using the Qualcomm chipset. see http://en.wikipedia.org/wiki/L4_microkernel_family for more details.
Slashdot Mirror
Yes, I've seen some of the work that's been done on trying to create a OS that can be mathematically proven to be secure, but I just don't buy it. Sure you can use some set theory and various other things to try to show how mathematically the system is bounded within the secure states, but all of that goes out the window once you move beyond a non-trivial set of functionality
Buy it or not, formal verification is becoming an increasingly important aspect of all software, especially OS design and construction. The seL4 project at NICTA is a prime example. It is complete and non-trivial operating system kernel that provides unbreakable guarantees of process isolation and containment as verified formally. L4, a close relative of seL4 is already deployed on hundreds of thousands of mobile phones using the Qualcomm chipset. see http://en.wikipedia.org/wiki/L4_microkernel_family for more details.