Formal modeling and analyzing method for database security policy

Rong WANG; Min ZHANG; Deng-guo FENG; Hao LI

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

您当前的位置：

首页 >

文章列表页 >

Formal modeling and analyzing method for database security policy

academic paper | 更新时间：2024-06-05

- Formal modeling and analyzing method for database security policy
- Journal on Communications Vol. 36, Issue 9, Pages: 193-203(2015)
- 作者机构：
  
  1. 中国科学院软件研究所可信计算与信息保障实验室，北京 100190
  2. 中国科学院大学，北京 100190
  3. 中国科学院软件研究所计算机科学国家重点实验室，北京 100190
- 作者简介：
- 基金信息：
  
  The National Natural Science Foundation of China(61232005);The National Natural Science Foundation of China(61402456)
- DOI：10.11959/j.issn.1000-436x.2015151
  CLC： TP309
- Online First：2015-09，
  
  Published：25 September 2015
- 稿件说明：
移动端阅览
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：

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 .

Views

1522

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

QML: a hybrid spatial index structure

Design for database access control mechanism based on blockchain

Related Author

Dong CUI

Qiaoyan WEN

Hua ZHANG

Huawei WANG

Yonggui FU

Jianming ZHU

Related Institution

The State Key Laboratory of Networking and Switching Technology， Beijing University of Posts and Telecommunications

School of Information,Shanxi University of Finance and Economics

School of Information, Central University of Finance and Economics

AI问答

⁰