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

doi:10.11959/j.issn.1000-436x.2015151

摘要/Abstract

摘要：

目前数据库形式化安全策略模型存在抽象层次较高、缺乏对数据库状态与约束的充分描述等问题，难以辅助用户发现商用数据库设计中的微小缺陷。提出了一种基于PVS语言的数据库形式化安全策略模型建模和分析方法，该方法较以往模型能够更加贴近实际数据库，应用范围更广，安全属性描述更加完整，描述的模型具有灵活的可扩展性，并且保证了建模与验证的效率。最后，将该方法应用于数据库管理系统 BeyonDB 的安全策略建模分析中，帮助发现了系统若干设计缺陷，证明了方法的有效性。

关键词: 形式化建模, 数据库, 定理证明, 安全策略模型

Abstract:

Because of the high-level abstraction,insufficient description of database states and constraints,it was difficult to find the tiny flaws in design and implementation.Based on PVS,a method for formal description and analysis of data-base security policy was proposed,which was more close to the actual database,more widely used in reality,and more complete in describing the safe properties,more extendible of the model,and ensure the efficiency of modeling and veri-fication.Finally,this method is applied in the security policy modeling and analyzing of BeyonDB,which is a commer-cial database,find some security risks in the system design,and thereby verify its effectiveness.

Key words: formal modeling, database, theorem proving, security policy mode

王榕,张敏,冯登国,李昊. 数据库形式化安全策略模型建模及分析方法[J]. 通信学报, 2015, 36(9): 193-203.

Rong WANG,Min ZHANG,Deng-guo FENG,Hao LI. Formal modeling and analyzing method for database security policy[J]. Journal on Communications, 2015, 36(9): 193-203.

图/表 20

图1

表1

图2

图3

图4

图5

图6

图7

图8

图9

图10

图11

图12

图13

图14

图15

图16

图17

表2

表3

参考文献 16

[1]	国家质量监督检验检疫总局. GB17859-1999计算机信息系统安全保护等级划分准则[S]. 第2版.北京：中国标准出版社 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.

描述对象	非形式化描述	抽象描述
操作	INSERT INTO realtable VALUES tuple	操作实体：Operation
操作者	数据库用户	主体：User
操作目标	实关系表	客体：Realtable (隐含指定 Database)
	1.当前数据库在数据库系统中存在	1.数据库存在判断：DatabaseExist
	2.用户在当前数据库系统中存在	2.用户存在判断：UserExist
操作成功判断条件	3.实关系表在当前数据库系统中存在4.主体是客体的属主或者拥有insert客体权限	3.实关系表存在判断：RealtableExist4.客体属主判断：Owner（或者insert权限判断）
	5.用户的安全标签要支配实关系表格的安全标签	5.标签支配判断：dom?
		6.涉及客体：标签Label，权限Permission

类型	错误	系统设计缺陷
策略设计不完整	安全策略的设计考虑不充分，部分内容会与安全属性发生冲突	Procedure 执行过程涉及到多个不同安全等级的客体
实体设计不完整	实体设计过程中考虑不充分，在安全性证明是发生冲突，无法继续证明	无主键表格插入记录
策略执行约束不满足	1.策略执行的前提条件不充分满足，与安全属性发生冲突；2.策略执行过程中，某些操作会与安全属性发生冲突	表级、行级开关会话过程中，主体标签修改

指标	SEPOSTG^[16]	理论模型分析方法^[7]	本文方法
实际系统相符性	中	未讨论	高
安全属性完备性	较差	未讨论	较完备
可扩展性	中	高	高
建模与验证效率	中	低	高