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

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

Abstract

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

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.

Figures/Tables 20

References 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.

Metrics

Recommended 0

No Suggested Reading articles found!

描述对象	非形式化描述	抽象描述
操作	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]	本文方法
实际系统相符性	中	未讨论	高
安全属性完备性	较差	未讨论	较完备
可扩展性	中	高	高
建模与验证效率	中	低	高

Formal modeling and analyzing method for database security policy

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 20

References 16

Related Articles 15

Metrics

Recommended 0

[1]	Dong CUI, Qiaoyan WEN, Hua ZHANG, Huawei WANG. QML: a hybrid spatial index structure [J]. Journal on Communications, 2021, 42(12): 1-16.
[2]	Yonggui FU,Jianming ZHU. Design for database access control mechanism based on blockchain [J]. Journal on Communications, 2020, 41(5): 130-140.
[3]	Zhaogen ZHONG,Zhaojun WU,Limin ZHANG,Zhiqing WANG. Blind recognition of RSC based on logarithmic conformity [J]. Journal on Communications, 2018, 39(10): 79-86.
[4]	Jia-jie XU,Kai ZHENG,Ming-min CHI,Yang-yong ZHU,Xiao-hui YU,Xiao-fang ZHOU. Trajectory big data:data,applications and techniques [J]. Journal on Communications, 2015, 36(12): 97-105.
[5]	Tao WEN,Yu-qing ZHANG,Qi-xu LIU,Gang YANG. UVDA:design and implementation of automation fusion framework of heterogeneous security vulnerability database [J]. Journal on Communications, 2015, 36(10): 235-244.
[6]	. Research on the optimization adjustment strategy for the SaaS multi-tenant data placement [J]. Journal on Communications, 2014, 35(Z2): 10-71.
[7]	Xiao-na LI,Qing-zhong LI,Lan-ju KONG,Zhong-min YAN. Research on the optimization adjustment strategy for the SaaS multi-tenant data placement [J]. Journal on Communications, 2014, 35(Z2): 63-71.
[8]	. GUC-secure protocol for private relational join operator computing [J]. Journal on Communications, 2014, 35(11): 12-106.
[9]	Yuan TIAN,Rong-xin SUN,Wu-yang CAI. GUC-secure protocol for private relational join operator computing [J]. Journal on Communications, 2014, 35(11): 107-116.
[10]	Xiao-na LI,Qing-zhong LI,Lan-ju KONG,Cheng PANG. Research on multi-tenant data partition mechanism for SaaS application based on shared schema [J]. Journal on Communications, 2012, 33(Z1): 110-120.
[11]	Jiao LI,Quan LIU,Qi-ming FU,Ting-gang WANG. Record matching method based on local CON model in distributed database [J]. Journal on Communications, 2011, 32(7): 196-202.
[12]	Yu-qing ZHANG,Shu-ping WU,Qi-xu LIU,Fang-fang LIANG. Design and implementation of national security vulnerability database [J]. Journal on Communications, 2011, 32(6): 93-100.
[13]	Ting LUO,Yuan-bo GUO,Yao-hui HAO,Hu LI. Method verifying the correctness of code refactoring program [J]. Journal on Communications, 2011, 32(11A): 152-157.
[14]	Hua DAI,Xiao-lin QIN,Liang LIU,Chuan-jie BAI. Database anomaly detection model based on mining object-condition association rules [J]. Journal on Communications, 2009, 30(9): 7-14.
[15]	Hai-tao ZENG,Yong-ji WANG,Li RUAN,Wei ZU,Jia-yong CAI. Covert channel mitigation method for secure real-time database using capacity metric [J]. Journal on Communications, 2008, 29(8): 47-57.