Computer Science – Cryptography and Security
Scientific paper
2010-12-14
Computer Science
Cryptography and Security
20 pages, this is an extended version of the paper published in UIC-ATC'09
Scientific paper
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 inter-procedural 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 our 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.
Chen Zhong
Sun Cong
Tang Liyong
No associations
LandOfFree
Secure Information Flow by Model Checking Pushdown System does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Secure Information Flow by Model Checking Pushdown System, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Secure Information Flow by Model Checking Pushdown System will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-180149