IEEE.org | IEEE Xplore Digital Library | IEEE Standards | IEEE Spectrum | More Sites
Call for Award Nominations
Thu, February 18, 2021
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.