What, indeed, is intransitive noninterference?1

Article type: Research Article

Authors: van der Meyden, Ron^*;

Affiliations: School of Computer Science and Engineering, UNSW Australia, Sydney, NSW, Australia. E-mail: [email protected]

Correspondence: [*] Address for correspondence: School of Computer Science and Engineering, UNSW Australia, Sydney, NSW 2052, Australia. E-mail: [email protected].

Abstract: This paper argues that Haigh and Young’s definition of noninterference for intransitive security policies admits information flows that are not in accordance with the intuitions it seeks to formalize. Several alternative definitions are discussed, which are shown to be equivalent to the classical definition of noninterference with respect to transitive policies. Rushby’s unwinding conditions for intransitive noninterference are shown to be sound and complete for one of these definitions, TA-security. Access control systems compatible with a policy are shown to be TA-secure, and it is also shown that TA-security implies that the system can be interpreted as an access control system.

Keywords: Information flow, noninterference, access control, verification

DOI: 10.3233/JCS-140516

Journal: Journal of Computer Security, vol. 23, no. 2, pp. 197-228, 2015