Paper Info
Title
Secure Information Flow in Java via Reachability Analysis of Pushdown System
Abstract
Automated verification of noninterference is commonly considered more precise than type-based approach on enforcing secure information flow for program. We propose an approach on model checking symbolic pushdown system generated from Java bytecode, and develop a deployment-time verification framework to ensure noninterference of bytecode. In order to overcome the constraints brought by the nature of object-oriented language and application scenario, we extend self-composition to low-recorded self-composition to reduce the partial correctness judgements on safety property to reachability analysis. In this variation, meta-level indices of heap are recorded into the self-composed pushdown system for the construction of auxiliary interleaving assignments and branch condition to illegal-flow state. Our experiments show that the approach is more scalable than previous work based on automated verification.
Year
DOI
Venue
2010
10.1109/QSIC.2010.50
QSIC
Keywords
Field
DocType
type-based approach,symbolic pushdown system,information flow,self-composed pushdown system,low-recorded self-composition,java bytecode,branch condition,auxiliary interleaving assignment,object-oriented language,deployment time verification framework,pushdown system,automated verification,low recorded self-composition,deployment-time verification framework,application scenario,auxiliary interleaving assignments,partial correctness judgements reduction,noninterference,secure information flow,model checking symbolic pushdown system,object-oriented languages,self-composition,java,noninterference automated verification,formal verification,security of data,reachability analysis,indexes,object oriented language,security,object oriented languages,model checking
Programming language,Model checking,Computer science,Correctness,Heap (data structure),Theoretical computer science,Reachability,Java bytecode,Java,Bytecode,Formal verification
Conference
ISSN
ISBN
Citations 
1550-6002 E-ISBN : 978-0-7695-4131-0
978-0-7695-4131-0
6
PageRank 
References 
Authors
0.51
17
3
Name
Order
Citations
PageRank
Cong Sun160.51
Liyong Tang2343.82
Zhong Chen350358.35