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 08:43 AM
About Abi Nourai:
Abi Nourai, Engineering Director at OK Labs, looks after a team of engineers focused on product development and delivering professional services to OK customers. Abi is excited about using the L4 technology he helped develop as an undergraduate to solve 'real world' problems. He gets away from it all by attempting to get speeding tickets on the Old Pacific Highway through the bushland to the central coast in Australia. When not speeding, Abi is an avid skier, and he has skied all over the world.
Share this article