Research On Formal Verification Method Of Embedded Operating System

Embedded operating systems,as foundational software systems,are the core and cornerstone of embedded systems,which manage the software and hardware resources of the embedded system.In recent years,with the continuous integration of intelligent technology and the Internet of Things,embedded operating systems have been widely used,which is showing an intelligent and networked development trend.But at the same time,the security of embedded operating systems and the security of users' sensitive information have become the key and difficult issues to be solved in the embedded field.Once a software error or leakage of confidential information occurs in an embedded operating system,it may cause a major security accident or great economic loss.Therefore,for the application scenario of the embedded operating system,analyzing the actual feature requirements,establishing functionality and security models,and being able to prove that the system code implementation does conform to the functionality and security specifications has become a significant and important research topic.In order to solve the above issues,the dissertation analyzes and summarizes the design,implementation and verification requirements of embedded operating systems,and addresses key issues such as the functional verification of the memory management module,the functional verification of the task management module and the security verification of the trusted execution environment.Finally,a scalable modular verification framework and verification system are presented.Besides,a verified secure embedded operating system trusted execution environment was implemented and evaluated.The evaluation results show that the scalable modular verification framework combined with the hardware isolation protection mechanism can not only meet the special requirements of the embedded operating system in terms of functionality,performance and security,but also improve the feasibility of the entire system verification,thus a credible evidence that the system source code implementation meets system functionality and security requirements is provided.The main contributions and innovations of this dissertation can be summarized as follows:(1)In order to achieve the entire verification of the embedded operating system,a scalable modular validation framework for embedded operating systems is proposed.For each individual module,the implementation layer specification of the C program is described based on separation logic,and the functional programming method is used to build the abstraction layer specification of the C program,and then the data refinement relationship between the two is established and the consistency proof is performed.Finally,a verified module whose source code implementation is consistent with the specification behavior of the abstraction layer is established.For the entire system verification,the framework's compositional rules are used to link the abstraction layer specifications of each submodule into a complete verified system.(2)For the memory management module of the embedded operating system,a method for modeling and verifying high-performance C programs containing complex pointer data structures is proposed.A memory management algorithm with low memory fragmentation rate,diverse memory allocation granularity and predictable execution time is taken as a case study.Based on the modular verification framework,the underlying data structure operation interface and the behavior semantics of the high-level memory allocation and release operation behavior semantics were successfully defined,thereby completing the modeling verification work of the high-performance memory management module.(3)For the task management module of the embedded operating system,an ARM assembly semantic model is built,the modular verification framework was extended for supporting verification of assembly language and a combined verification system supporting C and ARM assembler was proposed.Based on the combined verification system,the task management module is divided into two sub-modules: one is task scheduling(C implementation)and the other is task context switching(ARM assembly implementation).First,each model is verified at different levels of abstraction,and then compositional verification was performed based on the abstraction layer specification of each sub-module,which solves the problem that the separation logic does not support assembly function pointers,and finally completes the formal verification of the task management module.(4)In order to meet the isolation requirements of the execution environment of the embedded operating system,a design methodology with narrow communication interface is proposed for TrustZone trusted execution environment,and the security property model(e.g.,information flow non-interference)of the trusted execution environment is built.Finally,an integrated verification system supporting end-to-end security attribute verification,C and assembly correctness verification,program abstraction and data refinement verification are presented.To the best of our knowledge,it is the first verified multi-tasks embedded operating system based on ARM TrustZone hardware protection mechanism.(5)The formal implementation,specification,model,property definition and proof of the entire system are all done in the auxiliary theorem prover Coq,which minimizes the semantic gap between different specification interfaces.In addition,the verified software system can be executed on a real hardware platform,and the entire theoretical scheme is highly practical.At present,there are still many challenges in the field of embedded operating systems formal verification.The dissertation aims to provide a new theoretical basis and technical methodology for the development and verification of secure and reliable embedded operating systems.