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 条

[41] FORMAL SPECIFICATION AND VERIFICATION OF MULTI-AGENT ROBOTICS SOFTWARE SYSTEMS A Case Study [J].

Akhtar, Nadeem ;

Le Guyadec, Yann ;

Oquendo, Flavio .

ICAART 2009: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON AGENTS AND ARTIFICIAL INTELLIGENCE, 2009, :475-+

[42] SELECTION TEST VALIDATION - A CASE-STUDY [J].

HORNE, W ;

WARNE, S .

AUSTRALIAN PSYCHOLOGIST, 1988, 23 (01) :75-76

[43] Developing an Information Security Policy: A Case Study Approach [J].

Alqahtani, Fayez Hussain .

4TH INFORMATION SYSTEMS INTERNATIONAL CONFERENCE (ISICO 2017), 2017, 124 :691-697

[44] Integrated and Iterative Requirements Analysis and Test Specification: A Case Study at Kostal [J].

Wiecher, Carsten ;

Fischbach, Jannik ;

Greenyer, Joel ;

Vogelsang, Andreas ;

Wolff, Carsten ;

Dumitrescu, Roman .

24TH INTERNATIONAL CONFERENCE ON MODEL-DRIVEN ENGINEERING LANGUAGES AND SYSTEMS (MODELS 2021), 2021, :112-122

[45] Formal verification and validation with DEVS-Suite: OSPF Case study [J].

Zengin, Ahmet ;

Ozturk, Muhammed Maruf .

SIMULATION MODELLING PRACTICE AND THEORY, 2012, 29 :193-206

[46] Security test MOODLE: a penetration testing case study [J].

Mudiyanselage A.K. ;

Pan L. .

International Journal of Computers and Applications, 2020, 42 (04) :372-382

[47] Formal Specification and Risk Assessment Approach of Integrated Complex System: A Case Study in IMA Domain [J].

Ren, Fuchun ;

Zhao, Tingdi ;

Wang, Hongli .

PROCEEDINGS OF THE 2015 FIRST INTERNATIONAL CONFERENCE ON RELIABILITY SYSTEMS ENGINEERING 2015 ICRSE, 2015,

[48] Task level specification and formal verification of robotics control systems: state of the art and case study [J].

Kapellos, K ;

Simon, D ;

Jourdant, M ;

Espiau, B .

INTERNATIONAL JOURNAL OF SYSTEMS SCIENCE, 1999, 30 (11) :1227-1245

[49] Formal specification of SNMP MIB's using action semantics: The routing proxy case study [J].

Duarte, EP ;

Musicante, MA .

INTEGRATED NETWORK MANAGEMENT VI: DISTRIBUTED MANAGEMENT FOR THE NETWORKED MILLENNIUM, 1999, :417-430

[50] Teaching Formal Methods in Application Domains A Case Study in Computer and Network Security [J].

Brucker, Achim D. ;

Marmsoler, Diego .

FORMAL METHODS TEACHING, FMTEA 2024, 2024, 14939 :124-140

← 1 2 3 4 5 →