Formal Specification and Verification of an Eztended 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.
Zhu Hong Zhu Yi Li Chenyang Shi Jie Fu Ge Wang Yuanzhen
Database and Multimedia Technology Research Institute Huazhong University of Science and Technology, Wuhan, Hubei, 430074, P.R China
国际会议
Third Asia-Pacific Trusted Infrastructure Technologies Conference(第三届亚太地区可信基础架构技术大会)(APTC 2008)
武汉
英文
132-141
2008-10-14（万方平台首次上网日期，不代表论文的发表时间）