Name
Abstract | ||
|---|---|---|
We propose an approach on model checking information flow for imperative language with procedures. We characterize our model with pushdown system, which has a stack of unbounded length that naturally models the execution of procedural programs. Because the type-based static analysis is sometimes too conservative and rejects safe program as ill-typed, we take a semantic-based approach by self-composing symbolic pushdown system and specifying noninterference with LTL formula. Then we verify this LTL-expressed property via model checker Moped. Except for overcoming the conservative characteristic of type-based approach, our motivation also includes the insufficient state of arts on precise information flow analysis under interprocedural setting. To remedy the inefficiency of model checking compared with type system, we propose both compact form and contracted form of self-composition. According to experimental results, they can greatly increase the efficiency of realistic verification. Our method provides flexibility on separating program abstraction from noninterference verification, thus could be expected to use on different programming languages. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1109/UIC-ATC.2009.44 | Clinical Orthopaedics and Related Research |
Keywords | Field | DocType |
model checking pushdown system,conservative characteristic,type-based approach,symbolic pushdown system,programming languages,information flow,compact form,imperative language,model checking,semantic-based approach,noninterference verification,model checker moped,type system,pushdown system,ltl formula,model checking information flow,model checker,data flow analysis,program abstraction,type-based static analysis,noninterference,program verification,secure information flow,self-composition,sun,data structures,information analysis,computer languages,programming language,educational technology,art,data mining,boolean functions,computational modeling,static analysis,pervasive computing | Boolean function,Data structure,Information flow (information theory),Programming language,Abstraction,Model checking,Computer science,Static analysis,Imperative programming,Data-flow analysis,Theoretical computer science | Journal |
Volume | Issue | ISBN |
abs/1012.3100 | null | 978-0-7695-3737-5 |
Citations | PageRank | References |
10 | 0.63 | 16 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cong Sun | 1 | 10 | 0.63 |
| Liyong Tang | 2 | 23 | 3.73 |
| Zhong Chen | 3 | 28 | 3.08 |