Optimal Supervisory Control of Opacity for Modular Systems

In this paper, we consider parallel and concurred systems modeled as Discrete Event Systems where secret behavior should remain hidden from a malicious third party, called an attacker, that is partially observing the system. Opacity is a security property that characterizes whether this attacker is able or not to deduce some secret information from its provided interface. We address the problem of enforcing the opacity of modular Discrete Event Systems using Supervisory and Control Techniques. We propose a reduced-complexity algorithm, based on the Hyper Symbolic Observation Graph (HSOG). The HSOG allows to abstract the original system and takes into account only “important” events i.e., those observed by the supervisor and the attacker. Under the hypothesis that each module is observed by a local attacker, and assuming that the attacker can observe the interfaces between the different modules, we synthesize a local supervisor to each module. The global supervisor is then deduced from local supervisors without computing the synchronized product of the whole system. Our approach restricts the behavior of the system to its opaque part while enabling the most permissive behavior. We prove that the language of the obtained system is observable, controllable, supremal and opaque-by construction. To demonstrate the efficiency of our approach and its applicability in real life scenario, we illustrate it through an automated manufacturing case study.