Secure Information Flow for Concurrent Programs under Total Store Order

Modern multicore hardware and multithreaded programming languages expose weak memory models to programmers, which relax the intuitive sequential consistency (SC) memory model in order to support a variety of hardware and compiler optimizations. However, to our knowledge all prior work on secure information flow in a concurrent setting has assumed SC semantics. This paper investigates the impact of the Total Store Order (TSO) memory model, which is used by Intel x86 and Sun SPARC processors, on secure information flow, focusing on the natural security condition known as possibilistic noninterference. We show that possibilistic noninterference under SC and TSO are incomparable notions; neither property implies the other one. We define a simple type system for possibilistic noninterference under SC and demonstrate that it is unsound under TSO. We then provide two variants of this type system that are sound under TSO: one that requires only a small change to the original type system but is overly restrictive, and another that incorporates a form of flow sensitivity to safely retain additional expressiveness. Finally, we show that the original type system is in fact sound under TSO for programs that are free of data races.