Research On Key Issues In High Assurance System Software Of Embedded Systems

To meet the increased requirements of advanced industrial manufacturing and intelligent equipment control,embedded systems have become the main pillar underlying almost all the critical infrastructures in our daily life and determine the safety and security of the whole system in various fields,such as,industrial manufacturing,seafaring,transportation,national defense,and information communication.In recent years,with the pervasive use of the embedded devices,as well as the developmental trends of network connection and intelligent application,the embedded systems become more vulnerable.Ensuring the reliability of system operation and the security of sensitive data,is regarded as a major issue in the fields of embedded system research.Software failures and security breaches in the embedded systems will potentially cause serious accidents that may endanger the safety of national politics,economy and defenses.Therefore,the design and development of a functionally correct embedded system which can satisfy the property of security and safety,and capable of providing convincing evident of the claimed correctness,becomes an important research subject.In order to solve the above issues,this dissertation comprehensively analyzes and summarizes the security requirements of the high assurance embedded applications to the system software and presents a software architecture which can satisfy secure isolation and formal verification.Furthermore,to address those key issues of system software,including modeling hardware mechanism,verification of interruptible code,access control of untrusted components and hardware-virtualization based isolation and protection,proposes corresponding solutions.Finally,a scalable,compositional framework and related toolchain of developing and certifying high assurance system software of embedded systems are presented.With the proposed framework,a prototype system has been developed and evaluated.In conclusion,the approach of integrating component isolation,hardware protection mechanism and formal methods is able to support the development of high assurance system software that meets the security and reliability requirements of embedded applications,in both function and performance wise.It lays a solid foundation for the further development of high assurance embedded systems.The dissertation's main innovations and contributions can be summarized as follows:(1)In respect of security/safety-critical device drivers in the embedded systems,a compositional and scalable hardware abstraction and driver code verification framework have been proposed.This systematically ensures the isolation of driver modules while the end-to-end functional correctness property of them is proved.(2)To support the interruptible code verification of the kernel modules,this dissertation proposes an approach to formally model the interrupts.In this approach,two models of the interrupts are firstly built: a realistic “hardware interrupt model” which mimic the exact hardware behavior and an “abstract interrupt model” used to verify the interruptible code.Furthermore,through multiple layers of contextual refinement,the correctness of the interruptible code proved by the abstract interrupt model can be propagated to the hardware interrupt model.In this way,the nondeterministic semantics caused by the concurrent execution of kernel code and interrupt handlers is solved.(3)Based on the framework of driver verification and the approach of interrupt abstraction,several driver components in the high assurance operating system,including the interrupt controller,are formally verified.During this process,multiple bugs are found in the unverified system.To the best of our knowledge,it is the first verified interruptible OS kernel and device drivers that come with machine-checkable proofs.(4)Considering device drivers that are not security/safety-critical,but still in the high assurance embedded systems,this dissertation proposes a high-performance runtime framework based on a command interpreter and security policy checking mechanism to support their execution.Command channels based on shared memory pages are first built to enable the communication between the kernel and user-level device drivers.All the device operations are then translated into requests and sent to the command interpreter.In this way,the behavior of driver code can be monitored and checked against the security policy,and the accesses to the hardware resources can be controlled.This framework provides fault isolation and security protection of the untrusted system software components.(5)For the virtual machine monitor(VMM)in the high assurance embedded systems,this dissertation combines the formal verification approach based on the certified abstraction layers,and the secure run-time framework to propose a systematic design and verification framework.The proposed approach exploits the benefits of hardware-assisted virtualization,secure isolation and formal verification.Components directly related to the virtual machine isolation and access control,is formally verified by the layered contextual refinement proof to ensure their functional correctness.On the other hand,components which are not related to the secure execution of virtual machines,are hosted by user processes.The protection mechanisms from the kernel will guarantee the noninterference property between the guest systems.(6)The formal model,specification,implementation and proof are all done in a unified interactive theorem prover: Coq,yet the machine-checkable proofs verify the correctness of the code.Finally,the extracted code from the verification framework is used constructed a prototype system on top of actual hardware.The proposed approaches are highly practical.At present,there are still many open problems behind the research of high assurance embedded systems.The techniques and approaches proposed by this dissertation will provide new perspectives to the researchers in this filed.In addition,it also provides theoretic and technical supports to the research of high assurance embedded systems with independent intellectual property of China.