Formal Research On The Security Of The Microkernel Operating System

Since operating system is a software that directly operate the hardware,the industry and academia pay close attention to the research on the security of operating system.Especially in some secure crucial area such as aerospace,medical and unmanned aerial vehicles,the security of operating system must be guaranteed.At present,the acknowledged most effective method to prove the correctness of the operating system is formal verification.The researchers always pay attention to the research of properties such as functional correctness and integrity of operating system,few of them aim at the security by means of analyzing,modeling and verifying.This paper summarize the existing research methods to extract the security requirements of an operating system,and according to these requirements,an microkernel operating system is designed and implemented,which is called four threads operating system(FTOS).Then model and verify the security of FTOS by formal methods.In this paper,the main research contents include the following three parts:(1)Design and implement the microkernel operating system from the perspective of simplifying formal verification.To make verification of the kernel feasible,its design should minimise the complexity of data structures and algorithms,so verification related problems should be taken into account during developing FTOS.Design The formal semantics about the processes and the interrupts,and propose that concurrency and nondeterminism make it harder to verify FTOS,the solution is adopt Concurrent separation logic(CSL).(2)Extract the abstract function specification from FTOS,then establish a double-layer refinement model to describe the behavior of the system.The high-level abstract specification describes what the system does without saying how it is done,the underlying concrete specification fills in the details left open at the abstract level and to specify how the kernel works,involving abstraction of C and assembly semantics.Build the refinement relationship between the high-level and the underlying specification.The refinement relationship considers the nondeterminism caused by concurrency and then introduces the concept of invariant to ensure the consistency between the system states of the two levels of specification.Finally,take process scheduling as well as interrupt handling as examples,illustrates that the underlying specifications refines the high-level specification.(3)Extracte initialization,process scheduling and interrupt handling models from the microkernel operating system,then use these models to make up the domain of discourse of the operating system formal verification.Establish a concurrent logical separation relevant assertion,including its syntax and semantics,and then summarize the main inference rules.Design the pre-conditions and post-conditions of behaviors of system initialization,process scheduling and interrupt handling,and propose the invariance these behaviors should hold according to the pre-and-post conditions.Define and proof the lemmas of behaviors above in the theorem prover Coq,and integrate the proofs of these function modules to form a complete system correctness proof,achieve the verification of consistency between the design of the system and the security requirements.