The Formal Model of DBMS Enforcing Multiple Security Polices

摘要

The formal security policy model and securityanalysis is necessary to help Database Management System(DBMS) to attain a higher assurance level. In this paper wedevelop a formal security model for a DBMS enforcingmultiple security policies including mandatory multilevelsecurity policy, discretionary access control policy and rolebased access control policy. A novel composition scheme ofpolicies is introduced. And the security properties arecomprehensively and accurately specified in terms of about17 state invariants and state transition constraints.Furthermore, the security of the model is proved with theZ/EVES theorem prover.