Verifying Information Flow Security in Visibly Pushdown Automata?

Abstract. Information flow control is an important area in computer security. It aims at restricting what a low level observer can deduce from his observa-tions about high level system behavior. We investigate the problem of verifying possibilistic information flow properties for visibly pushdown automata. Such properties can be expressed by Basic Security Predicates (BSPs) in the Modular Assembly Kit for Security [15]. They are, however, known to be undecidable for context free languages [8]. The class of visibly pushdown languages (VPLs) [2] lies between regular and deterministic context free languages. Still, VPLs share many desirable properties with the class of regular languages. In addition, they allow for model checking non-regular properties like stack inspection or pre- and post-conditions. Assum-ing a low level observable stack, we show in this paper how BSPs can be auto-matically verified for VPLs. In a second step, we extend this result to intransitive information flow properties.