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
    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
    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
    Bouquet, F
    Legeard, B
    FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 778 - 795
  • [24] Specifying a security policy: A case study
    Cuppens, F
    Saurel, C
    9TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 1996, : 123 - 134
  • [25] Combining graphical representations and formal notations in software specification: A case study
    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
  • [26] Controlling test case explosion in test generation from B formal models
    Legeard, B
    Peureux, F
    Utting, M
    SOFTWARE TESTING VERIFICATION & RELIABILITY, 2004, 14 (02): : 81 - 103
  • [27] Integrated security verification and validation: Case study
    Ghindici, Dorina
    Grimaud, Gilles
    Simplot-Ryl, Isabelle
    Liu, Yanguo
    Traore, Issa
    31ST IEEE CONFERENCE ON LOCAL COMPUTER NETWORKS, PROCEEDINGS, 2006, : 1000 - +
  • [28] Formal Specification for Compiler Based Test Case Generation of Embedded Real-Time System
    Chen, Yong
    He, Yanxiang
    Xu, Chao
    Wu, Wei
    Liu, Jianbo
    BUSINESS, ECONOMICS, FINANCIAL SCIENCES, AND MANAGEMENT, 2012, 143 : 643 - 650
  • [29] Specification of an automatic manufacturing system: A case study in using integrated formal methods
    Wehrheim, H
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, 2000, 1783 : 334 - 348
  • [30] FORMAL SPECIFICATION METHODS AND NUMERICAL SOFTWARE - A CASE-STUDY USING Z
    LUCENA, CJP
    QIAN, YM
    UTILITAS MATHEMATICA, 1993, 44 : 85 - 114
12345