A Survey on Formal Verification of Separation Kernels

Introduction: In developing safety and security-critical systems, separation kernel acts as a primary foundation, which provides spatial as well as temporal separation. The separation kernel offers highly assured partitions to the applications hosted on the fundamentally critical systems and can also control the flow of information between them. The industries, as well as academia, have developed several separation kernels that have been broadly applied in critical systems like military/defense secured applications, avionics/aerospace intelligent systems, healthcare units that deal with human lives and in many more areas. The increasing popularity of separation kernels demands the formal verification that assures the correctness of the functionalities in it. Further, formal verification of separation kernels has become mandatory by the security/safety certification authorities. Conclusion: This paper first presents the concept of the separation kernel, and then it discusses the functionalities, design, and properties of it. The classification and analysis of the formal languages are being presented in this paper used for writing the specifications of the separation kernel and verifying it. The paper is an attempt towards the classification of formal languages being used for the verification of several separation kernels.