The correctness of design and implementation of operating system is difficult to be described and verified with the traditional methods, due to the huge size of the system. In this paper, a model is build for the functionality semantics of the system modules on the assembly layer. A system state model is proposed as the link of the design and verification on the assembly layer. Through defining the legal states and state transition functions, the universe of discourse of the system state model and the assembly layer are constructed. The correctness of functionality modules is verified to ensure the correctness of design and functionality implementation. Within the Isabelle/HOL theorem prover, the system state model is described, and the correctness of functionality semantics of the system modules is verified. Meanwhile, the self-implemented secure trusted operating system (verified secure operating system, VSOS) is used as the example to illustrate the proposed formal method for design and verification, and to show the feasibility of the method.