Generalized Security-Preserving Refinement for Concurrent Systems
Huan Sun and David Sanán and Jingyi Wang and Yongwang Zhao and Jun Sun and Wenhai Wang
众所周知,确保遵守信息流安全(IFS)具有挑战性,特别是对于具有大型代码库(如多核操作系统(OS)内核)的并发系统。 精炼,它验证了一个实现保留了一个更抽象的规范的某些属性,对于应对这些挑战很有希望。 然而,就基于改进的安全属性验证而言,现有技术仍然仅限于顺序系统,或者缺乏捕获并发系统复杂安全策略所需的表现力。 在这项工作中,我们展示了一种通用的安全保护改进技术,特别是用于验证受潜在复杂安全策略支配的并发系统的IFS。 我们正式化了并发系统的 IFS 属性,并提出了基于精细化的组合方法,以证明广义的安全属性(例如,非瞬态互不干涉)在实现和抽象之间保留。 与以前的细化工作相比,实现这种推理的关键直觉是建立实现和抽象之间的逐步映射关系,这足以确保安全策略允许或禁止每个配对的步骤(分别在抽象和实现中)。 我们采用我们的方法,根据一系列安全政策验证两个非平凡的案例研究。 我们的证明在Isabelle/HOL中完全机械化,在此期间,我们发现ARINC 653单核标准先前报告的两个秘密通道也存在于ARINC 653多核标准中。 我们随后证明了修订机制的正确性,展示了我们方法的有效性。
Ensuring compliance with Information Flow Security (IFS) is known to be challenging, especially for concurrent systems with large codebases such as multicore operating system (OS) kernels. Refinement, which verifies that an implementation preserves certain properties of a more abstract specification, is promising for tackling such challenges. However, in terms of refinement-based verification of security properties, existing techniques are still restricted to sequential systems or lack the expre...