Modeling and Re-Evaluating Security in an Incremental Development of RBAC-Based Systems Using B Method

View Sample PDF

Author(s): Nasser Al-Mur Al-Hadhrami (Ministry of Education, Oman)
Copyright: 2019
Pages: 32
Source title: Exploring Security in Software Architecture and Design
Source Author(s)/Editor(s): Michael Felderer (University of Innsbruck, Austria)and Riccardo Scandariato (Chalmers University of Technology, Sweden & University of Gothenburg, Sweden)
DOI: 10.4018/978-1-5225-6313-6.ch005

Keywords: Computer Science & IT / Information Science Reference / IT Security and Ethics / Systems & Software Design

Purchase

View Modeling and Re-Evaluating Security in an Incremental Development of RBAC-Based Systems Using B Method on the publisher's website for pricing and purchasing information.

Abstract

Incremental software development through the addition of new features and access rules potentially creates security flaws due to inconsistent access control models. Discovering such flaws in software architectures is commonly performed with formal techniques that allow the verification of the correctness of a system and its compliance with applicable policies. In this chapter, the authors propose the use of the B method to formally, and incrementally, design and evaluate the security of systems running under role-based access control (RBAC) policies. They use an electronic marking system (EMS) as a case study to demonstrate the iterative development of RBAC models and the role of the B language in exploring and re-evaluating the security of the system as well as addressing inconsistencies caused by incremental software development. Two formal approaches of model checking and proof obligations are used to verify the correctness of the RBAC specification.

The IRMA Community

Research IRM

Modeling and Re-Evaluating Security in an Incremental Development of RBAC-Based Systems Using B Method

Purchase

Abstract

Related Content

IRMA Sponsors