Paper Info
Title
Model-checking trace-based information flow properties
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. (Work partially done while visiting Indian Institute of Science, Bangalore.)
Year
DOI
Venue
2011
10.3233/JCS-2010-0400
Model checking trace-based information flow properties
Keywords
Field
DocType
information flow property,pushdown system,system model,simple trace-based property,automata-theoretic technique,indian institute,basic security predicates bsps,security property,low-level user,trace-based information flow property,finite state system,finite-state system,building block,finite-state system model,pushdown system model,verifying bsps,basic security predicates,trace-based property,particular bsp,confidential event,basic security predicate,security,model checking,information flow
Information flow (information theory),Model checking,Programming language,Computer science,Theoretical computer science,Predicate (grammar),Undecidable problem
Journal
Volume
Issue
ISSN
19
1
0926-227X
ISBN
Citations 
PageRank 
383837780X
8
0.49
References 
Authors
16
4
Name
Order
Citations
PageRank
Deepak D'souza123917.90
Raveendra Holla2140.95
K. R. Raghavendra3171.71
Barbara Sprick4747.27