Thread algebra for noninterference

Sectie Software Engineering, University of Amsterdam, Kruislaan 403, 1098 SJ Amsterdam, The Netherlands; tdvu@science.uva.nl

Received: 8 May 2007
Accepted: 11 September 2008

Abstract

Thread algebra is a semantics for recent object-oriented programming languages [J.A. Bergstra and M.E. Loots, J. Logic Algebr. Program. 51 (2002) 125–156; J.A. Bergstra and C.A. Middelburg, Formal Aspects Comput. (2007)] such as C# and Java. This paper shows that thread algebra provides a process-algebraic framework for reasoning about and classifying various standard notions of noninterference, an important property in secure information flow. We will take the noninterference property given by Volpano et al. [D. Volpano, G. Smith and C. Irvine, J. Comput. Secur. 4 (1996) 167–187] on type systems as an example of our approach. We define a comparable notion of noninterference in the setting of thread algebra. Our approach gives a similar result to the approach of [G. Smith and D. Volpano, in POPL'98 29 (1998) 355–364] and can be applied to unstructured and multithreaded programming languages.