Generalized Security-Preserving Refinement for Concurrent Systems
Huan Sun, David Sanán, Jingyi Wang, Yongwang Zhao, Jun Sun, Wenhai Wang
TL;DR
The paper tackles proving information-flow security (IFS) for concurrent systems under general, intransitive policies, a challenge for large codebases like multicore OS kernels. It introduces an unwinding-preserving simulation with a state invariant $ obreak\alpha$ and a step mapping $ obreak\zeta$ to relate an implementation to an abstract specification, ensuring that every paired step respects the security policy or remains silent. The approach is compositional via rely-guarantee reasoning and is fully formalized in Isabelle/HOL, demonstrated on two nontrivial case studies: ARINC 653 multicore IPC and a sealed-bid auction with declassification, revealing and fixing covert channels. The results show that security-preserving refinement can be applied with only modest additional proof burden compared to standard refinement, offering a practical path to scalable, secure refinement proofs for real-world concurrent systems. The work advances the state of the art by handling general (intransitive) policies, enabling controlled declassification, and preserving unwinding conditions in a compositional, executable framework with concrete multicore security applications.
Abstract
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.