Secure Information Flow for Concurrent Programs with Expressive Synchronization

Practical enforcement of secure information flow in concurrent programs remains notoriously difficult. An underexplored reason is that concurrent programs rely on a wide variety of synchronization primitives, which can leak information. However, the existing literature on security for concurrent programs has focused on a small set of such primitives. This paper studies how channel-like synchronization primitives can leak information and describes enforcement mechanisms to prevent such leaks. Out of this study, we provide two technical contributions. First, we introduce a simple, novel analysis that bans memory races and channel contention that otherwise lead to timing channels. This analysis repurposes security labels for information flow control to be used also as capabilities for accessing resources. Compared with the fractional capabilities technique used by prior work, our analysis supports a significantly simpler inference procedure at a small expense in expressivity. Second, we generalize the security definition of observational determinism as first proposed by Zdancewic and Myers [24] to allow for a limited amount of observable nondeterminism while ensuring this cannot leak information. This security condition is designed for a synchronization primitive whose behavior is inherently nondeterministic. We integrate these technical contributions into a type system and soundness result for a concurrent language with dynamically created threads.