将 Isabelle 内部者框架应用于飞机安全
软件工程
2020-03-27 v1 计算机科学中的逻辑
摘要
航空电子是验证方法被开创并为其安全关键环境中的系统带来全新可靠性水平的领域之一。诸如 2015 年德国飞机内部者攻击（机上 150 人全部遇难）之类的悲剧表明，安全性与安保性关键不仅取决于系统的良好运行，还取决于人类与系统交互的方式。策略描述了人类在与技术系统交互时应如何行为，对此类策略的形式化推理需要将人为因素整合进验证过程。在本文中，我们报告了利用带参与者的基础设施模型与策略的逻辑建模和分析，在存在内部者的情况下审视安全策略的工作。我们在 Isabelle 内部者框架中对飞机上的内部者攻击进行建模。该应用促使我们对该框架进行扩展，引入 Kripke 结构与时序逻辑 CTL，以实现对动态系统状态的推理。此外，我们说明 Isabelle 建模与不变量推理能揭示微妙的安全假设。最后，我们总结并提出一种用于开发满足既定性质之策略的方法论。
引用
@article{arxiv.2003.11838,
title = {Applying the Isabelle Insider Framework to Airplane Security},
author = {Florian Kammüller and Manfred Kerber},
journal= {arXiv preprint arXiv:2003.11838},
year = {2020}
}