| As the core of computer software, operating system security is vital for all computer software. But the extremely large size and the extremely complex structure of the operating system make the operating system’s security extremely uncertainty.Formal method is a currently accepted method which can ensure security and reliability of system software.It is based on strict mathematical logic system,and transform the operating system into the system whom is described by the mathematical logic language(we call this system as formal system), and then through the verification of the safety properties of the formal system to ensure the safety of the operating system.OCAP (Open Certified Assembly Programming) is a remarkable model about formal methods,it not only manages to make the verifications of different modules in the operating system combined, but also ensures the good extensibility of the model.Refer to OCAP, this paper establishes a verification model to verify the micro kernel operating system,and then verifys the message module of the operating system VTOS which is come true by our project team members.This paper makes the following study and contributions:1. Come true the OCAP framework to verify the operating system VTOS by the prover Isabelle,and extend the types base on OCAP, which will make explaining the consistency between the implement and the logic easier.2. Refer to Hoare Logic, design precondition for each instruction, divide the precondition into two part:One is the precondition about the function which the instruction in;the other is the precondition about the instruction itself.3. Through this model verify the message module of the operating system VTOS which is come true by Our project team,this part has two main aspects:first, prove that execute each instruction when its corresponding state meet the preconditions of the instruction(this paper call this property well-structured);Second, the functions of the message module are correct. |
PDF Full Text Request