Non-interference Preserving Optimising Compilation

To protect security-critical applications, secure compilers have to preserve security policies, such as noninterference, during compilation. The preservation of security policies goes beyond the classical notion of compiler correctness which only enforces the preservation of the semantics of the source program. Therefore, several standard compiler optimisations are prone to break standard security policies like non-interference. Existing approaches to secure compilation are very restrictive with respect to the compiler optimisations that they permit or to the security policies they support because of conceptual limitations in their formal setup.

In this paper, we present hyperproperty simulations, a novel framework to secure compilation that models the preservation of arbitrary 𝑘-hyperproperties during compilation and overcomes several limitations of existing approaches, in particular it is more expressive and more flexible. We demonstrate this by designing and proving a generic non-interference preserving code transformation that can be applied on different optimisations and leakage models. This approach reduces the proof burden per optimisation to a minimum. We instantiate this code transformation on different leakage models with various standard compiler optimisations that could be handled in a very limited and less modular way (if at all) by existing approaches. Our results are formally verified in the Rocq theorem prover.

CCS Concepts: • Security and privacy → Formal methods and theory of security; • Software and its engineering → Compilers; • Theory of computation → Logic and verification.