A new approach for synthesizing opacity-enforcing supervisors for partially-observed discrete-event systems

Opacity is a confidentiality property for partially-observed discrete-event systems relevant to the analysis of security and privacy in cyber and cyber-physical systems. It captures the plausible deniability of the system´s “secret” in the presence of an outside observer that is potentially malicious. In this paper, we consider the enforcement of opacity on systems modeled by finite-state automata. We assume that the given system is not opaque and the objective is to restrict its behavior by supervisory control in order to enforce opacity of its secret. We consider the general setting of supervisory control under partial observations where the controllable events need not all be observable. Our approach for the synthesis of an opacity enforcing supervisor is based on the construction of a new transition system that we call the “All Inclusive Controller for Opacity” (or AIC-O). The AIC-O is a finite bipartite transition system that embeds in its transition structure all valid opacity enforcing supervisors. We present an algorithm for the construction of the AIC-O and discuss its properties. We then develop a synthesis algorithm, based on the AIC-O, that constructs a “maximally permissive” opacity-enforcing supervisor. Our approach generalizes previous approaches in the literature for opacity enforcement by supervisory control.