Accelerating Time-to-Market
separation kernel ( sel4 . systems ). It is a mathematically provably correct microkernel that will provide both time and space separation between running processes . It guarantees that there will be no unintended data leakage between processes , and that one process cannot impact the operation of another . This provides greater system resilience and security ( these are also attributes of a multiple independent levels of security ( MILS ) solution 3 ). On top of this , we use a middleware framework based upon the Object Management Group Data Distribution Service standard ( OMG DDS ). The subsections below describe the motivations for each .
To understand the need for a secure microkernel , like seL4 , it is helpful to start with a closer look at kernel design principles in general . As shown in Figure 3-2 , there are two main kernel design approaches – the monolithic kernel and the microkernel . In the former one , all code required for providing typical OS services is directly implemented in the kernel itself . The kernel executes in the privileged mode of the hardware , meaning that all code is granted unrestricted access and control of all system resources . This type of implementation might be beneficial to the overall system performance , but it can lead to dangerous situations if any of the kernel components feature some type of malfunction – a state that could be exploited by an attacker . A prominent example is provided by the Linux kernel , which – containing more than 20 million lines of code – can be expected to contain a certain number of bugs providing potential attack channels .
In contrast , the microkernel design copes with this drawback by drastically reducing the trusted computing base ( TCB ), meaning the subset of code in the overall system that must be trusted to operate correctly . A microkernel follows the design principle of having the kernel contain only the most fundamental mechanisms ( e . g . IPC , scheduling ). All remaining OS functionality must be transferred to the unprivileged user mode , thereby running encapsulated within isolated sandboxes . This approach protects the kernel processes from any interference from the outside , only allowing communication that is explicitly wanted . For a well-designed microkernel like seL4 this means that code base can be reduced to the order of ten thousand lines of code . This drastically shrinks the attack surface . The general performance problem of typical microkernels , induced by the significant communication overhead due to the additional kernel entries / exits and context switches , was solved back in the mid- ‘ 90s by Jochen Liedtke 4 . He accelerated the underlying IPC concept and designed the first L4 microkernel .
Journal of Innovation 89