Information system security function validating using model checking

Information systems will be encountered more and more security threats due to the development of computer attack method and technology. Generally, different security policies are used to protect the sensitive information in these systems. There has been a lot of study on security policy conformance and completeness verification and validation. However, there have few researches to validate whether the system behaviors satisfy the security policies. A model checking based information system security function validation method is proposed to validate the conformance between the system security solutions and the security policies in this paper. The system behaviors and the security policies are modeled separately, and the consistency between them is validated using the model checker SPIN.