The Community for Technology Leaders
2014 IEEE 27th Computer Security Foundations Symposium (CSF) (2014)
Vienna, Austria
July 19, 2014 to July 22, 2014
ISSN: 1063-6900
ISBN: 978-1-4799-4290-9
pp: 277-292
Willard Rafnsson , Chalmers Univ. of Technol., Gothenburg, Sweden
Andrei Sabelfeld , Chalmers Univ. of Technol., Gothenburg, Sweden
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 condition enforced by practical tools like JSFlow, Paragon, sequential LIO, Jif, Flow Caml, 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. In contrast to PINI, we show what PSNI behaves well under composition, with and without fairness assumptions. Our work is performed within a general framework for nondeterministic interactive systems.
INDEX TERMS
Security, Computational modeling, Semantics, Interactive systems, Cognition, Sensitivity, Synchronization
CITATION

W. Rafnsson and A. Sabelfeld, "Compositional Information-Flow Security for Interactive Systems," 2014 IEEE 27th Computer Security Foundations Symposium (CSF), Vienna, Austria, 2014, pp. 277-292.
doi:10.1109/CSF.2014.27
168 ms
(Ver 3.3 (11022016))