Introduction

One of the vital aspects of a computer system is to store and protect highly sensitive data. At the same time, attacker resources and determination are also amplifying significantly. According to recent studies about very sophisticated and targeted attacks as well as sizeable nationwide surveillance programs, the effectiveness of currently deployed security systems is in question. Hence, systems capable of providing securities to critical application and information must assure the quality to function correctly. A solution to security threat would be to compartmentalize data and its application. An example can be the usage of a dedicated computer for each task and is only connected to the Internet when needed. However, this solution does not fit well. Also expecting high assurance for the security of today's monolithic Operating Systems (OS) is extremely hard because of their large size and complex functionalities. The OS vendors regularly highlight this fact in their security updates. Thus, they are a weak foundation for building secure systems\cite{kernel2015}.
However, on the other side, microkernels are a useful resource for the system which has strict demands on robustness and security. These are small in size compared to monolithic kernels, which is also a precondition for formal verification. Microkernel keeps user services and kernel services in separate address space, whereas in monolithic kernel user services and kernel services both are held in the same address space as shown in Fig \ref{337922}.