Formal Specification and Verification of Data Separation for Muen Separation Kernel - Bhushan, Ram C.; Yadav, Dharmendra K. (Recent Advances in Computer Science and Communications, 2022)
Introduction: Integrated mixed-criticality systems are becoming increasingly popular for application-specific systems that need a separation mechanism for available onboard resources and the processors equipped with hardware virtualization, which allows the partitions to physical resources, including processor cores, memory, and I/O devices, among guest Virtual Machines (VMs). For building mixed-criticality computing environment, traditional virtual machine systems are inappropriate because they use hypervisors to schedule separate VMs from physical processor cores. This article discusses the design of an environment for mixed-criticality systems: The Muen, an x86/64 separation kernel for high assurance. The Muen Separation Kernel is an open source microkernel with no run-time errors at the source code level. The Muen separation kernel has been designed precisely to encounter the challenging requirements of high-assurance systems built on the Intel x86/64 platform. Muen is under active development, and none of the kernel properties of it has been verified yet. In this paper, we present a novel work of demonstrating one of the kernel properties formally. Methods: The CTL used in NuSMV is a first-order modal along with data-depended processes and regular formulas. CTL is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any of which might be an actual path that is realized. This section shows the verification of all the requirements mentioned in section 3. In the NuSMV tool, the command used for confirmation of the formulas written in CTL is checkctlspec -p ”CTL-expression”. The nearest quantifier binds each occurrence of a variable in the scope of the bound variable, which has the same name and the same number of arguments. Results: Formal methods have been applied to various projects for specification and verification of safety properties. Some of them are the SCOMP , SeaView , LOCK, and Multinet Gateway projects. The TLS was written formally. Several mappings were done between the TLS and the SCOMP code: Informal English language to TLS, TLS to actual code, and TLS to pseudo-code. The authors present an ACL2 model for a generic separation kernel, also known as GWV approach. Conclusion: We consider the formal verification of data separation property, which is one of the crucial modules to achieve separation functionality. The verification of the data separation manager is carried out on the design level using the NuSMV tool. Furthermore, we present the complete model of the data separation unit along with its code written in the NuSMV modelling language. Finally, we have converted the non-functional requirements into the formal logic, which then has verified the model formally.
Keywords: muen