数据库管理系统强制访问控制形式化分析与明证  

Formal Verification of Mandatory Access Control for Database Management Systems

作　　者：朱薏[1] 朱虹[1] 谢美意[1] 冯玉才[1] 

机构地区：[1]华中科技大学计算机科学与技术学院,武汉430074

出　　处：《小型微型计算机系统》2015年第3期401-407,共7页Journal of Chinese Computer Systems

基　　金：国家核高基重大专项(2010ZX01042-001-003-03)资助

摘　　要：强制访问控制是保护数据库管理系统安全的有效机制.DMOSMAC是一个依赖于安全操作系统实现强制访问控制机制的数据库管理系统.在分析该系统实现的基础上,对该系统进行了形式化分析.给出了信息流的概念,将信息流集合作为被验证系统状态的一部分.信息流集合始终是一个递增的集合,利用信息集合流可防止删除等操作的证明被绕过的可能,保证验证过程的严密性.在信息流的基础上提出了一种对系统代码进行抽象、抽取的形式化分析方法.即抽象DMOSMAC系统状态,从源代码中提取操作规则,将BLP模型中的状态、访问规则分别与DMOSMAC系统的状态、操作规则建立映射关系,BLP模型中简单安全性和*-特性转换为面向信息流的状态不变式,继承BLP模型的相关安全公理和定理进行分析和证明;最后用定理证明器COQ进行安全性证明的方法.Mandatory Access Control is one of the essential secure mechanisms for a DBMS. In a DMOSMAC system, the mandatory access control is implemented based on the mandatory access control mechanism of a secure operating system. The system is verified formally and the implementation of the system is analyzed. The concept of information flow is presented in this paper. The set of infor- mation flow is one of the elements of the system status for the DMOSMAC system and the set of the information flow increases so that the circumvention of verification for delete operation （ and so on） is prevented. Therefore, the rigidity of the verification is preserved. Based on information flow, a method of formal verification for source codes of a DBMS system is proposed：extracting the system sta- tus and operational rules from source codes of DMOSMAC to ensure that the verification is accordance with the implementation;map- ping the system status and operational rules of the BLP model to the status and operational rules of the DMOSMAC; adapting the sim- ple security property and ＊ - property in BLP model into the invariants for information flow; verifying the security based on the axioms and theorems in the BLP model. The theorem prover COQ is used to verify the security of the DMOSMAC system.

关 键 词：强制访问控制 形式化验证 信息流 定理证明器Coq 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]