Discrete Event Systems: Opacity and Its Enforcement

Abstract

Opacity is an information-flow property used in privacy and security applications. A dynamic system is opaque if an external observer that knows the system model and makes online observations of its behavior is not able to detect with certainty some "secret" information about the system. We discuss various notions of opacity and their verification in the context of discrete event systems modeled by automata or transition systems: current-state opacity, initial-state opacity, and K-step opacity. Then we consider how to enforce opacity for systems that are not opaque. We focus on opacity enforcement using obfuscation, when an external interface edits the outputs of the system in order to confuse the observer. We present solution methodologies for different variations of this problem. We conclude with illustrative examples of opacity in the context of location privacy in location-based services.