Verification and Enforcement of State-Based Notions of Opacity in Discrete Event Systems

Discrete Event Systems;Security;Finite Automata;Partial Event Observation;Information Flow;Tracking Problems in Sensor Networks

Saboori, Anooshiravan

关键词: Discrete Event Systems;    Security;    Finite Automata;    Partial Event Observation;    Information Flow;    Tracking Problems in Sensor Networks;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/18226/Saboori_Anooshiravan.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

Motivated by security and privacy considerations in applications of discrete event systems, we describe and analyze the complexity ofverifying various state-based notions of opacity in systems that are modeled as (possibly non-deterministic) finite automata with partial observation on their transitions. Assuming that the intruder observes system activity through someprojection map and has complete knowledge of the system model, we define three notions of opacity with respect to a set of secret states: (i) initial-state opacity is a notionthatrequiresthe membership of the system true initial state to the set of secret states remain opaque (i.e., uncertain) to the intruder; (ii) K-step opacity is a notion that requires thatat any specific point in time within the last K observations, the entrance of the systemstateto the given set of secret statesremain opaqueto the intruder;(iii) infinite-step opacity is a notion that requiresthe entrance of the systemstate at any particular instantto the set of secret statesremain opaque, for the length of the system operation, to the intruder.As illustrated via examples in the thesis, the above state-based notions of opacitycan be used to characterize the security requirements in many applications, includingencryption using pseudo-random generators, coverage properties in sensor networks, and anonymity requirements in protocols for web transactions.In order to model the intruder capabilities regarding initial-state opacity, weaddress the initial-state estimation problem in anon-deterministic finite automaton under partial observations on its transitions via the construction of an initial-state estimator. We analyze the properties and complexity of the initial-state 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 initial-state opacity is a PSPACE-complete problem. In order to verify K-step opacity, we introduce the K-delay state estimator which constructs the estimate of the state of the system K observations ago (K-delayed state estimates) for a given non-deterministic finite automaton under partial observation on its transitions.We provide two methods for constructing K-delay state estimators, and hence two methods for verifying K-step opacity, and analyzethe computational complexity of both. In the process, we also establish that the verification of $K$-step opacity is an NP-hard problem. We also investigate the role of the delay K in K-step opacity and show that there exists a delay K* such that K-step opacity implies K'-step opacityfor any K and K' such that K'>K>= K*. This is not true for arbitrary K'>K though the converse holds trivially. Infinite-step opacity can be verified via the construction of a current-state estimator and a bank ofappropriate initial-state estimators.The verification of infinite-step opacity is also shown to be a PSPACE-hard problem.Finally, wetackle the problem of constructing a minimally restrictive opacity-enforcing supervisor (MOES)which limits the system's behavior within some pre-specified 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 pre-specified legal behavior while enforcing opacity bydisabling, at any given time, a subset of the controllable system events, in a way that minimally restricts the range of allowable system behavior.