Isabelle 中的可信性工程
软件工程
2021-12-09 v1 密码学与安全
摘要
在本文中，我们介绍了一个在专用 Isabelle 框架中由交互式定理证明支持的形式化系统开发过程。该 Isabelle 基础设施框架在一个由攻击树分析支持的循环过程中实现规范与验证，该过程与规范的形式化精化紧密相连。这个过程是循环的：在重复迭代中，精化为系统规范添加更多细节。如何找到下一个精化步骤是一个已知的难题：这个问题通过使用 Kripke 结构和 CTL 逻辑的基于攻击的分析来解决。我们称这个循环过程为精化-风险循环（RR-cycle）。它最初是为物联网医疗系统的安全与隐私而开发的，但更普遍地也适用于安全，即可靠性。在本文中，我们介绍了对 Isabelle 基础设施框架的扩展，该扩展为 RR-cycle 实现了一种形式化的属性保持精化概念，并与攻击树分析交织进行。该过程在移动新冠病毒警告应用的规范开发和隐私分析上进行了说明。
引用
@article{arxiv.2112.04374,
title = {Dependability Engineering in Isabelle},
author = {Florian Kammüller},
journal= {arXiv preprint arXiv:2112.04374},
year = {2021}
}