Files in this item
Files  Description  Format 

application/pdf Saboori_Anooshiravan.pdf (985kB)  (no description provided) 
Description
Title:  Verification and Enforcement of StateBased Notions of Opacity in Discrete Event Systems 
Author(s):  Saboori, Anooshiravan 
Director of Research:  Hadjicostis, Christoforos N. 
Doctoral Committee Chair(s):  Basar, Tamer 
Doctoral Committee Member(s):  Hadjicostis, Christoforos N.; Coleman, Todd P.; Sreenivas, Ramavarapu S.; Kumar, P.R. 
Department / Program:  Electrical & Computer Eng 
Discipline:  Electrical & Computer Engr 
Degree Granting Institution:  University of Illinois at UrbanaChampaign 
Degree:  Ph.D. 
Genre:  Dissertation 
Subject(s):  Discrete Event Systems
Security Finite Automata Partial Event Observation Information Flow Tracking Problems in Sensor Networks 
Abstract:  Motivated by security and privacy considerations in applications of discrete event systems, we describe and analyze the complexity of verifying various statebased notions of opacity in systems that are modeled as (possibly nondeterministic) finite automata with partial observation on their transitions. Assuming that the intruder observes system activity through some projection map and has complete knowledge of the system model, we define three notions of opacity with respect to a set of secret states: (i) initialstate opacity is a notion that requires the membership of the system true initial state to the set of secret states remain opaque (i.e., uncertain) to the intruder; (ii) Kstep opacity is a notion that requires that at any specific point in time within the last K observations, the entrance of the system state to the given set of secret states remain opaque to the intruder; (iii) infinitestep opacity is a notion that requires the entrance of the system state at any particular instant to the set of secret states remain opaque, for the length of the system operation, to the intruder. As illustrated via examples in the thesis, the above statebased notions of opacity can be used to characterize the security requirements in many applications, including encryption using pseudorandom generators, coverage properties in sensor networks, and anonymity requirements in protocols for web transactions. In order to model the intruder capabilities regarding initialstate opacity, we address the initialstate estimation problem in a nondeterministic finite automaton under partial observations on its transitions via the construction of an initialstate estimator. We analyze the properties and complexity of the initialstate estimator, and show how the complexity of the verification method can be greatly reduced in the special case when the set of secret states is invariant (i.e., it does not change over time). We also establish that the verification of initialstate opacity is a PSPACEcomplete problem. In order to verify Kstep opacity, we introduce the Kdelay state estimator which constructs the estimate of the state of the system K observations ago (Kdelayed state estimates) for a given nondeterministic finite automaton under partial observation on its transitions. We provide two methods for constructing Kdelay state estimators, and hence two methods for verifying Kstep opacity, and analyze the computational complexity of both. In the process, we also establish that the verification of $K$step opacity is an NPhard problem. We also investigate the role of the delay K in Kstep opacity and show that there exists a delay K* such that Kstep opacity implies K'step opacity for any K and K' such that K'>K>= K*. This is not true for arbitrary K'>K though the converse holds trivially. Infinitestep opacity can be verified via the construction of a currentstate estimator and a bank of appropriate initialstate estimators. The verification of infinitestep opacity is also shown to be a PSPACEhard problem. Finally, we tackle the problem of constructing a minimally restrictive opacityenforcing supervisor (MOES) which limits the system's behavior within some prespecified legal behavior while enforcing opacity requirements. We characterize the solution to MOES, under some mild assumptions, in terms of the supremal element of certain controllable, normal, and opaque languages. We also show that this supremal element always exists and that it can be implemented using state estimators. The result is a supervisor that achieves conformance to the prespecified legal behavior while enforcing opacity by disabling, at any given time, a subset of the controllable system events, in a way that minimally restricts the range of allowable system behavior. 
Issue Date:  20110114 
URI:  http://hdl.handle.net/2142/18226 
Rights Information:  Copyright 2010 Anooshiravan Saboori 
Date Available in IDEALS:  20110114 
Date Deposited:  December 2 
This item appears in the following Collection(s)

Graduate Dissertations and Theses at Illinois
Graduate Theses and Dissertations at Illinois 
Dissertations and Theses  Electrical and Computer Engineering
Dissertations and Theses in Electrical and Computer Engineering