Model Checking for Security Policy of A High Secure Operating System

摘要

Security is the most important property of operating system. Model checking is a technique that relies on building a finite model of the system and checks whether the desired properties hold in that model. In this paper, we use model checking to formally verify security policy of a high secure operating system. One important aspect of secure operating system design is mandatory access control mechanisms. We firstly proposed a security policy based on unified information flow analysis. Then, this paper gives a formal semantics for the security policy, which is used to support and ensure secure communication between processes.