Model-checking trace-based information flow properties

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 tracebased 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.

• Type: Journal
• Year: 2011
• Where: JCS
• Authors: Deepak D'Souza, Raveendra Holla, K. R. Raghavendra, Barbara Sprick
• Keywords: Information flow Properties, JCS 2011, Trace-based Information, finite-state Systems