Applying the Isabelle insider framework to airplane security
Article
Kammueller, F. and Kerber, M. 2021. Applying the Isabelle insider framework to airplane security. Science of Computer Programming. 206. https://doi.org/10.1016/J.SCICO.2021.102623
Type | Article |
---|---|
Title | Applying the Isabelle insider framework to airplane security |
Authors | Kammueller, F. and Kerber, M. |
Abstract | Avionics is one of the fields in which verification methods have been pioneered and brought about a new level of reliability to systems used in safety-critical environments. Tragedies, like the 2015 insider attack on a German airplane, in which all 150 people on board died, show that safety and security crucially depend not only on the well-functioning of systems but also on the way humans interact with the systems. Policies are a way to describe how humans should behave in their interactions with technical systems. Formal reasoning about such policies requires integrating the human factor into the verification process. In this paper, we report on our work on using logical modelling and analysis of infrastructure models and policies with actors to scrutinize security policies in the presence of insiders. An insider is a user of a system who behaves like an attacker abusing privileges thereby bypassing security controls. We model insider attacks on airplanes in the Isabelle Insider framework. This application motivates the use of an extension of the framework with Kripke structures and the temporal logic CTL to enable reasoning on dynamic system states. Furthermore, we illustrate that Isabelle modelling and invariant reasoning reveal subtle security assumptions. This results in a methodology for the development of policies that satisfy stated properties. To contrast our approach to model checking, we provide an additional comparative analysis. |
Publisher | Elsevier |
Journal | Science of Computer Programming |
ISSN | 0167-6423 |
Publication dates | |
Online | 23 Feb 2021 |
01 Jun 2021 | |
Publication process dates | |
Deposited | 22 Feb 2021 |
Accepted | 08 Feb 2021 |
Output status | Published |
Accepted author manuscript | License |
Copyright Statement | © 2021. This manuscript version is made available under the CC-BY-NC-ND 4.0 license http://creativecommons.org/licenses/by-nc-nd/4.0/ |
Digital Object Identifier (DOI) | https://doi.org/10.1016/J.SCICO.2021.102623 |
Language | English |
https://repository.mdx.ac.uk/item/89458
Download files
70
total views24
total downloads0
views this month0
downloads this month