ModelChecking InfiniteState 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 highlevel (or confidential)events as well as lowlevel (or public) events, and a typical property requires that the highlevel events should not “influence ”the occurrence of lowlevel events. In other words, the sequence of lowlevel events observed from a system execution should not reveal “too much” information about the highlevel events that may have taken place. For example, the tracebased “noninference” property states that for every trace produced by the system, its projection to lowlevel events must also be a possible trace of the system. For a system satisfying noninference, a lowlevel adversary (who knows the language generated by the system) viewing only the lowlevel events in any execution cannot infer any information about the occurrence of highlevel events in that execution. Other wellknown properties include separability, generalized noninterference, nondeducibility of outputs etc. These properties are tracebased. Similarly there is another class of properties based on the structure of the transition system called bisimulationbased information flow properties, defined by Focardiand Gorrieriin1995.
In our thesis we study the problem of modelchecking the wellknown tracebased and bisimulationbased properties for some popular classes of infinitestate system models. We first consider tracebased properties. We define some languagetheoretic operations that help to characterize languageinclusion 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 modelchecking problem for F, whenever F, is effectively closed under these languagetheoretic operations. We apply this result to show that the modelchecking 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 modelchecking 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 modelchecking problem becomes decidable. Similarly we show that the problem of modelchecking bisimulationbased 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“ noninterference” 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)“passwordchecking” program failing it.“Abstract noninterference(ANI)”and its variants were proposed in the literature to generalize or weaken noninterference. We call these definitions qualitative refinements of noninterference. We study the problem of modelchecking many classes of finitedata 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 finitedata programs.
We finally study different quantitative refinements of noninterference proposed 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.
Collections
Related items
Showing items related by title, author, creator and subject.

Optimal Control of Information Epidemics in Homogeneously And Heterogeneously Mixed Populations
Kandhway, Kundan (20170923)Social networks play an important role in disseminating a piece of information in a population. Companies advertising a newly launched product, movie promotion, political campaigns, social awareness campaigns by governments, ... 
Algorithms for Multilingual IR in Low Resource Languages using Weakly Aligned Corpora
Tholpadi, GouthamMultilingual information retrieval (MLIR) methods generally rely on linguistic resources such as dictionaries, parallel corpora, etc., to overcome the language barrier. For low resource languages without these resources, ... 
Matching Domain Model with Source Code using Relationships
Bharat, Patil Tejas (20180130)We address the task of mapping a given domain model (e.g., an industrystandard reference model) for a given domain (e.g., ERP), with the source code of an independently developed application in the same domain. This has ...