Model-Checking Infinite-State Systems For Information Flow Security Properties

Abstract

Information flow properties are away of specifying security properties of systems ,dating back to the work of Goguen and Meseguer in the eighties. In this framework ,a system is modeled as having high-level (or confidential)events as well as low-level (or public) events, and a typical property requires that the high-level events should not “influence ”the occurrence of low-level events. In other words, the sequence of low-level events observed from a system execution should not reveal “too much” information about the high-level events that may have taken place. For example, the trace-based “non-inference” property states that for every trace produced by the system, its projection to low-level events must also be a possible trace of the system. For a system satisfying non-inference, a low-level adversary (who knows the language generated by the system) viewing only the low-level events in any execution cannot infer any in-formation about the occurrence of high-level events in that execution. Other well-known properties include separability, generalized non-interference, non-deducibility of outputs etc. These properties are trace-based. Similarly there is another class of properties based on the structure of the transition system called bisimulation-based information flow properties, defined by Focardiand Gorrieriin1995. In our thesis we study the problem of model-checking the well-known trace-based and bisimulation-based properties for some popular classes of infinite-state system models. We first consider trace-based properties. We define some language-theoretic operations that help to characterize language-inclusion in terms of satisfaction 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 model-checking problem for Petri nets, push down systems and for some properties on deterministic push down systems is undecidable. We also consider the class of visibly pushdown systems and show that their model-checking problem is undecidable in general(for some properties).Then we show that for the restricted class of visibly pushdown systems in which all the high (confidential) event are internal, the model-checking problem becomes decidable. Similarly we show that the problem of model-checking bisimulation-based properties is undecidable for Petrinets, pushdown systems and process algebras. Next we consider the problem of detecting information leakage in programs. Here the programs are modeled to have low and high inputs and low outputs. The well known definition of“ non-interference” on programs says that in no execution should the low outputs depend on the high inputs. However this definition was shown to be too strong to be used in practice, with a simple(and considered to be safe)“password-checking” program failing it.“Abstract non-interference(ANI)”and its variants were proposed in the literature to generalize or weaken non-interference. We call these definitions qualitative refinements of non-interference. We study the problem of model-checking many classes of finite-data programs(variables taking values from a bounded domain)for these refinements. We give algorithms and show that this problem is in PSPACE for while, EXPTIME for recursive and EXPSPACE for asynchronous finite-data programs. We finally study different quantitative refinements of non-interference pro-posed in the literature. We first characterize these measures in terms of pre images. These characterizations potentially help designing analysis computing over and under approximations for these measures. Then we investigate the applicability of these measures on standard cryptographic functions.