Note: [**] Current address: Oracle Labs, Brisbane.
Abstract: We consider the problem of model-checking some of the well-known trace-based information flow properties from the literature for classes of infinite-state system models. We first define some language-theoretic operations that help to characterize language inclusion in terms of these properties. This gives us a reduction of the language inclusion problem for a class of system models, say F, to the model checking problem for F, whenever F is effectively closed under these language-theoretic operations. We apply this result to show that the problem of model-checking any of these properties for One Counter Nets, One-Counter Automata, Basic Parallel Processes, and some properties for deterministic One Counter Automata, is undecidable. We also consider the class of Visibly Pushdown Systems and show that their model-checking problem is undecidable for a couple of properties. For the special case when all confidential events are internal we show that model-checking each of these properties for Visibly Pushdown Systems becomes decidable.
Keywords: Model-checking, Petri net, information flow, security, pushdown, visibly pushdown, deterministic pushdown, one-counter
