面向软件产品线安全论证的认证分析

安全关键软件系统在许多情况下被设计和实现为产品族,通常称为软件产品线(SPLs)。SPL中的产品因所包含特征的不同而彼此相异。将现有分析技术应用于SPL及其安全论证通常具有挑战性,因为相对于所支持特征的数量,产品数量可能呈指数增长。在本文中,我们提出了一种将现有单产品安全分析认证式地提升(lifting)至产品线的 methodology 与基础设施。为确保我们基础设施的认证安全性,我们在交互式定理证明器中实现它,包括形式化定义、引理、正确性判据定理与证明。我们将该基础设施应用于形式化并提升一个变更影响评估(CIA)算法。我们给出了提升后算法的形式化定义,概述了其正确性证明(完整的机器检查证明可在线获取),并讨论了其在模型管理框架内的实现。