Abstract: As the cornerstone of the information age, the importance of operating system security is self-evident. Conventional methods of software testing are not enough to guarantee the safety of the operating system, so we need to use more rigorous formal verification methods based on mathematical logic. This paper puts forward a new idea of formal verification of software: constructing a simulation running environment in Isabelle, and running the assembly code in it, recording the changes of the system state, and finally according to the changes of system state before and after run of the program, determining the correctness and safety of the program. It emphatically introduces the prove method of sequential, conditional and iterative structure, uses them on to a sample program, and gets the state  changes under any preconditions.


Key words: secure operating system, formal verification, Isabelle/HOL, Hoare logic