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

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

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

您当前的位置：

首页 >

文章列表页 >

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

学术论文 | 更新时间：2024-06-05

- 数据库形式化安全策略模型建模及分析方法
- 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 .

浏览量

984

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

QML：一种混合空间索引结构

基于区块链的数据库访问控制机制设计