Hyper Symbolic Observation Graph to Enforce Opacity of Discrete Event Systems using Supervisory Control

Discrete Event systems are dynamic systems with two main characteristics: their set of states is discrete and their dynamic is event driven (as opposed to time driven). In this paper, we study a security property for DES called opacity. A system T, partially observed by a third party -called an attacker- is said to be opaque if the attacker can never conclude from its provided interface that T is in a secret state. Given a critical system that may leak confidential information, an attacker and a subset of controllable actions, we propose an approach to synthesize a controller that enforces the system's opacity. This controller is designed as a function that applies, at run time, on the current executions to disable any controllable action that eventually leads to the violation of the system's opacity. Our approach is based on a novel graph called a Hyper Symbolic Observation Graph. The language obtained under control is proven to be maximal whatever is the relationship between the attacker and the controller observations.