数据库的应用已经渗透到各个领域,数据库中存储的大量敏感数据是攻击者所觊觎的,数据库的安全问题一直备受关注。研究并开发高安全等级的数据库管理系统,对于提高数据库系统的安全性具有重要意义。在开发四级及以上的高安全等级的数据库管理系统过程中,需要引入形式化分析技术,对安全模型、顶层规范甚至系统代码进行分析,以保障系统在设计和实现上符合安全模型的要求。针对传统的数据库形式化安全模型在存储过程、触发器的处理上可能存在的安全缺陷,改进了数据库安全模型,使得该模型能够安全地处理存储过程和触发器等数据库对象。该模型扩充了状态转换规则,改进了客体兼容性,将实体完整性、参照完整性和客体兼容性作为所有状态应满足的安全性质,保证系统状态的正确性与一致性。针对新的数据库安全模型,给出了基于定理证明器Coq的安全模型规范和安全性分析,给出了用于安全性分析的状态不变式、相关公理、引理和推论,以及各状态转换规则的规范描述和证明步骤,通过形式化分析,修改了新模型存在的不足,表明新模型是安全的。针对多级安全数据库管理系统,给出了基于安全数据字典的多级安全数据库管理系统顶层规范形式化分析。定义了多级安全数据字典作为安全数据库管理系统的状态的成员,基于该系统状态和状态不变式、系统操作规则的形式化规范描述,给出了基于数据字典的顶层抽象规范的安全性形式化分析,对数据库管理系统顶层规范进行了基于定理证明器Coq的描述和安全性分析,改进了原有的系统顶层规范在设计过程中的缺陷,表明顶层规范的设计是符合安全模型要求的。在将BLP模型直接扩展映射到源代码进行分析的过程中,针对数据库管理系统的特点,对BLP模型中描述系统状态的元素可访问集分析后,发现在删除操作的分析中,后状态满足某些安全性质时,实际上并不需要满足删除操作的任何前提条件,就可以证明得到后状态是安全的,证明有被绕过的可能,不能保证证明的完备性和严密性。利用完全依赖于安全操作系统实现强制访问控制的数据库管理系统DMOSMAC代码规模小的特点,对DMOSMAC进行了形式化分析和证明,以确保DMOSMAC正确实现了安全策略。给出了这类体系结构下的数据库管理系统进行形式化分析的方法。给出了数据库内的信息流定义,在此基础上给出了一种对系统代码进行抽取,避免删除等操作的证明被绕过的可能,保证安全性分析过程的严密性。结果表明该方法能够有效避免BLP模型直接用于数据库系统安全性形式化分析时可能引起的证明被绕过的问题。通过以上研究,我们在数据库管理系统的形式化安全模型及其安全性分析、顶层规范以及实现级安全性分析等方面进行了研究,所提出的方法可用于与相同体系结构的系统的分析和证明。