Provable Security: How Feasible Is It?
For mainstream operating systems the community has given up on strong security. One can graft mandatory access control onto Linux, or try to harden Windows NT, but people are in no position to get to provable or even just assurable security of such OSes in the next 20 years. There do exist a number of high-level security models that work with nice, provable properties. There are ways to build and structure secure systems. It is known that systems can be secured much better by reducing the Trusted Computing Base (TCB). Microkernels with access control and separation kernels provide solid foundations for implementing such models. Some such systems have been built, demonstrated, and are deployed. But even with their reduced TCBs nobody has yet proved security down to the implementation level.