  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.
