Non-interference through determinism^*

Article type: Research Article

Authors: Roscoe, A.W. | Woodcock, J.C.P. | Wulf, L.

Affiliations: Oxford University Computing Laboratory, Parks Road, Wolfson Building, Oxford OX1 3QD, UK

Note: [*] This paper is a revised version of [16]. The notation has been slightly modified to make it compatible with that used in related publications [13, 14].

Abstract: The standard approach to the specification of a secure system is to present a (usually state-based) abstract security model separately from the specification of the system's functional requirements, and establishing a correspondence between the two specifications. This complex treatment has resulted in development methods distinct from those usually advocated for general applications. We provide a novel and intellectually satisfying formulation of security properties in a process algebraic framework, and show that these are preserved under refinement. We relate the results to a more familiar state-based (Z) specification methodology. There are efficient algorithms for verifying our security properties using model checking.

Keywords: Security, non-interference, formal methods, process algebra, determinism, automatic verification

DOI: 10.3233/JCS-1996-4103

Journal: Journal of Computer Security, vol. 4, no. 1, pp. 27-53, 1996