Supervisor Obfuscation Against Actuator Enablement Attack

TL;DR

This paper introduces a method to obfuscate supervisors in control systems to prevent actuator enablement attacks, preserving system behavior and minimizing supervisor states using SAT solvers and attack verification techniques.

Contribution

It presents a novel approach combining SAT-based supervisor synthesis with attackability verification to enhance security against actuator enablement attacks.

Findings

Obfuscated supervisors are resilient against actuator enablement attacks.

The method preserves the original system behavior.

The obfuscated supervisor has minimal states among all resilient supervisors.

Abstract

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.