The impact of synchronisation on secure information flow in concurrent programs

Abstract

Synchronisation is fundamental to concurrent programs. This paper investigates the security of information flow in multi-threaded programs in the presence of synchronisation. We give a small-step operational semantics for a simple shared-memory multi-threaded language with synchronisation, and present a compositional timing-sensitive bisimulation- based confidentiality specification. We propose a type-based analysis improving on previous approaches to reject potentially insecure programs. © Springer-Verlag Berlin Heidelberg 2001.