Paper Info
Title
Enforcing Reactive Noninterference with Reachability Analysis
Abstract
The reactive computational model is pervasively used as a proper abstraction of web-based applications which receive inputs and generate outputs throughout execution. The present static enforcements of information flow security on reactive program are either based on type system or abstract interpretation. In this work we first propose an approach using automated verification to check conformance with information flow policy for reactive program. This approach utilizes our previous idea to incorporate self-composition with reach ability analysis. In order to reduce the state space of model, we propose the Store-Match Self-Composition (SMSC) to avoid duplicating the low channels. The result of preliminary experiments shows that our approach is more precise and efficient than existing work and also more efficient than our previous reach ability analysis.
Year
DOI
Venue
2011
10.1109/ITNG.2011.63
ITNG
Keywords
Field
DocType
information flow,reactive computational model,abstract interpretation,web-based applications,store-match self-composition,information flow policy,information flow security,pushdown system,smsc,automated verification,previous reach ability analysis,previous idea,internet,program analysis,reactive noninterference,enforcing reactive noninterference,reach ability analysis,noninterference,formal verification,reactive program,security of data,reachability analysis,semantics,type system,state space,security,computer model,computational modeling,secure computation,web based applications,data structure,data structures
Information flow (information theory),Data structure,Abstract interpretation,Computer science,Communication channel,Reachability,Program analysis,State space,Formal verification,Distributed computing
Conference
ISBN
Citations 
PageRank 
978-0-7695-4367-3
1
0.35
References 
Authors
18
3
Name
Order
Citations
PageRank
Cong Sun152.44
Liyong Tang2343.82
Zhong Chen3283.08