At Design-Time Approach for Supervisory Control of Opacity

Opacity is a property of information flow that characterizes the ability of a system to keep a secret information hidden from a malicious external entity, called an attacker. Given a critical system that may leak confidential information, an attacker with partial observation of the system 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, to the current execution to disable any controllable action that eventually leads to the violation of the opacity of the system. The supervision function is built at design time based on a new version of the symbolic observation graph that represents a reduced abstraction of the state space graph of the system preserving the observation of both the attacker and the controller. The language induced by this function is proven to be controllable, observable and supremal no matter the relation that exists between the observations of the attacker and the controller.