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

摘要 强制访问控制是保护数据库管理系统安全的有效机制.DMOSMAC是一个依赖于安全操作系统实现强制访问控制机制的数据库管理系统.在分析该系统实现的基础上，对该系统进行了形式化分析.给出了信息流的概念，将信息流集合作为被验证系统状态的一部分.信息流集合始终是一个递增的集合，利用信息集合流可防止删除等操作的证明被绕过的可能,保证验证过程的严密性.在信息流的基础上提出了一种对系统代码进行抽象、抽取的形式化分析方法.即抽象DMOSMAC系统状态，从源代码中提取操作规则，将BLP模型中的状态、访问规则分别与DMOSMAC系统的状态、操作规则建立映射关系，BLP模型中简单安全性和*-特性转换为面向信息流的状态不变式，继承BLP模型的相关安全公理和定理进行分析和证明；最后用定理证明器COQ进行安全性证明的方法