Method for verifying security model of computer system

Abstract

The invention discloses a method for verifying a security model of a computer system, and belongs to the technical field of security of an operating system. The method provided by the invention comprises the steps: (1) an ML (modeling language) modeling module describes the dynamic and the static attributes of a security model of a computer system by adopting of a UML (unified modeling language) description language to obtain the UML model of the security model of the computer system; (2) a security attribute to be verified is described through a mathematical logical formula adopted by a preset formal verification tool; (3) the UML model is converted into an input model, capable of being processed by the preset formal verification tool, through a UML model conversion module; and (4) state traversal is performed on the input model through the preset formal verification tool, the satisifiability of the formula obtained in the step (2) on each state is calculated, and verified results are output. By means of the invention, the automation degree of verification and the verification capability are improved, and at the same time, the structural defects of the security model per se and the condition of violation of a time sequence attribute can be verified.

Description

technical field [0001] The invention belongs to the technical field of operating system security, and in particular relates to a computer system security model verification method. Background technique [0002] With the rapid development of computer technology and communication technology and the continuous increase of user needs, computer operating systems, as the underlying software of various applications, are increasingly dependent on them. However, while enjoying the powerful functions and convenience brought by computing technology and the accompanying network communication technology, people are also facing increasingly severe information security situation. Introducing a security model in the system design stage can root out the opportunities left to hackers due to design flaws. Therefore, how to verify whether the security model adopted by a computer system is correct or not has become a research hotspot in the field of computer security. Formal technology has rece...

AI Technical Summary

Problems solved by technology

This method tries to analyze the security model by using mature automatic analysis tools for model checking. However, its modeling method is completed manually by the verifier, which requires very familiarity with the model checking technology, otherwise a slight negligence will lead to the failure of the constructed model. The problem with state explosion

The third type of method uses the UML language familiar to developers to describe the security model. This method can only construct the static structure of the security model at present, and cannot reflect the dynamic attributes of the security model. The timing behavior of the model is judged

Images