Enforcing the Opacity of Modular Discrete Event Systems Using Supervisory Control

Abstract

Opacity is a security property that guarantees the confidentiality of secret information from a partial observer of the system. To address this problem, we propose a modular approach that uses Supervisory and Control Theory to design a global supervisor for Modular Discrete Event Systems (MDES). This approach assumes the attacker can observe the shared alphabet between modules, and takes into account the modular structure of the system; which significantly decreases computational complexity compared to monolithic methods. To achieve this, we introduce a reduced-complexity algorithm, based on the Hyper Symbolic Observation Graph. The HSOG is an abstraction graph that considers only events that have a direct impact on the opacity. This reduces the number of states to be considered, making the algorithm more efficient.