Supervisor Obfuscation Against Actuator Enablement Attack
For researchers in discrete event systems and cyber-physical security, this work addresses a novel attack scenario with a provably minimal-state solution.
The paper proposes a method to obfuscate supervisors against actuator enablement attacks, preserving the original closed-loop system behavior while achieving minimal state count. The approach combines separating automata computation with SAT solvers and a verification technique for attackability.
In this paper, we propose and address the problem of supervisor obfuscation against actuator enablement attack, in a common setting where the actuator attacker can eavesdrop the control commands issued by the supervisor. We propose a method to obfuscate an (insecure) supervisor to make it resilient against actuator enablement attack in such a way that the behavior of the original closed-loop system is preserved. An additional feature of the obfuscated supervisor, if it exists, is that it has exactly the minimum number of states among the set of all the resilient and behavior-preserving supervisors. Our approach involves a simple combination of two basic ideas: 1) a formulation of the problem of computing behavior-preserving supervisors as the problem of computing separating finite state automata under controllability and observability constraints, which can be efficiently tackled by using modern SAT solvers, and 2) the use of a recently proposed technique for the verification of attackability in our setting, with a normality assumption imposed on both the actuator attackers and supervisors.