Survey of Safety and Security Verification of Operating System Kernel Based on Formal Method

Abstract:
The OS kernel implements the basic functions of the OS. Verifying the kernel to ensure that it meets specific needs has been a research hotspot in industry and academia. This paper analyzes the safety and security verification of OS kernel based on formal methods. First of all, the visual analysis of the safety and security verification of the OS is used to grasp the development trend of the research on a macro scale. Then summarize the definitions of safety and security in multiple related standards and literature. On this basis, the safety and security verification of the OS kernel and the application of formal methods are analyzed through systematic literature review methods. Finally, interviews were conducted with OS designers, testers, and users through questionnaire surveys to summarize the cognitive differences between the industrial and academic circles.