Verification and Enforcement of Opacity Security Properties in Discrete Event Systems.

Abstract

The need for stringent cybersecurity is becoming significant as computers and networks are integrated into every aspect of our lives. A recent trend in cybersecurity research is to formalize security notions and develop theoretical foundations for designing secure systems. In this dissertation, we address a security notion called opacity based on the control theory for Discrete Event Systems (DES). Opacity is an information-flow property that captures whether a given secret of the system can be inferred by intruders who passively observe the behavior of the system. Finite-state automata are used to capture the dynamics of computer systems that need to be rendered opaque with respect to a given secret. Under the observation of the intruder, the secret of the system is opaque if “whenever the secret has occurred, there exists another non-secret behavior that is observationally equivalent.” This research focuses on the analysis and the enforcement of four notions of opacity. First, we develop algorithms for verifying opacity notions under the attack model of a single intruder and that of multiple colluding intruders. We then consider the enforcement of opacity when the secret is not opaque. Specifically, we propose a novel enforcement mechanism based on event insertion to address opacity enforcement for a class of systems whose dynamics cannot be modified. An insertion function, placed at the output of the system, inserts fictitious observable events to the system’s output without interacting with the system. We develop a finite structure called the All-Insertion Structure (AIS) that enumerates all valid insertion functions. The AIS establishes a necessary and sufficient condition for the existence of a valid insertion function, and provides a structure to synthesize one insertion function. Furthermore, we introduce the maximum total cost and the maximum mean cost to quantify insertion functions. A condition for determining which cost objective to use is established. For each cost, we develop an algorithmic procedure for synthesizing an optimal insertion function from the AIS. Finally, our analysis and enforcement procedure is applied to ensuring location privacy in location-based services.