Research on Formal Design and Verification of Operating Systems

The security of operating system is the foundation of information system. There is no recognized answer about how to guarantee the OS security. The accepted and reliable approach is to validate the design and implementation of OS with formal methods of mathematical logic reasoning. In this paper, we propose to use the "lightweight" formal method to describe and design the system. Through the formalization of OS functionality model and security requirements, we can get the description of system functionality design and security requirements on the same domain. We use logical reasoning to verify whether the system functionality design meets the security requirements. If the verification cannot pass, indicating that there are problems in the system functionality design, then we improve the design and implementation, and verify the re-designed functionality again. The verification result shows that the proposed method is feasible.