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 expressiveness needed to capture complex security policies for concurrent systems. In this work, we present a generalized security-preserving refinement technique, particularly for verifying the IFS of concurrent systems governed by potentially complex security policies. We formalize the IFS properties for concurrent systems and present a refinement-based compositional approach to prove that the generalized security properties (e.g., intransitive noninterference) are preserved between implementation and abstraction. The key intuition enabling such reasoning, compared to previous refinement work, is to establish a step-mapping relation between the implementation and the abstraction, which is sufficient to ensure that every paired step (in the abstraction and the implementation, respectively) is either permitted or prohibited by the security policy. We apply our approach to verify two non-trivial case studies against a collection of security policies. Our proofs are fully mechanized in Isabelle/HOL, during which we identified that two covert channels previously reported in the ARINC 653 single-core standard also exist in the ARINC 653 multicore standard. We subsequently proved the correctness of the revised mechanism, showcasing the effectiveness of our approach.

翻译：确保符合信息流安全（IFS）要求一直被认为具有挑战性，特别是对于代码库庞大的并发系统（如多核操作系统内核）。精化方法通过验证实现是否保持了更抽象规约的特定性质，为解决此类挑战提供了可行途径。然而，在基于精化的安全性质验证方面，现有技术仍局限于顺序系统，或缺乏表达并发系统复杂安全策略的能力。本研究提出一种广义的安全保持精化技术，专门用于验证受潜在复杂安全策略约束的并发系统的IFS性质。我们形式化了并发系统的IFS性质，并提出一种基于精化的组合式验证方法，以证明广义安全性质（如非传递无干扰性）在实现与抽象规约之间得以保持。相较于先前的精化研究，实现该推理的关键思路是在实现与抽象之间建立步骤映射关系，该关系足以确保每对步骤（分别位于抽象规约与实现中）均被安全策略允许或禁止。我们将该方法应用于两个非平凡案例研究，针对一组安全策略进行验证。所有证明均在Isabelle/HOL中实现完全机械化验证，期间我们发现ARINC 653单核标准中先前报告的两个隐蔽信道同样存在于ARINC 653多核标准中。随后我们证明了修正机制的正确性，从而展示了本方法的有效性。