数据库形式化安全策略模型建模及分析方法
Formal modeling and analyzing method for database security policy
- 通信学报 2015年36卷第9期 页码：193-203
- 作者机构：
1. 中国科学院 软件研究所 可信计算与信息保障实验室，北京 100190
2. 中国科学院大学，北京 100190
3. 中国科学院 软件研究所 计算机科学国家重点实验室，北京 100190
- 作者简介：
[ "王榕（1986-），女，辽宁大连人，中国科学院软件研究所博士生，主要研究方向为数据安全、隐私保护。" ]
[ "张敏（1975-），女，安徽萧县人，中国科学院软件研究所副研究员，主要研究方向为数据库安全与隐私保护。" ]
[ "冯登国（1965-），男，陕西靖边人，中国科学院软件研究所研究员，主要研究方向为密码学与信息安全。" ]
[ "李昊（1983-），男，河南固始人，中国科学院软件研究所副研究员，主要研究方向为网络与系统安全。" ]
- 基金信息：国家自然科学基金资助项目(61232005);国家自然科学基金资助项目(61402456)
DOI：10.11959/j.issn.1000-436x.2015151
中图分类号： TP309-
网络首发：2015-09，
纸质出版：2015-09-25
- 稿件说明：
移动端阅览
王榕, 张敏, 冯登国, 等. 数据库形式化安全策略模型建模及分析方法[J]. 通信学报, 2015,36(9):193-203.
Rong WANG, Min ZHANG, Deng-guo FENG, et al. Formal modeling and analyzing method for database security policy[J]. Journal on Communications, 2015, 36(9): 193-203.
王榕, 张敏, 冯登国, 等. 数据库形式化安全策略模型建模及分析方法[J]. 通信学报, 2015,36(9):193-203. DOI： 10.11959/j.issn.1000-436x.2015151.
Rong WANG, Min ZHANG, Deng-guo FENG, et al. Formal modeling and analyzing method for database security policy[J]. Journal on Communications, 2015, 36(9): 193-203. DOI： 10.11959/j.issn.1000-436x.2015151.
摘要
目前数据库形式化安全策略模型存在抽象层次较高、缺乏对数据库状态与约束的充分描述等问题，难以辅助用户发现商用数据库设计中的微小缺陷。提出了一种基于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.
关键词
Keywords
references
国家质量监督检验检疫总局 . 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 .
张敏 ， 冯登国 ， 陈驰 . 基于安全策略模型的安全功能测试用例生成方法 [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 .
官尚元 ， 伍卫国 ， 董小社 . 自动信任协商的形式化描述与验证研究 [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 .
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 .
肖芳雄 ， 黄志球 ， 曹子宁 . 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 .
陈小峰 . 可信平台模块的形式化分析和测试 [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 .
何建波 ， 卿斯汉 ， 王超 . 对一类多级安全模型安全性的形式化分析 [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 .
钱振江 ， 黄皓 ， 宋方敏 . 操作系统形式化设计与安全需求的一致性验证研究 [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 .
杨涛 ， 王永刚 ， 唐礼勇 . 一种实用动态完整性保护模型的形式化分析 [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 .
BELL D E , LA PADULA L J . Secure computer system:Unified exposition and multics interpretation [R ] . MITRE CORP BEDFORD MA , 1976 .
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 .
张敏 ， 徐震 ， 冯登国 . 数据库安全 [M ] . 北京 ： 科学出版社 ， 2005 .
ZHANG M , XU Z , FENG D G . Database Security [M ] . Beijing : Science Press ， 2005 .
李丽萍 ， 卿斯汉 ， 周洲仪 . 安全策略模型规范及其形式分析技术研究 [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 .
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 .
SANDHU R S , COYNE E J , FEINSTEIN H L , et al . Role-based access control models [J ] . Computer , 1996 , 29 ( 2 ): 38 - 47 .
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 .
0
浏览量
1423
下载量
0
CSCD
- 网络PDF下载
- XML下载
- Meta-XML下载
- BibTeX下载
- Endnote下载
- RefMan 下载
- NoteExpress下载
- NoteFirst下载
关联资源
相关文章
相关作者
相关机构
AI问答- 技术支持由北京北大方正电子有限公司提供 京ICP备09064830号-19
京公网安备11010802024621 - 本系统建议在Chrome、 IE9+ 以上版本浏览器阅读本站内容，360浏览器请切换至极速模式
- Cookies帮助我们提供服务并提供个性化体验。使用本网站，即表示您同意我们使用Cookies
- 总访问量：582255 今日访问量：71