METHOD FOR DISCOVERY OF OPERATING SYSTEM ACCESS CONTROL VULNERABILITY BASED ON MODEL CHECKING

摘要

Disclosed is a method for discovery of an operating system access control vulnerability based on model checking; in the method, the security attributes of operating system access control are analyzed to provide a system security protocol; an access control model is bui a theorem is used to prove the security analysis of access control; a model checking tool is used to check the consistency of abstract machine specifications and check the correctness and completeness of components, achieving vulnerability discovery of operating system access control. The method provides theoretical and technical support for research on operating system security protection.