Formal Specification and Verification of an Extended Security Policy Model for Database Systems

In order to develop highly secure database systems to meet the requirements for class B2, an extended formal security policy model based on the BLP model is presented in this paper. A method for verifying security model for database systems is proposed. According to this method, the development of a formal specification and verification to ensure the security of the extended model is introduced. During the process of the verification, a number of mistakes have been identified and corrections have been made. Both the specification and verification are developed in Coq proof assistant. Our formal security model was improved and has been verified secure. This work demonstrates that our verification method is effective and sufficient and illustrates the necessity for formal verification of the extended model by using tools.