数据库形式化安全策略模型建模及分析方法

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

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

1 引言

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

安全策略模型是独立于软件实现的高层概念模型，它来源于需求规约，描述安全系统的安全保护需求与功能性质[2]。安全策略模型的形式化分析是评估第四级系统[1]的重要内容之一，在许多应用领域都扮演着重要的角色，如建立可信操作系统、可信数据库管理系统等高可信软件系统。目前，通过一系列形式化方法在工程中的应用[3～5]，对系统进行形式化描述和验证不仅可以发现系统设计上的问题、验证系统设计的正确性，而且还可以指导开发、检验系统实现的正确性等。然而在数据库安全领域，现有的形式化方法还不能满足实际需求。此外形式化方法在很大程度上受到其支持工具的限制，一些语言和分析方法由于缺乏原生分析工具的支持，导致验证效率不能满足大型复杂系统的工程需求。如Z语言，在20世纪80年代末到90年代初国际上相继提出了很多Z语言的扩展，并进行了一些标准化工作，提出了与形式化方法和面向对象方法相结合的思想[6,7]。然而，虽然基于Z语言的形式化方法和相关工具得到了发展，但是仍然无法支持在数据库等大型复杂系统的工程应用。

针对这些问题，本文提出了一种高等级数据库形式化安全策略模型的建模方法，并将其应用于实际商用数据库 BeyonDB中进行有效性验证。该数据库经相关测评机构测评已达到第三级，并具备部分第四级安全特性。将本文提出的建模与分析方法应用于 BeyonDB安全功能设计与开发中，帮助发现并纠正了系统若干设计缺陷，取得了良好的实际效果。

2 相关工作

近年来，国内外已逐渐开展了形式化方法在各类模型及实际系统中的安全分析的研究，如操作系统、防火墙等。Qian等[8]采用数学形式化方法，使用OSOSM对操作系统进行建模并采用Isabelle验证，保证了系统的高度安全性。Yang等[9]从完整性模型的实用性角度出发，提出一种新型的动态完整性保护模型（DMIP, dynamic integrity protection model），并给出了形式化分析。还有部分工作提出了在形式化安全策略模型验证的基础上对目标系统进行测试的方法。数据库的安全策略模型形式化分析，由于其分析规模和主客体的复杂性，目前仍然缺少实际商用的安全策略模型的形式化建模与分析方法。

Bell和LaPadula在1975年提出了BLP经典模型[10]，基于该模型提出了保护数据机密性的重要思想，为后来数据库管理系统各种安全策略模型的建立奠定了坚实的基础。SeaView模型[11]基于BLP经典模型，详细提出了 16条完整性约束，分析了包括自主访问控制（DAC, discretionary access control）和强制访问控制（MAC, mandatory access control）等安全模型，访问控制粒度实现元素级，为多级安全数据库的设计和分析提出了良好的基础。但是，SeaView模型[11]采用的是 TCB子集架构[12]，将数据库管理系统与 TCB分开描述，不能满足当今大部分采用可信主体架构[12]的商用数据库的形式化分析需求。Li等[13]提出了一种基于Z语言的策略模型形式化方法，并且以BLP模型为例进行了验证。Zhu等[14]扩展了SeaView模型的客体结构，在丰富了客体类型的同时扩展了安全属性，并用 Gallina语言对其进行了形式化描述，在Coq定理证明器帮助下对模型进行了证明。Sandhu[15]提出了基于角色进行访问控制的RBAC（role-based access control）模型，该模型将权限与角色相关联，通过角色获取的权限进行访问控制，极大地简化了权限的管理。He等[16]不仅提出了详细的安全属性，还将BLP模型和RBAC模型进行了逻辑结合，采用Z语言对该模型进行形式化描述，实现了多策略的数据库管理系统访问控制。

上述相关工作多数集中于对 DBMS的通用模型部分进行研究，其访问控制粒度较粗，不满足高等级系统要求；或提出新的数据库安全策略模型，并进行形式化分析，没有考虑数据库系统完整性约束等固有属性，缺少从实际数据库系统建立安全策略模型的方法。更加缺少对实际商用数据库管理系统的安全策略模型进行描述和分析。

基于以上原因，本文提出了一种数据库形式化建模和安全性分析方法，该方法建立的模型能够提供更加完整的安全属性描述，更加灵活的可扩展性，保证了建模和验证的效率，并且应用于实际数据库系统，发现数据库安全功能设计和实现中的错误和缺陷，验证了其有效性。

3 PVS语言及定理证明器

本文采用了国际上较为流行的 PVS语言和验证工具作为形式化方法的基础。该系统由斯坦福研究机构开发，包括PVS规约语言和PVS定理证明器2部分组成：前者基于高阶逻辑，具有丰富的数据类型系统，表达能力强；后者采用目标制导的方式工作，即一个证明的构造从待证明的定理开始，逐步推理，不断生成子目标，直至所有子目标均为真。PVS定理证明器拥有强大灵活的命令集。高效的决策过程、高度交互与自动化的定理证明使PVS在当今形式化语言中较有优势。

PVS语言不但拥有强有力的推理机制，而且有丰富的表达手段，目前已在很多领域得到应用。典型应用包括：我国国内可信电子电力系统的建模与证明、轨交控制系统的SCADE开发和国际上NASA的对基于时间触发以太网的时钟同步协议的形式化验证等。

4 安全策略形式化描述方法

国标GB17859-1999[1]中指出：为了满足结构化保护系统功能的安全性要求，安全策略模型的形式化应该至少包含自主访问控制和强制访问控制。因此，以BeyonDB系统对BLP模型的实现为例展示本文的建模方法，流程如图1所示。为使形式化模型与实际数据库保持高度的一致性，将形式化安全策略模型的描述和安全性分析分为3个部分。

1) 模型目标提取：抽取必要的实体与操作。

2) 系统状态、操作规则生成与描述：对数据库相关实体进行分析、描述、综合生成系统状态；利用系统状态中描述的实体等内容描述操作规则。

3) 描述安全定义并进行安全性分析：描述系统安全定义，对模型进行安全分析，交互式证明安全定理。通过安全分析发现系统安全缺陷，指导修改系统设计。重复以上步骤，不断完善形式化模型。

4.1 模型目标提取

对于形式化模型中应该具体描述的实体，抽取途径主要是通过系统中顶层的访问控制接口、安全需求以及数据库系统实际的系统表，采用基于操作接口的目标提取方法来获取描述目标，即对于一个指定的访问控制接口，统一以操作者、操作目标、操作成功判断条件的形式对每一个操作接口进行描述和分析。如表1所示，在BeyonDB数据库中，根据实际操作接口 Insert，结合实际存在的系统表iiuser，将操作者抽象为模型中的主体：User；根据操作的对象实体表格，抽象出客体：Realtable；同时在实际的强制访问控制和自主访问控制中需要判断实关系表和操作者的标签支配关系，所以需要对标签（Label）和标签支配判断函数（dom?）进行描述并定义。按此方法对系统中所有接口进行描述，分类总结出系统的基本元素，为下一步的形式化语言描述提供必要基础。

图1 形式化建模与安全分析流程

表1 操作Insert的描述目标提取

4.2 系统状态生成与描述

完成了上述基于操作接口的目标提取后，使用PVS语言对提取出的元素进行描述，描述内容包括实体、与数据完整性相关的约束元素、访问控制相关元素、系统状态、操作规则。在描述中，为了使形式化模型具有较高的可读性和验证的效率，充分应用 PVS语言中一些内置类型、类型构造器及函数。例如采用PVS语言中的集合类型来描述实体，在判断某一类型的实体时，利用PVS语言内置函数member能够方便判断某一元素是否存在于某一指定的集合当中。如系统状态，为了快速提取状态中某一内容，采用记录类型对状态进行描述，同时也提高了代码的可读性。

4.2.1 实体描述

1) 主体存在

本文使用集合类型对各类实体进行描述，优点是可以直接利用PVS定理证明器内置的member和subset函数来判断某一个元素是否在一个集合中或一个集合是否是另外一个集合的子集。同时为了增加语言的可读性和使用的灵活性，采用记录类型描述所有主体集合（主体存在Subject_Exist），每一类主体集合作为记录中的一个域，例如 UserExist是主体的集合，RoleExist是角色的集合。主体存在描述具体如图2所示。

图2 主体存在描述

2) 主体映射

主体映射描述了数据库中相关联主体间的对应关系，如用户与组、用户与轮廓以及用户与角色等。各类对应关系均采用PVS语言中的函数类型来描述，如引入函数类型映射 UsertoType:TYPE=[USER->USER_TYPE]描述用户到用户类型，再将各类与主体相关的函数映射组织成记录类型Subject_Map（如图3所示），Subject_Map的生成为自主访问控制和强制访问控制提供了方便的依据。

图3 主体映射描述

3) 客体存在

将除数据库客体以外的其他客体分为2类，一类是具有层次结构的客体，如实关系表、元组、视图；另一类是不具有层次关系的客体，如事件、序列、过程。模型中，将客体组织成如下树形结构，如图4所示。为了描述数据库中复杂的客体和繁多的完整性关系，使用记录格式ObjectExist描述模型中不同类型的客体，每一类客体集合作为记录一个域，分别包括数据库、实关系表、视图和元组。

图4 数据库客体层次结构

4) 客体映射

客体映射是各客体间的层次关系的抽象描述。通常采用的描述方法是，参照BeyonDB设计文档，依据系统中各类系统表，将相关系统表关联并抽象定义。例如，将设计文档中iintegrity与iikey这2张系统表进行关联并抽象，得到关系表与其引用表的映射 Realtable_Reftable。为方便描述数据库系统的引用完整性这一固有属性，要对必要的实体间映射进行描述，包括关系表与被引用表的映射RefTable_RealTable、元组与主键的映射Tuple_PKey、元组与外键的映射Tuple_FKey。客体间的映射函数应至少包含上述内容，映射关系如图5所示。以上映射函数的描述为下文安全属性定义提供基础。

图5 客体关系映射

4.2.2 策略相关元素描述

自主访问控制和强制访问控制的形式化证明是国家相关标准要求中的必要内容。以 BeyonDB为例，自主访问控制通过以下步骤进行：首先获得该用户拥有的权限，其次判断指定权限是否在其中。按照系统设计文档对该步骤进行细化，分别定义主体权限、客体权限、数据库权限。为了满足系统的可信主体权限最小化原则，将主体权限细分为系统权限、审计权限、安全权限，相应定义了用户到其拥有的不同类型权限的函数映射，并组织为记录类型DAC_Table。强制访问控制的核心操作是标签支配判断，首先分别获得主客体标签，然后进行标签对比判断。由此定义2个函数：主体到主体标签的函数映射和客体到客体标签的函数映射。最后，根据断言dom？如图6所示定义来进行标签支配判断（如下规约描述，返回一个BOOL 类型）。

图6 dom?规约描述

同时为了增加系统的灵活性，能够在会话当中动态调节主客体的标签，根据系统中描述的最低、最高安全等级，最小、最大范畴，定义模型中安全等级范围和范畴范围，如图7所示，均采用记录类型描述，这样便于对极限值的获取。另外，为了记录登录用户和数据库的相关信息，定义一个会话记录，通过会话记录（下面表达式中的session）可以方便提取与登录用户和数据库相关的内容。在安全约束属性描述中，为了给安全定义中的状态属性的证明提供依据，对当前用户的合法操作进行记录，定义一个记录类型的动作记录 Action_ID，再根据访问控制不同分别用 Cur_Perms_DAC和 Cur_Perm_MAC 表示记录的集合。

图7 级别、范畴规约描述

4.2.3 系统状态描述

一个数据库的系统状态应该包含所有评估者关心的数据，仅对模型各单位元素进行描述是不充分的。本文使用记录类型描述系统状态 system_state，并将不同类型的实体、关系映射、访问控制等内容组织成系统状态中的一个域。这样可以根据操作的需要从系统状态中提取出相关的信息。system_state通过具体操作、安全属性集合及实体关系集合进行获取生成，具体算法如下。

系统状态获取算法

算法GetSystemState

输入：操作集合OPERATIONS ，安全属性集合INVARIANTS，实体或关系集合VARS

输出：系统状态SYSTEM_STATE

4.2.4 操作规则

操作规则（operation rules）描述了模型是如何具体实施安全策略的，揭示了2个连续状态的状态转换过程中状态变量之间的关系。针对不同操作，操作规则包括操作发生条件与操作执行影响 2部分。操作发生条件即操作成功判断条件，如强制访问控制的标签支配判断、自主访问控制授权检查。操作执行影响主要描述的是操作执行后系统状态变量的改变。操作规则的产生是将操作判断条件和操作执行后系统状态变量的改变进行逻辑组合，具体算法如下所示。

操作规则生成算法

算法 Operation Rules Generation

输入：系统状态SS0，基于操作接口的目标提取方法中的各项操作成功判断条件的逻辑与集合CONS，初始操作规则序列Rules

输出：操作规则序列Rules

5 形式化策略模型安全分析

5.1 安全定义

在国标[1]对第四级的信息系统明确要求了自主访问控制和强制访问控制，此外针对不同的信息系统，还有其他特别的安全需求。对具体的数据库系统来说，安全属性的定义应该从2个方面进行该考虑，首先是为满足国家标准的安全属性内容，主要是以经典安全策略模型作为基础（自主访问控制、强制访问控制）；其次是针对不同系统的具体安全需求。例如，数据库需要添加的固有的一些安全属性（如实体完整性、引用完整性、用户自定义完整性）。通过将要求的安全需求内容与实际系统安全需求内容结合定义出多条安全属性。在安全属性基础之上，根据形式化验证目标将不同安全属性通过PVS中的逻辑运算符“and”进行连接来定义状态安全，如图8所示。具体地，针对BeyonDB，本文将数据库安全属性分为6条，包括主体标签支配会话标签，客体间标签支配（关系标签支配数据库标签，元组标签支配关系标签），自主访问控制，简单安全，*安全以及引用安全属性。

图8 安全定义与安全性分析

安全属性1（主体标签支配）：会话的发起者即当前用户必须支配当前会话的安全标签。

图9 主体标签支配描述

安全属性2（客体间标签支配）：为了达到更细粒度的标签控制，需要满足以下条件：关系的安全等级支配其所属数据库的安全等级；元组的安全等级支配其所属的实关系表的安全等级（如图10所示）。

图10 客体标签支配描述

安全属性 3（自主安全）：根据 cur_perms_DAC，如果当前用户对某些客体进行过操作合法，那么该用户必然是当前客体的属主或者对该客体具有相应的客体权限（如图11所示）。

图11 自主安全描述

安全属性4（引用完整性）：数据完整性对数据库来说至关重要，数据库中的数据是否满足完整性关系到其能否真实反映出现实世界，能否在数据库中保护数据的正确性、有效性和相容性。尤其对于引用完整性，BeyonDB系统中采用了3种不同的策略，级联删除、受限删除、置空删除。可以根据需要采用不同的默认策略，这里限于篇幅原因描述受限删除时的系统引用完整性如图12所示，要求某一元组的外键要么全空，要么全部非空（此种情况必定存在相应的一个被引用的表的元组，使其主键等于该元组的外键并且安全等级应该支配被引用表的安全等级）。

图12 引用完整性描述

安全属性5（简单安全性）：根据具体的数据库的要求将BLP模型调整为：如果一个用户对某客体进行了读的操作，那么当前用户的安全标签应该支配该客体的安全标签从而达到不上读的要求（如图13所示）。

图13 简单安全性描述

安全属性 6（*安全性）：如果一个用户对某客体进行了写操作，那么该客体的安全标签一定支配当前用户的安全标签以达到不下写的安全要求，如图14所示。

图14 *安全

5.2 安全性分析

仅仅定义出模型的各种元素是不充分的，必须对模型进行形式化的分析，即验证模型描述的系统的安全性，系统处于安全的状态。

因此系统状态安全定义应该是上述安全属性、数据库特有属性约束和类型约束的组合。形式化定义如图15所示。

图15 形式化定义

该安全定义是以PVS断言的and连接生成，可以灵活地添加各类数据库属性作为安全状态的描述。由于 PVS能够对已证明的片段进行保存，并可将已存的证明片段用于整体的证明过程。故以该方式定义的状态安全在保证不影响已分析过的内容的同时，增加新的安全断言，从而使建模和分析的效率更高。

本文提出的安全性分析的思路是：首先使用do_init 函数对系统状态进行初始化，得到初始状态 init_ss0，然后根据状态安全定义 State_Safe?分析初始状态 init_ss0是否为安全状态；然后，根据状态安全的定义判断任意状态 SS0是否安全，如果SS0安全则通过状态转移规则函数对SS0进行操作得到状态SS1，则SS1也是安全的；重复上述操作直至所有可达状态判断完毕，如果所有可达状态都是安全的那么数据库系统就是安全的。由此，需要的安全定理包括：初始状态安全定理和状态转换安全定理。

初始状态安全定理 系统进行初始化操作后得到的状态满足安全状态的定义。即要证明的基本安全定理如图16所示。

图16 初始状态安全定理

状态转换安全定理 针对每一个操作，都应保证对于一个安全状态进行操作OP之后得可达状态仍然是安全的。即操作运行之前处于安全状态操作运行之后仍然处与安全状态。

表达式为：状态SS0安全and操作OP则可达状态SS1也安全。即需要证明的状态转换安全定理如图17所示。

图17 安全定理

若能够证明 InitialSafe和任意操作后的SecurityTheorem则系统就是安全的。本文采用PVS交互式证明对如上2个定理进行证明。并且发现了BeyonDB的一些缺陷。

在安全证明中，通常情况下很难一次证明成功，下面结合一些例子，举出3类典型的错误原因。

原因一：模型与设计不统一，如 BeyonDB中要求一张引用表只能应用到一张被引用表，则在形式化描述模型中引用表到被引用的映射关系（单向）则应该是一对一的关系。如果遇到此类问题，需要检查描述的模型，将模型与系统的实际设计严格对应，防止不一致的问题发生。

原因二：模型未消除设计中的二义性，模型内部存在矛盾和不一致性。如模型变量需要常量化时，需要保证该常量符与其他位置同一变量的常量符一致。这种问题的发生是因为对PVS证明机制没有清楚了解，所以针对证明过程中使用的命令，需要明确命令的证明过程，尤其涉及到变量常量化的命令。

原因三：模型与设计相符，且描述方面没有问题，仍然无法证明，则发现了系统设计中的确存在缺陷。

5.3 系统存在缺陷

将本文提出的方法对实际的商用数据库BeyonDB进行分析，发现其一些典型的问题，并给而解决方案（如表 2所示），此时需要在系统中进行试验确定系统漏洞，从而发现实际系统的安全缺陷，指导修改系统设计。

发生问题的主要类型有：系统设计本身不完整；操作执行时不满足安全属性。

1) 策略设计不完整：制定策略时，忽略一些细节，尤其像对 procedure这种实体进行操作时容易出现问题。因为 procedure实体涉及到若干个不同安全等级的客体，如果仅仅考虑用户主体安全标签与 procedure安全标签的标签支配是不充分的。例如一个低等级用户的安全标签等级支配 procedure的安全标签等级，系统中要求执行者具有exec的权限。不关注用户和所有涉及其他客体等级支配关系。当 procedure中包含高于用户等级的客体时，用户执行该procedure，则低安全等级用户间接访问了高安全等级的客体，在操作执行后会对操作所涉及的所有客体进行记录，记录（exec,object1），（exec,object2）等。在进行安全证明时，如果低等级用户“读”访问了高安全等级的客体object1，则证明无法通过简单安全属性，返回系统，修改系统策略，要求在执行 procedure的过程中，用户的标签安全等级需要支配 procedure所包含的所有客体的安全等级。

2) 实体设计不完整：设计系统实体时，存在安全隐患。当一个表格在没有设置主键的情况下，允许插入内容完全相同的记录，且没有序列号区分，例如安全等级为L1的用户创建一个等级为L1的表格T1，插入一条等级为L1的元组R1，并且对该元组执行了 select操作，系统会记录该操作（select,R1）。然后提高了用户自身的等级为L2，并且向L1表中插入等级为L2的相同内容元组R1'，此时当系统进行证明时，当遇到相同内容不同等级的R1和R1'时，无法进行判断，不满足简单安全属性。为了更加符合数据库的完整性要求，所以在没有主键的数据库表格中系统要默认插入一列ID，不允许相同内容的元组存在。

3) 策略执行不满足安全属性：策略设计本身没有问题。但是需要一定的前提条件，必须在满足前提条件的情况下才满足安全属性。

a) 表级、行级开关：在BeyonDB中为了增加系统的灵活性，所以设置了表级还有行级的不同粒度的强制访问控制开关。如果只开启表级的强制访问控制开关未开启行级访问控制开关，如果一位支配表级安全标签等级的主体用户就可以访问该表的所有记录，包含行级安全等级高于用户的记录。给出的解决方法是：表级、行级强制访问控制开关必须同时开启。

b) 在会话中，允许用户修改会话标签，用户安全标签修改后，则操作记录中的部分记录会违背安全属性。比如用户对客体O进行了读操作（用户安全标签等级支配 O），若该用户提高了自身的安全标签等级且支配O，则不满足“简单安全属性”和“星”安全属性。给出的解决方法是：在会话过程中不允许用户修改安全标签。

表2 错误类型以及系统缺陷

5.4 方法对比

本文提出的方法与以往方法比较，描述的粒度是记录级别，并且给出了数据库固有的完整性方面的约束，并给出证明；没有采用 TCB子集架构，这样更符合商用数据库可信系统的要求。将本文方法与其他方法在实际系统相符性、安全属性完整性、可扩展性、建模与验证效率等几个方面进行比较，如表3所示。

表3 方法对比

与实际系统设计相符性：提供了通过系统的变量以及系统表等内容获得实体与关系的方法，不仅仅局限于访问控制的理论模型，而是将实际系统的设计细节反映在模型中，如针对客体定义Owner获取客体的属主，定义ProcedureToObject描述过程与客体的映射，定义Tuple_Fkey描述客体元组到外键的映射。针对主体，定义UserToRole，UserToGroup来描述用户到角色，用户到群组的映射。考虑实际操作系统，定义出更加详细的内容。因此实用性更强，这是传统理论模型分析方法中[7]并没有涉及到的内容。文献[7]中只将客体简单描述为单一客体O_Single并未详细的考虑客体间、主体间的详细内容，仅仅针对DBLP涉及的内容进行描述，局限性较强，并不适合实际的系统。文献[16]中只对粗粒度的Database和Table进行描述，并未对细粒度的Tuple等进行讨论。

安全属性更加完备：安全属性除了需要满足安全测评相关标准对访问控制的需求外，还需结合实际数据库系统，将实体完整性等考虑在内，而文献[16]和文献[7]并没有考虑完整性。文献[7]关注BLP模型文献[16]关注RBAC和BLP模型，仅考虑系统中数据的机密性，忽略数据库完整性。

可扩展性：作为结构化建模方法的保证，采用了可扩展性的构架，在系统状态、安全定义、操作描述等方面采用PVS中的逻辑“与”描述使结构相对于其他方法更加易于扩展，文献[16]描述了不同的不变式，但是受到定理证明器的限制无法将不变式进行逻辑组合，导致部分不变式需要手工证明。

建模与验证效率：迭代式的建模与证明过程使模型修改容易，迭代代价较小，并且PVS原生工具的支持使本文方法在实际工程中有更高的效率。其他文献中，早期是采用手工证明，或者采用Z语言描述，但相应证明器不能提供有效的推理支持，所以在大量需要展开的模式时效率非常低，这就要求在模型描述的时候进行优化，但Z语言描述的模型在修改方面非常困难，故证明的工作量也会增加许多。文献[7]中指出，当展开大量的模式时，定理的证明速度明显放慢。而文献[16]中针对部分的不变式无法采用机器证明，故采用人工证明，大大降低了证明的效率。

综上，本文方法对于大型复杂系统在实际设计开发中应用，能给与足够的支持，帮助发现系统漏洞，指导系统开发并且在系统安全性建模和验证效率方面都拥有更大优势。

6 结束语

本文提出了一种数据库形式化安全策略模型建模与分析方法，为当前第四级安全数据库管理系统的安全策略模型建模与分析提供参考。该方法基于设计文档分析，抽象提取出安全定义和操作规则：前者体现系统关键安全需求，定义模型中状态与状态转移间的约束；后者体现实施安全需求的方式。该方法在 BeyonDB数据库安全策略模型分析中获得了很好的效果，显示出该模型安全属性上的可扩展性和灵活性。采用的 PVS 语言以及其原生的定理证明器使该方法效率得到保障，证明该方法具有良好的可行性。

[1] 国家质量监督检验检疫总局.GB17859-1999计算机信息系统安全保护等级划分准则[S].北京:中国标准出版社,1999.General Administration of Quality Supervision, Inspection and Quarantine of P.R.C. GB17859-1999 Classified Criteria for Security Protection of Computer Information System[S]. Beijing:Standards Press of China, 1999.

[2] 张敏, 冯登国, 陈驰.基于安全策略模型的安全功能测试用例生成方法[J].计算机研宄与发展,2009,46(10):1686-1692.ZHANG M,FENG D G, CHEN C. A security function test suite generation method based on security policy model[J].Journal of Computer Research and Development, 2009, 46(10):1686-1692.

[3] 官尚元,伍卫国,董小社.自动信任协商的形式化描述与验证研究[J].通信学报,2011,32(3):86-99.GUAN S Y, WU W G. DONG X S. Research on formal description and verification of automated trust negotiation[J]. Journal on Communications, 2011, 32(3):86-99.

[4] LUO X Y, TAN Z, SU K L.A verification approach for web service compositions based on epistemic model checking[J].Chinese Journal of Computers, 2011,34(6):1041-1061.

[5] 肖芳雄, 黄志球, 曹子宁. Web 服务组合功能与 QoS 的形式化统一建模和分析[J]. 软件学报, 2011, 22(11): 2698-2715.XIAO F X, HUANG Z Q, CAO Z N. Unified formal modeling and analyzing both functionality and QoS of Web services composition[J].Journal of Software, 2011, 22(11): 2698-2715.

[6] 陈小峰. 可信平台模块的形式化分析和测试[J]. 计算机学报, 2009,32(4): 646-653.CHEN X F. The formal analysis and testing of trusted platform module[J]. Chinese Journal of Computers, 2009, 32(4): 646-653.

[7] 何建波, 卿斯汉, 王超. 对一类多级安全模型安全性的形式化分析[J]. 计算机学报, 2006, 29(8): 1468-1479.HE J B, QING S H, WANG C. Formal safety analysis of a class of multilevel security models[J]. Chinese Journal of Computers, 2006,29(8): 1468-1479.

[8] 钱振江, 黄皓, 宋方敏. 操作系统形式化设计与安全需求的一致性验证研究[J]. 计算机学报, 2014, 37(5): 1082-1099.QIAN Z J, HUANG H, SONG F M. Research on consistency verification of formal design and security requirements for operating system[J]. Chinese Journal of Computers, 2014, 37(5):1082-1099.

[9] 杨涛, 王永刚, 唐礼勇. 一种实用动态完整性保护模型的形式化分析[J]. 计算机研究与发展, 2013, 50(10): 2082-2091.YANG T, WANG Y G, TANG L Y. A practical dynamic integrity protection model[J]. Journal of Computer Research and Development,2013, 50(10): 2082-2091.

[10] BELL D E, LA PADULA L J. Secure computer system: Unified exposition and multics interpretation[R]. MITRE CORP BEDFORD MA, 1976.

[11] LUNT T F, DENNING D E, SCHELL R R,et al. The sea view security model[J]. Software Engineering, IEEE Transactions, 1990,16(6): 593-607.

[12] 张敏, 徐震, 冯登国. 数据库安全[M].北京:科学出版社, 2005.ZHANG M, XU Z, FENG D G. Database Security[M]. Beijing:Science Press, 2005.

[13] 李丽萍, 卿斯汉,周洲仪. 安全策略模型规范及其形式分析技术研究[J]. 通信学报, 2006, 27(6): 94-101.LI L P, QING S H, ZHOU Z Y. Research on formal security policy model specification and its formal analysis[J]. Journal on communications,2006, 27(6): 94-101.

[14] HONG Z, YI Z, L C Y,et al. Formal specification and verification of an extended security policy model for database systems[A]. Trusted Infrastructure Technologies Conference[C]. 2008. 132-141.

[15] SANDHU R S, COYNE E J, FEINSTEIN H L,et al. Role-based access control models[J]. Computer, 1996, 29(2): 38-47.

[16] HE Y Z, HAN Z, FU H,et al. The formal model of DBMS enforcing multiple security polices[J]. Journal of Software, 2010, 5(5): 514-521.