A security verification method for information flow security policies implemented in operating systems

Nowadays, operating system security depends much on the security policies implemented in the system. It's necessary to verify whether the secure operating system's implementation of security policies is correct. The paper provides a general and automaticable security verification method which is suitable for deploying in practice to verify information flow security policies implemented in information systems specially in secure operating systems. We first use information flow graphs (IFG) to express the information flow security policies specified by temporal logic. Then, based on the express method, we supply a verification framework to verify whether the implementation of an information system satisfies the restrictions of security policies. At last, a security verification framework based on mandatory access control (MAC) which is fit for current secure operating systems has been given.