基于Isabelle/SACM的形式化证明与统一保证案例集成

关键系统认证常需保证案例。在保证中使用形式化方法可改善自动化、增强信心并克服错误推理。然而，保证案例永远无法完全形式化，因为形式化方法的使用依赖于由非形式化过程验证的模型。因此，保证技术应支持形式化与非形式化制品，并显式表达它们之间的推理链接。本文贡献了一种称为Isabelle/SACM的形式化机器检查交互式语言，支持构建符合OMG结构化保证案例元模型（Structured Assurance Case Meta-Model）的计算机辅助保证案例。Isabelle/SACM的使用保证了保证案例的良构性、一致性与可追踪性，并允许紧密集成来自不同来源的形化与非形式化证据。特别地，Isabelle带来了可提供证据的多种自动化验证技术。为验证我们的方法，我们基于Tokeneer安全入口系统基准给出了一个实质性案例研究。我们将其功能规约嵌入Isabelle，验证其安全需求，并在Isabelle/SACM中形成结合异构制品的模块化安全案例。我们由此表明Isabelle是关键系统保证的合适平台。