
etd AT Indian Institute of Science >
Division of Electrical Sciences >
Computer Science and Automation (csa) >
Please use this identifier to cite or link to this item:
http://etd.iisc.ernet.in/2005/2601

Title:  ModelChecking InfiniteState Systems For Information Flow Security Properties 
Authors:  Raghavendra, K R 
Advisors:  D'Souza, Deepak 
Keywords:  Information Flow Properties Computer Security Computer Access Control InfiniteState System Models Information Leakage Detection, Computer Programs Tracebased Information Flow Properties Bisimulationbased Information Flow Properties Information Flow Properties  Model Checking System Models Petri Nets Process Algebra  Model Checking Pushdown Systems  Model Checking Access Control Models 
Submitted Date:  Dec2013 
Series/Report no.:  G26018 
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. 
Abstract file URL:  http://etd.ncsi.iisc.ernet.in/abstracts/3395/G26018Abs.pdf 
URI:  http://etd.iisc.ernet.in/handle/2005/2601 
Appears in Collections:  Computer Science and Automation (csa)

Items in etd@IISc are protected by copyright, with all rights reserved, unless otherwise indicated.
