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 条

[21] National information security policy and its implementation: A case study in Taiwan [J].

Ku, Cheng-Yuan ;

Chang, Yi-Wen ;

Yen, David C. .

TELECOMMUNICATIONS POLICY, 2009, 33 (07) :371-384

[22] Checking the Conformance of a Promela Design to its Formal Specification in Event-B [J].

Vu, Dieu-Huong ;

Chiba, Yuki ;

Yatake, Kenro ;

Aoki, Toshiaki .

FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, FTSCS 2014, 2015, 476 :110-126

[23] Reification of executable test scripts in formal specification-based test generation: The Java']Java Card Transaction Mechanism case study [J].

Bouquet, F ;

Legeard, B .

FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 :778-795

[24] Specifying a security policy: A case study [J].

Cuppens, F ;

Saurel, C .

9TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 1996, :123-134

[25] A Case Study in Formal Specification and Runtime Verification of a CubeSat Communications System [J].

Luppen, Zachary Allen ;

Lee, Dae Young ;

Rozier, Kristin Yvonne .

AIAA SCITECH 2021 FORUM, 2021,

[26] Combining graphical representations and formal notations in software specification: A case study [J].

Dascalu, S ;

Hitchcock, P ;

Vert, G .

SERP'03: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING RESEARCH AND PRACTICE, VOLS 1 AND 2, 2003, :483-489

[27] Controlling test case explosion in test generation from B formal models [J].

Legeard, B ;

Peureux, F ;

Utting, M .

SOFTWARE TESTING VERIFICATION & RELIABILITY, 2004, 14 (02) :81-103

[28] Formal Specification for Compiler Based Test Case Generation of Embedded Real-Time System [J].

Chen, Yong ;

He, Yanxiang ;

Xu, Chao ;

Wu, Wei ;

Liu, Jianbo .

BUSINESS, ECONOMICS, FINANCIAL SCIENCES, AND MANAGEMENT, 2012, 143 :643-650

[29] Integrated security verification and validation: Case study [J].

Ghindici, Dorina ;

Grimaud, Gilles ;

Simplot-Ryl, Isabelle ;

Liu, Yanguo ;

Traore, Issa .

31ST IEEE CONFERENCE ON LOCAL COMPUTER NETWORKS, PROCEEDINGS, 2006, :1000-+

[30] Specification of an automatic manufacturing system: A case study in using integrated formal methods [J].

Wehrheim, H .

FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, 2000, 1783 :334-348

← 1 2 3 4 5 →