王榕，张敏，冯登国，李昊

（1. 中国科学院 软件研究所 可信计算与信息保障实验室，北京 100190；2. 中国科学院大学，北京 100190；3. 中国科学院 软件研究所 计算机科学国家重点实验室，北京 100190）

1 引言

数据库管理系统是多数信息系统的重要基础平台，其安全性是信息系统安全中的重要环节。近年来，伴随着国家信息化建设飞速发展，我国对数据库系统的安全也逐步重视，已有一批达到国标[1]第三级产品，在军用、政务、电力、通信、铁路等国家重要领域逐渐得到应用推广，取代国外同类产品，发挥骨干支撑作用。但是随着国家信息化程度的提高，现有第三级数据库产品已经逐渐不能满足安全需求。因此，迫切需要开展高安全等级数据库构建与评估技术的研究。而本文关注的安全策略模型建模与分析就是其核心技术之一。

安全策略模型是独立于软件实现的高层概念模型，它来源于需求规约，描述安全系统的安全保护需求与功能性质[2]。安全策略模型的形式化分析是评估第四级系统[1]的重要内容之一，在许多应用领域都扮演着重要的角色，如建立可信操作系统、可信数据库管理系统等高可信软件系统。目前，通过一系列形式化方法在工程中的应用[3～5]，对系统进行形式化描述和验证不仅可以发现系统设计上的问题、验证系统设计的正确性，而且还可以指导开发、检验系统实现的正确性等。然而在数据库安全领域，现有的形式化方法还不能满足实际需求。……