| Being a most critical part of the computer system,operating systems are the key to the reliability of computers.Any vulnerabilities and errors of operating systems are likely to result in catastrophic consequences.Formal program verification uses mathe-matical proofs to establish the correctness of programs,thus provides a stronger guar-antee of reliability than other techniques,and has been applied to the verification of operating systems.Operating system's global properties are the properties that must always hold dur-ing system execution.They are called global properties in the sense that they are not concerned about the behavior of a particular API but instead apply to the whole system,and must be preserved by each execution step.Formally verifying global properties ensures that the runtime behaviors of the entire system follow the intent of the kernel programmer.Beijing Institute of Control Engineering developed an embedded real-time oper-ating system that has been deployed on the spacecraft for Chinese Lunar Exploration programs.Earlier verifications on this operating system either focus on a specific ap-plication scenario or are limited to a single kernel module,and no effort has been made to verify system-wide properties.The Certi-μC/OS project developed an operating system verification framework that support third party operating systems.However,the framework has but a rudimen-tary support for reasoning about system-wide properties,demanding high verification effort.We first extend the original framework to resolve this issue,and then based on the extended framework,we formulate and verify several global properties for the aforementioned operating system.Specifically,this thesis makes the following contri-butions:1.We extend the Certi-μC/OS framework with a set of inference rules that provide better support for global property verification.2.Based on the extended framework,we first build an abstract model for the target kernel and give abstract specifications for eight kernel functions from key kernel modules.Then we formally specify eight global properties related to task and semaphore management of the target kernel,and using our inference rules verify that the abstract kernel satisfies these properties.3.All our work are mechanized in the Coq proof assistant and all the proof scripts are machine checkable.We also develop several Coq tactics that minimize proof cost. |
