Date Added: Dec 2010
The authors propose an approach on model checking information flow for imperative language with procedures. They characterize their 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, they take a semantic-based approach by self-composing symbolic pushdown system and specifying noninterference with LTL formula. Then, they verify this LTL-expressed property via model checker Moped. Except for overcoming the conservative characteristic of type-based approach, their 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, they propose both compact form and contracted form of self-composition.