Validation of a Security Policy by the Test of its Formal B Specification - a Case Study

被引：3

作者：

Ledru, Yves ^{[1
]}

Idani, Akram ^{[1
]}

Richier, Jean-Luc ^{[2
]}

机构：

[1] Univ Grenoble Alpes, LIG, F-38000 Grenoble, France

[2] CNRS, LIG, F-38000 Grenoble, France

来源：

2015 IEEE/ACM 3RD FME WORKSHOP ON FORMAL METHODS IN SOFTWARE ENGINEERING | 2015年

关键词：

D O I：

10.1109/FormaliSE.2015.9

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper discusses the use of test and animation techniques to validate an access control policy, expressed in SecureUML. It reports on a case study of secure medical information system, where the SecureUML model expresses both functional and security models of the information system. It is translated into a specification in the B language. The case study takes advantage of animation tools associated to the B language to validate the functional model, to perform systematic test of permission rules and to investigate potential insiders attacks.

引用

页码：6 / 12

页数：7

共 50 条

[1] Research on formal security policy model specification and its formal analysis
Institute of Software, Chinese Academy of Sciences, Beijing 100080, China
不详
不详
Tongxin Xuebao, 2006, 6 (94-101):
[2] Formal Specification and Validation of Security Policies
Bourdier, Tony
Cirstea, Horatiu
Jaume, Mathieu
Kirchner, Helene
FOUNDATIONS AND PRACTICE OF SECURITY, 2011, 6888 : 148 - +
[3] SPECIFICATION AND VALIDATION OF A SECURITY POLICY MODEL
BOSWELL, A
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1995, 21 (02) : 63 - 68
[4] A study of collaborative work: Answers to a test on formal specification in B
Habrias, H
Poizat, P
Lafaye, JY
FM'99-FORMAL METHODS, VOL II, 1999, 1709 : 1856 - 1857
[5] Formal Specification and Verification of an Extended Security Policy Model for Database Systems
Hong, Zhu
Yi, Zhu
Li Chenyang
Jie, Shi
Ge, Fu
Wang Yuanzhen
APTC 2008: THIRD ASIA-PACIFIC TRUSTED INFRASTRUCTURE TECHNOLOGIES CONFERENCE, PROCEEDINGS, 2008, : 132 - 141
[6] A formal policy specification language for an 802.11 WLAN with enhanced security network
Çalikli, HG
Çaglayan, U
COMPUTER AND INFORMATION SCIENCES - ISCIS 2005, PROCEEDINGS, 2005, 3733 : 183 - 192
[7] Validation of Stepwise Refinement with Test Cases Generated from Formal Specification
Yamada, Shinya
Keijiro, Araki
Kusakabe, Shigeru
Omori, Yoichi
TENCON 2010: 2010 IEEE REGION 10 CONFERENCE, 2010, : 2449 - 2453
[8] Formal Specification and Verification of Modular Security Policy Based on Colored Petri Nets
Huang, Hejiao
Kirchner, Helene
IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING, 2011, 8 (06) : 852 - 865
[9] A case study in formal design specification with CCS
Wang, Q
Cheng, MHM
PROCEEDINGS OF THE 9TH INTERNATIONAL CONFERENCE ON COMPUTER APPLICATIONS IN INDUSTRY AND ENGINEERING, 1996, : 169 - 172
[10] Formal specification of managed objects - a case study
Judge, A.J.
Wezeman, C.
British Telecom technology journal, 1993, 11 (03): : 89 - 97

← 1 2 3 4 5 →