Reasoning about information flow in a concurrent setting is notoriously difficult due in part to timing channels that may leak sensitive information. In this paper, we present a compositional and flexible type-and-effect system that guarantees non-interference by disallowing potentially insecure races that can be exploited through internal timing attacks. In contrast to many previous approaches, which disallow all races on public variables, we use an explicit scheduler model to give a more permissive security definition and type system, which allows benign races on public variables. To achieve compositionality, we use the idea of resources from separation logic, both to locally specify and reason about whether accesses may be racy and to bound the security level of data that may be learned through scheduling.
CITATION STYLE
Karbyshev, A., Svendsen, K., Askarov, A., & Birkedal, L. (2018). Compositional non-interference for concurrent programs via separation and framing. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10804 LNCS, pp. 53–78). Springer Verlag. https://doi.org/10.1007/978-3-319-89722-6_3
Mendeley helps you to discover research relevant for your work.