Secure Information Flow by Model Checking Pushdown System
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.