Research On Formal Analysis For Security Of Database Management System

The application of database has gone deep into each field and a lot of sensitive data which the attacker wants stored in the database, the security problems of database aroused general concern. Research and develop database management system with high security levels, is of great significance for improving the security of database system.When developing database management system with security level4and higher, we need to introduce the formal analysis technology to analyse the security model, FTLS, even system code, that our system can meet the requirements of security model.Considering the new types of complex objecst emerged from database and according to the characteristic of procedure and trigger about the security, an extended security model based on BLP was presented which make procedure and trigger operated securely.The model extended the state transition rules, the object compatibility. Entity integrity together with object compatibility as invariants of the model for every state, make sure that the state of the system is correct and coincident.For the new database security model, a specification and formal analysis of the model based on theorem prover Coq are given.The statu invairents, security axiom, lemma deduction, specification description, and all state transition rules are specificatied and formal analysed in the paper, through which, we revised the new model and get secure model.According to multilevel security database management system, the specification and formal analysis of FTLS basted on the data dictionary are given. The multilevel security data dictionary as members of the security state of the database management system is defined, based on which the state of the system description, state invariants, and system operation rules are given. The specification and formal analysi of FTLS is given based on Coq. Through the analysis, the defects of the original specification in the design are corrected, which shows FTLS meetS the requirements of security model.During mapping the BLP model directly to the source code, problems on of the accessible set by delete operation is found, wich make the delete operation always secure without anypremise conditions, which is unsecure when applying to database. The mandatory access control of database management system (DMOSMAC) is realized on secure operating system, the code quantity of which is small. With this feature, we formally analyse the DMOSMAC to insure that DMOSMAC implements the security policies. Gives the concept of information flow with in database, based on which a, extraction methods for system code is provided to formal analysis. The results show that the method can effectively avoid the bypass problem. Finally the DMOSMAC system is formally analysed secure.Through the above research, our method in formaliy analyzing model and its FTLS, can be used as analysis in the same architecture of the system, and method used in modeling is also have important reference value.