Timing-Sensitive Noninterference through Composition

Sound compositional reasoning principles are the foundation for analyzing the security properties of complex systems. We present a general theory for compositional reasoning about the information-flow security of interactive discrete-timed systems. We develop a simple core-and with it, a language-of combinators, including ones that orchestrate the execution of a collection of interactive systems. We establish conditions under which timing-sensitive noninterference is preserved through composition, for each combinator in our language. To demonstrate the practicality of our theory, we model secure multi-execution (SME) using our combinators. Through this, we show that our theory makes it straightforward 1) to prove, through compositional reasoning, that complex systems are free of external timing channels, and 2) to identify sub-components that cause information leakage of a composite system.