Verification and Enforcement of Opacity Security Properties in Discrete Event Systems

A recent trend in cybersecurity research is to formalize security notions and develop theoretical foundations for secure system design. In this dissertation, we address a security property called opacity based on the control theory for Discrete Event Systems. Finite-state automata are used to capture the dynamics of systems that need to be rendered opaque with respect to a given secret. Under the passive observation of the intruder, 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. We provide algorithms for verifying these opacity notions under the attack model of a single intruder and that of multiple colluding intruders. We 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 algorithmic procedure that synthesizes one insertion function is developed. We also synthesize an optimal insertion function with respect to a given cost criterion. Finally, our analysis and enforcement procedures are applied to ensuring location privacy in location-based services.