A Method for Discovering Vulnerabilities of Operating System Access Control Based on Model Checking

Abstract

The invention discloses a method for discovering the vulnerability of operating system access control based on model detection. The method analyzes the security attributes of the operating system access control, provides system security regulations, constructs an access control model, and uses theorem proof to conduct security analysis on access control. , through the model checking tool to check the consistency of the abstract machine specification and the correctness and completeness of the components, and realize the vulnerability discovery of the access control of the operating system. This method provides theoretical and technical support for the research on operating system security protection.

Description

technical field [0001] The invention relates to the field of operating system access control vulnerability discovery, in particular to a method for discovering operating system access control vulnerability based on model detection. Background technique [0002] The operating system uses a variety of access controls for system protection, but there are still many security holes exposed in access control granularity and authorization management, such as privilege escalation and privilege leakage. Although scholars at home and abroad have proposed some access control improvement schemes to deal with various security threats and exploit attacks, under the current situation of serious system fragmentation, access control schemes that rely on system versions have exposed application limitations, and the implementation of the scheme is lacking. Theoretical analysis and verification, the certainty of its security policy is difficult to guarantee, so the completeness and correctness ...

AI Technical Summary

Problems solved by technology

Although scholars at home and abroad have proposed some access control improvement schemes to deal with various security threats and exploit attacks, under the current situation of serious system fragmentation, access control schemes that rely on system versions have exposed application limitations, and the implementation of the scheme is lacking. Theoretical analysis and verification, the certainty of its security policy is difficult to guarantee, so the completeness and correctness of the rules cannot be guaranteed

Part of the work uses formal methods to assist in analyzing the vulnerability of the system. However, these methods have a high level of abstraction and lack of application in real systems.

Images