Research On Formal Modeling And Verification Method For Separation Kernel

With the rapid development of computer technology,software architecture has become more and more complex,and software security has become a hot topic in industry research.Realizing independent management and control of multi-level subsystems through partition isolation is an effective means of security assurance.The partitioned operating system built with this idea can provide an independent and safe operating environment for application layer software.As the cornerstone of the partitioned operating system,the separation kernel realizes the management and control of information flow between partitions by providing a temporal and spatial isolation mechanism.Therefore,the security of the separation kernel itself and the effectiveness of the mechanisms provided are critical and subject to rigorous certification and evaluation.Formal verification technology is widely used in the field of operating system security verification because of its accuracy of description,unambiguity,and rigor based on mathematical logic proofs.However,the existing formal verification methods for separation kernel isolation still have problems such as poor scalability and low efficiency,and it is difficult to support automated overall verification from the attribute side to the source code side of the model,and it is difficult to balance spatial isolation and temporal isolation of the verified attributes.Aiming at the problems existing in the current separation kernel verification method,this thesis proposes a separation kernel semantics model(SKSM).This model fully considers the temporal isolation and spatial isolation mechanism provided by the separation kernel,selects three key basic modules of memory management,thread scheduling and thread communication as the modeling target,and adopts a hierarchical structure to divide the behavior of each module into abstract framework layer,behavioral logic layer and the underlying function layer can formally define the kernel behavior layer by layer from top to bottom,and provide the spatio-temporal isolation requirements that the kernel should meet layer by layer.Aiming at the formal verification requirements of the semantic model,this thesis further proposes a set of separate kernel formal modeling schemes: functional correctness modeling of the underlying function layer based on Hoare logic,abstract behavior modeling of the abstract framework and behavioral logic layers using the BIP modeling language,modeling of spatio-temporal isolation requirements based on linear timing logic,and solving the overall path state explosion of the system based on the combined modeling technique.The bottom-up formal modeling of the three SKSM layers is achieved.Finally,in order to meet the verification requirements of the formal modeling scheme,this thesis extends the verification function of the source code layer to the existing abstract behavior modeling verification tool,and realizes the automatic verification of the separation kernel model from the attribute side to the source code side on an integrated verification platform,effectively improving the verification efficiency.In order to facilitate the elaboration of the formal modeling and verification method of the kernel,this thesis takes the sel4 separation kernel as the research object,and conducts modeling and verification of its memory management,thread scheduling and thread communication modules.The validation results demonstrate the effectiveness of the proposed separate kernel semantic model,the formal modeling scheme,and the integrated verification platform.