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 条

[31] FORMAL SPECIFICATION METHODS AND NUMERICAL SOFTWARE - A CASE-STUDY USING Z [J].

LUCENA, CJP ;

QIAN, YM .

UTILITAS MATHEMATICA, 1993, 44 :85-114

[32] Formal methods for verification and validation of partial specifications: A case study [J].

Easterbrook, S ;

Callahan, J .

JOURNAL OF SYSTEMS AND SOFTWARE, 1998, 40 (03) :199-210

[33] Early validation of requirements - A case study using formal methods [J].

Miller, SP ;

Heimdahl, MPE .

BUILDING THE INFORMATION SOCIETY, 2004, 156 :521-526

[34] Validation of Railway Interlocking Systems by Formal Verification, A Case Study [J].

Bonacchi, Andrea ;

Fantechi, Alessandro ;

Bacherini, Stefano ;

Tempestini, Matteo ;

Cipriani, Leonardo .

SOFTWARE ENGINEERING AND FORMAL METHODS, 2014, 8368 :237-252

[35] Policy validation for system automation: A case study [J].

Zarpas, Emmanuel ;

Eisner, Cindy ;

Tal, Sivan .

2008 IEEE WORKSHOP ON POLICIES FOR DISTRIBUTED SYSTEMS AND NETWORKS, PROCEEDINGS, 2008, :46-53

[36] Test case, the Balkans - European security and defence policy and transatlantic relations [J].

Ehrhart, HG .

INTERNATIONALE POLITIK, 2002, 57 (05) :15-20

[37] Case study on combined validation of safety & security requirements [J].

Sojka, Michal ;

Krec, Michal ;

Hanzalek, Zdenek .

2014 9TH IEEE INTERNATIONAL SYMPOSIUM ON INDUSTRIAL EMBEDDED SYSTEMS (SIES), 2014,

[38] CASE-STUDY - THE USE OF FORMAL SPECIFICATION AND RAPID PROTOTYPING TO ESTABLISH PRODUCT FEASIBILITY [J].

ALEXANDER, H ;

POTTER, B .

INFORMATION AND SOFTWARE TECHNOLOGY, 1987, 29 (07) :388-394

[39] Generation of functional test sequences from B formal specifications - Presentation and industrial case-study [J].

Legeard, B ;

Peureux, F .

16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, :377-381

[40] Formal specification of MPI 2.0: Case study in specifying a practical concurrent programming API [J].

Li, Guodong ;

Palmer, Robert ;

DeLisi, Michael ;

Gopalakrishnan, Ganesh ;

Kirby, Robert M. .

SCIENCE OF COMPUTER PROGRAMMING, 2011, 76 (02) :65-81

← 1 2 3 4 5 →