Paper Info
Title
On the Decidability of Model-Checking Information Flow Properties
Abstract
Current standard security practices do not provide substantial assurance about information flow security: the end-to-end behavior of a computing system. Noninterference is the basic semantical condition used to account for information flow security. In the literature, there are many definitions of noninterference: Non-inference, Separability and so on. Mantel presented a framework of Basic Security Predicates (BSPs) for characterizing the definitions of noninterference in the literature. Model-checking these BSPs for finite state systems was shown to be decidable in [8]. In this paper, we show that verifying these BSPs for the more expressive system model of pushdown systems is undecidable. We also give an example of a simple security property which is undecidable even for finite-state systems: the property is a weak form of non-inference called WNI, which is not expressible in Mantel's BSP framework.
Year
DOI
Venue
2008
10.1007/978-3-540-89862-7_2
ICISS
Keywords
Field
DocType
bsp framework,pushdown system,model-checking information flow properties,current standard security practice,basic security predicates,information flow security,computing system,expressive system model,finite state system,simple security property,finite-state system,model checking,information flow,system modeling
Information flow (information theory),Model checking,Computer science,Theoretical computer science,Decidability,Turing machine,Predicate (grammar),System model,Computing systems,Undecidable problem
Conference
Volume
ISSN
Citations 
5352
0302-9743
6
PageRank 
References 
Authors
0.47
16
5
Name
Order
Citations
PageRank
Deepak D'souza123917.90
Raveendra Holla2140.95
Janardhan Kulkarni315317.73
Raghavendra K. Ramesh460.81
Barbara Sprick5747.27