Sciweavers

Share
JCS
2011

Model-checking trace-based information flow properties

8 years 3 months ago
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.
Deepak D'Souza, Raveendra Holla, K. R. Raghavendra
Added 14 May 2011
Updated 14 May 2011
Type Journal
Year 2011
Where JCS
Authors Deepak D'Souza, Raveendra Holla, K. R. Raghavendra, Barbara Sprick
Comments (0)
books