Open Kernel Labs Blog

May 06, 2008

TCB Size Does Matter

If you read about computer security in the literature, you'll come a lot of discussion about various kinds of access-control policies.  One particular policy that is becoming more and more mainstream, thanks largely to seLinux, is mandatory access control (or MAC for short).  For all the talk that takes place about using the 'right' access-control policy to build more secure systems, it's often understated  that unless your operating-system kernel actually correctly enforces the authorization rules you establish, all bets are off.

Another way of saying this is that correct kernel functionality is a pre-requisite for building a secure system.  This is a pretty obvious and easy statement to make. The tricky bit is actually coming up with a kernel you can have faith in, in the first place.

At OK Labs we employ two unique approaches to building truly trustworthy systems. The first is defensive. We start by acknowledging that software is inherently buggy.  Yep, perfect code is a rare find - even the best programmers introduce a defect every now and then. One of the best ways to build a correct and secure system is to minimize the amount of code you depend on for correct functionality. At OK Labs we call this minimizing your Trusted Computing Base (TCB) and it's one of the unique things the microkernel approach offers.

The second approach is more offensive but happens to be related to the minimal TCB doctrine. In striving for a small TCB, you want to minimize what runs in privileged mode, because thats the part of the system where any defects can lead to circumvention of security policies. The added bonus is that small kernels become an automatic candidate for formal verification. This is a technique by which a kernel's implementation is modeled by mathematics and logic representations, and then powerful theorem proving techniques are employed to prove correctness (and in particular the absence of defects).

The bottom line is that OKL4 serves as a powerful basis for constructing truly trustworthy systems. Reconnecting with the topic of mandatory access control introduced earlier, and the recent press on Secure HyperCell Technology, with OKL4 you can apply MAC across virtual machines and cells in general, and also trust that your operating-system kernel will actually enforce the security mechanisms you come to depend on.

Posted by Abi Nourai on May 06 at 10:43 AM

blog comments powered by Disqus
Abi Nourai's avatar

About Abi Nourai:

Abi Nourai - Sales Director has recently relocated from Sydney to OK's Paris office, and even more recently, made another move to London. The journey was a little easier this time round. Abi is excited about using the OKL4 technology he helped develop as an undergraduate to solve business problems for the mobile and embedded spaces. Abi gets away from it all by indulging in fine cuisine, roaming through museums, and hopping around Europe's many great cities.

Email Abi Nourai

Virtualization for Embedded SystemesPermalink

▲ Back to Top