Document RAIRO-Theor. Inf. Appl. (2008)
DOI: 10.1051/ita:2008026
Thread algebra for noninterference
Thuy Duong VuSectie Software Engineering, University of Amsterdam, Kruislaan 403, 1098 SJ Amsterdam, The Netherlands; tdvu@science.uva.nl
Received May 8, 2007. Accepted September 11, 2008. Published online 2 October 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.
Mathematics Subject Classification. 68Q60
Key words: Noninterference -- thread algebra -- formal methods -- security verification
© EDP Sciences 2008