论文标题
将Isabelle Insider框架应用于飞机安全
Applying the Isabelle Insider Framework to Airplane Security
论文作者
论文摘要
航空电子学是验证方法已开创并为安全关键环境中使用的系统带来新的可靠性的领域之一。悲剧，例如2015年内幕人士对德国飞机的攻击，其中所有150人都死了，这表明安全和保障不仅取决于系统的运作良好，而且还取决于人类与系统互动的方式。政策是描述人类在与技术系统中的互动中应如何行事的一种方式，有关此类政策的正式推理需要将人类因素整合到验证过程中。在本文中，我们报告了有关使用逻辑建模和分析基础架构模型和政策分析的工作，并与参与者在存在内部人员的情况下审查安全策略。我们对Isabelle Insider框架中的飞机进行内幕攻击进行建模。该应用程序激发了使用Kripke结构和时间逻辑CTL的框架扩展，以实现动态系统状态的推理。此外，我们说明了Isabelle建模和不变推理揭示了微妙的安全性假设。我们通过提供一种满足陈述特性的政策的制定方法来总结。
Avionics is one of the fields in which verification methods have been pioneered and brought 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 how 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. 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. We summarize by providing a methodology for the development of policies that satisfy stated properties.
