Compositional Information-flow Security for Interactive Systems

ABSTRACT. To achieve end-to-end security in a system built from parts, it is important to ensure that the composition of secure components is itself secure. This work investigates the compositionality of two popular conditions of possibilistic noninterference. The first condition, progress-insensitive noninterference (PINI), is the security property enforced by practical tools like JSFlow, Paragon, LIO, Jif, FlowCaml, and SPARK Examiner. We show that this condition is not preserved under fair parallel composition: composing a PINI system fairly with another PINI system can yield an insecure system. We explore constraints that allow recovering compositionality for PINI. Further, we develop a theory of compositional reasoning and enforcement for progress-sensitive noninterference (PSNI). Our work is performed within a general framework for nondeterministic interactive systems.