Model-checking trace-based information flow properties^*

Article type: Research Article

Authors: D'Souza, Deepak^a | Holla, Raveendra^a | Raghavendra, K.R.^a | Sprick, Barbara^{b; **}

Affiliations: [a] Department of Computer Science and Automation, Indian Institute of Science, Bangalore, India. E-mails: deepakd@csa.iisc.ernet.in, raveendra@csa.iisc.ernet.in, raghavendrakr@csa.iisc.ernet.in | [b] TU Darmdstadt, Fachbereich Informatik, Darmdstadt, Germany. E-mail: sprick@mais.informatik.tu-darmstadt.de

Note: [*] Preliminary results in this paper appeared in [9] and [7].

Note: [**] Work partially done while visiting Indian Institute of Science, Bangalore.

Abstract: In this paper we consider the problem of verifying trace-based information flow properties for different classes of system models. We begin by proposing an automata-theoretic technique for model-checking trace-based information flow properties for finite-state systems. We do this by showing that Mantel's Basic Security Predicates (BSPs), which were shown to be the building blocks of most trace-based properties in the literature, can be verified in an automated way for finite-state system models. We also consider the problem for the class of pushdown system models, and show that it is undecidable to check such systems for any of the trace-based information flow properties. Finally we consider a simple trace-based property we call “weak non-inference” and show that it is undecidable even for finite-state systems.

Keywords: Model-checking, non-interference, information flow properties, security

DOI: 10.3233/JCS-2010-0400

Journal: Journal of Computer Security, vol. 19, no. 1, pp. 101-138, 2011