Source-linked AI summary
Detection and Mitigation of Classes of Attacks in Supervisory Control Systems
Lilian Kawakami Carvalho, Yi-Chin Wu, Raymond Kwong, Stéphane Lafortune
TL;DR
Network-connected supervisory control systems can be attacked through vulnerable actuators and sensors, threatening reachability of unsafe states. The paper models actuator enablement, sensor erasure, and sensor insertion attacks, proposes online detection followed by safe mode, and characterizes GF-safe controllability as a necessary and sufficient condition verifiable with diagnoser or verifier automata. The methodology is illustrated with a traffic control example.
Problem
Network-connected supervisory control systems need intrusion detection and mitigation because attackers can manipulate vulnerable actuator commands or sensor readings and drive the system toward unsafe states.
Method
The paper models AE-, SE-, and SI-attacks, detects them online, switches to safe mode by disabling all controllable events, and verifies GF-safe controllability with diagnoser or verifier automata.
Results
GF-safe controllability is characterized as the condition the system should satisfy to prevent damage under the considered attacks and defense strategy.
Takeaways & Limitations
The methodology provides a formal way to model attack effects, assess whether conservative safe-mode mitigation prevents unsafe-state reachability, and illustrate the analysis in a traffic control system.
Takeaways & Limitations
Actuator disablement attacks are not further analyzed because they cannot violate safety as defined, although they may cause blocking.
Abstract
from arXiv · showhide
The deployment of control systems with network-connected components has made feedback control systems vulnerable to attacks over the network. This paper considers the problem of intrusion detection and mitigation in supervisory control systems, where the attacker has the ability to enable or disable vulnerable actuator commands and erase or insert vulnerable sensor readings. We present a mathematical model for the system under certain classes of actuator enablement attacks, sensor erasure attacks, or sensor insertion attacks. We then propose a defense strategy that aims to detect such attacks online and disables all controllable events after an attack is detected. We develop an algorithmic procedure for verifying whether the system can prevent damage from the attacks considered with the proposed defense strategy, where damage is modeled as the reachability of a pre-defined set of unsafe system states.The technical condition of interest that is necessary and sufficient in this context, termed "GF-safe controllability", is characterized. We show that the verification of GF-safe controllability can be performed using diagnoser or verifier automata. Finally, we illustrate the methodology with a traffic control system example.
1 Introduction
Networked feedback control systems are vulnerable to cyber threats, motivating formal intrusion detection and mitigation for safety-critical supervisory systems. The paper models several attack classes, proposes online detection with safe-mode mitigation, and develops safe-controllability verification procedures.
- Network-connected feedback control systems are vulnerable to cyber threats, especially where safety-critical systems such as avionics and power grids are involved.
- The paper models attacks that alter vulnerable actuator commands or sensor readings and targets prevention of unsafe-state reachability.
- The work uses model-based representations to characterize attacker-induced unsafe behavior, defender resiliency, and deviations from normal behavior.
- The paper extends earlier intrusion-prevention work by explicitly modeling multiple attack classes, algorithmic detection, and switching to safe mode.
- The proposed defense detects attacks online and disables all controllable events after detection with certainty.
- AE-safe and GF-safe controllability are developed with diagnoser and verifier procedures, while new results cover Sections 5.4, 6, 7, and 8.
2 Types of attacks
The attack model lets an attacker manipulate vulnerable actuators or sensors while affecting both supervisor observations and plant control actions. Four attack classes are defined, and the intrusion detector is designed to identify and mitigate them.
- The system contains a plant, partial-observation supervisor, controllable actuators, observable sensors, and an attacker-mediated architecture.
- Actuator enablement attacks override disabled vulnerable events by enabling them, whereas actuator disablement attacks override enabled vulnerable events by disabling them.
- Sensor erasure attacks hide occurrences of vulnerable observable events from the supervisor and intrusion detector.
- Sensor insertion attacks add fictitious vulnerable observable events to the observation streams of the supervisor and intrusion detector.
- The fixed supervisor is paired with an intrusion detector that observes the attacked system and reports detected attacks for mitigation.
3 Mathematical framework
The mathematical framework represents plants and supervisors as finite-state discrete-event systems with partial observation and controllability. Supervisors restrict plant behavior to an admissible specification using projected event observations.
- Plants are modeled as deterministic finite-state automata with finite states, events, an initial state, transitions, and optionally marked states.
- Events are partitioned into observable and unobservable sets and into controllable and uncontrollable sets.
- The natural projection maps observable events to themselves and unobservable events to the empty string, extending recursively over strings.
- A partial-observation supervisor maps projected plant behavior to enabled-event decisions and therefore gives the same control action to strings with the same projection.
- The supervisor restricts plant behavior to a specification K, while controllability and observability are necessary and sufficient for enforcing K.
4 Actuator enablement attacks
Actuator enablement attacks can override supervisor disable commands and drive the plant toward unsafe states. The paper models these attacks compositionally, detects them online, switches to conservative safe mode, and verifies whether AE-safe controllability prevents damage.
- 4 Actuator enablement attacks: AE-attacks enable vulnerable actuator events that the supervisor has disabled, potentially driving the plant to unsafe states.
- 4 Actuator enablement attacks: The attack model interprets the supervisor–attacker control combination as an OR operation on enabled vulnerable events.
- 4 Actuator enablement attacks: The nominal supervisor may enforce a controllable and observable specification K without being resilient to actuator attacks.
- Detection and mitigation: The detector switches the supervisor to safe mode after certain detection, permanently disabling all controllable events.
- Attack model: The AE model uses dilation and compression to represent attacker events and their correspondence to vulnerable actuator events.
- Attack model: Algorithm 1 constructs attacked plant and supervisor automata, adds attack and uncontrollable-event self-loops, and composes them into GM.
- Example 1: In Example 1, enabling vulnerable event b lets the plant move from state 2 to state 3 and reach unsafe state 4 through uncontrollable event c.
5 Detection and mitigation of actuator enablement attacks
The paper models actuator enablement attacks that can drive supervisory control systems toward unsafe states, then proposes online detection and safe-mode mitigation. AE-safe controllability characterizes exactly when detection followed by disabling controllable events prevents unsafe reachability, with diagnoser- and verifier-based tests.
- Defense strategy: The defense detects actuator attacks online and switches the supervisor to safe mode, disabling controllable events after detection.The strategy is intended to prevent damage before the plant reaches unsafe states.
- AE-safe controllability: AE-safe controllability requires detecting every attack occurrence and disabling a controllable event before the plant reaches an unsafe state.The condition is defined over attacked actuator events, unsafe states, and the closed-loop attacked system.
- AE-safe controllability: System safety under the attack and defense model holds if and only if the system is AE-safe controllable.The characterization is stated with respect to the observation projection, vulnerable actuator events, and unsafe-state set.
- Diagnoser-based verification: Diagnoser verification builds a label automaton with the attacked system and checks uncertain and first-entered certain states for unsafe-state reachability.The diagnoser identifies whether attacks are certain before unsafe states can be reached.
- Failure condition: Immediate attack detection does not guarantee safety when uncontrollable attacked events can still carry the plant to an unsafe state.In the example, the attack is detected before unsafe state (2, 4), but uncontrollable event c still permits that state, violating AE-safe controllability.
- Verifier-based verification: The verifier procedure marks possible attack detection and tests whether unsafe states remain reachable through uncontrollable events after detection.The verifier adds a state A for possible detection and checks unsafe reachability from that state.
6 Sensor erasure attacks
Sensor erasure attacks replace vulnerable observable events with unobservable counterparts, potentially desynchronizing the supervisor from the plant and causing unsafe behavior or blocking.
- Attack model: SE-attacks erase vulnerable observable sensor events, making them unobservable to the supervisor and plant model.The attack model adds corresponding erased-event transitions while preserving inherited controllability properties.
- Attack model: Algorithm 4 constructs the attacked closed-loop system by augmenting the event set and building plant and supervisor automata for erased events.Uncontrollable events are added where needed so controllability is not violated after supervisor and plant behavior become out of sync.
- Examples: In Example 4, erasing b after a makes the supervisor believe the plant is in state 2 while it is actually in state 4, enabling c and reaching an unsafe state.The attacked closed-loop system is computed as GM = Ha∥Ga.
7 Sensor insertion attacks
Sensor insertion attacks inject fictitious observable events that the supervisor cannot distinguish from genuine events, potentially changing control actions and steering the plant to unsafe states.
- Attack model: SI-attacks insert fictitious occurrences of vulnerable observable events into the observation streams of the supervisor and detection module.The attacker is assumed to know the supervisor state and inserts events only when the supervisor expects them to be feasible.
- Attack model: Algorithm 5 models an SI-attack by adding onset events and paired plant transitions that emulate vulnerable events without advancing the plant to a new state.Inserted events remain indistinguishable from genuine observable events to the supervisor and detector.
- Attack model: The supervisor realization gains self-loops for feasible vulnerable insertions and additional uncontrollable-event loops to preserve controllability.The attacked closed-loop system is computed as GM = Ha∥Ga.
- Example: In Example 6, onset bi followed by inserted b makes the supervisor believe the system is in state 3 while it is actually in state 2, enabling c and reaching an unsafe state.The example uses vulnerable event set Eo,v = {b} and unsafe state set Xf = {5}.
8 General approach for detection of attacks
The paper generalizes safe controllability across actuator enablement, sensor erasure, and sensor insertion attacks, using diagnoser or verifier procedures to test whether detection and mitigation prevent unsafe states.
- Defense strategy: After detecting an attack, the intrusion detector directs the supervisor into safe mode, where all controllable events are disabled.The defense is effective only when detection occurs before unsafe-state reachability and disabling can prevent the remaining behavior.
- Generalized condition: GF-safe controllability is the generalized property used to analyze whether the proposed detection and mitigation strategy prevents unsafe states across attack types.For SE- and SI-attacks, it becomes SE-safe controllability and SI-safe controllability after constructing the corresponding attacked model.
- Verification: Algorithm 6 uses a parameterized label automaton and diagnoser to test whether attacks are detected before unsafe states and whether the supervisor can disable events in time.A verifier-based test can also be obtained by adapting the corresponding algorithm to each attack case.
- Examples: For Example 4, an uncertain diagnoser state contains an unsafe state, so the system under SE-attacks is not SE-safe controllable.The diagnoser analysis therefore identifies a case where attack detection and mitigation cannot prevent unsafe reachability.
- Examples: For Example 6, the SI-attack is not detected by the diagnoser and the system reaches unsafe state Xf = {5}, so it is not SI-safe controllable.The corresponding diagnoser is shown in Figure 13.
- Scope and caveats: After GF-safe controllability is verified, SE- and SI-attack models may still require a separate deadlock test.Example 5 demonstrates why safety verification alone does not settle blocking behavior.
- Scope and caveats: The methodology can model combinations of attacks, while attackers that do not attack at every opportunity require assumptions about their knowledge of plant and supervisor state spaces.Acquiring that attacker knowledge is identified as application-dependent future work.
9 Traffic control system example
The traffic-control example evaluates sensor-erasure and sensor-insertion attacks using the proposed attack models and safety criteria. Sensor erasure avoids unsafe states but deadlocks, whereas sensor insertion reaches an unsafe state and evades detection.
- Traffic control system example: The example models two vehicles traveling through four road sections toward a shared destination.Vehicle-entry events are denoted a_i and b_i for vehicles a and b.
- Sensor-erasure attack: Under sensor erasure, vulnerable sensor events are {a3, b3}, and the attacked closed-loop system is constructed using Algorithm 4.The resulting system is shown in Figure 14.
- Sensor-insertion attack: Under sensor insertion, vulnerable sensor events are {a4, b4}, and the attacked closed-loop system reaches unsafe state (3, 3).The attacked system is depicted in Figure 15.
- Sensor-insertion attack: The intrusion detector cannot detect the sensor-insertion attack because an attacked trace has the same projection as a genuine trace, so the system is not SI-safe controllable.The indistinguishable traces are b1b2b3bi4b4a1a2a3 and b1b2b3b4a1a2a3.
10 Conclusion
The conclusion consolidates a framework for modeling, detecting, and mitigating actuator and sensor attacks in supervisory control systems. It characterizes GF-safe controllability and identifies diagnoser- and verifier-based verification procedures, while noting several directions for extension.
- Conclusion: The paper models actuator enablement or disablement and sensor erasure or insertion attacks in supervisory control systems.The attacks are analyzed through a general methodology for AE-, SE-, and SI-attacks.
- Conclusion: The proposed defense detects attacks online and switches to a safe mode that disables all controllable events after detection.This conservative response is intended to prevent damage from attacks.
- Conclusion: AE-safe controllability, SE-safe controllability, and SI-safe controllability are unified as cases of GF-safe controllability.The properties specify when the system can prevent damage under the corresponding attacks.
- Conclusion: Diagnoser or verifier automata provide algorithmic procedures for testing safe controllability, including a generalized diagnoser-based procedure for GF-safe controllability.The conclusion specifically reports algorithms for AE-safe controllability and their generalization.
- Conclusion: Future work includes combinations of attacks, different attacker information structures, and response modes beyond disabling all controllable events.The paper notes that allowing damage prevention without disabling every controllable event can be formulated as a supervisory control problem for a modified specification.
B Proof of Proposition 1
The proof establishes Proposition 1 by relating diagnoser-state conditions and uncontrollable transitions to the two clauses defining safe controllability. It shows that violating any relevant condition produces a trace decomposition that violates safe controllability, while the absence of such conditions implies the property.
- Proof of Proposition 1: The proof names the two defining clauses SC1 and SC2 and analyzes them through trace decompositions.The clauses concern the placement of attacked events and controllable events within a decomposition t = t1t2.
- Proof of Proposition 1: An uncontrollable unsafe continuation in the attacked closed-loop system violates SC2 after detection.The proof identifies a continuation in (Euc ∪ Ea,c,v)* that prevents the required controllable-event condition.
- Proof of Proposition 1: An uncertain diagnoser state containing a potentially unsafe plant state yields a trace that violates SC1.The proof constructs a diagnoser trace reaching such a state and extends it to an attacked-system trace.
- Proof of Proposition 1: Conversely, if the three relevant diagnoser and uncontrollable-transition conditions are false, every applicable trace decomposition satisfies both SC1 and SC2.The proof concludes that LM is AE-safe controllable.
- Proof of Proposition 1: A first-entered certain state containing an unsafe plant state yields a trace decomposition that violates SC1 or SC2.The proof uses the occurrence of a vulnerable observable event and forces the second decomposition component to be empty in one case.
C Proof of Proposition 2
The proof of Proposition 2 uses verifier-automaton traces and projections to establish safe controllability by contrapositive. It shows that the absence of unsafe verifier states and forbidden continuations guarantees both safe-controllability clauses.
- Proof of Proposition 2: The proof uses the event sets of the automata in Algorithm 3 to analyze the two safe-controllability clauses.Table C.1 lists the automata event sets used in the proof.
- Proof of Proposition 2: A verifier continuation containing an attacked observable event followed only by uncontrollable events violates SC2.The constructed trace has the form sVσosuc, with σo an attacked observable event and suc uncontrollable events.
- Proof of Proposition 2: A verifier state pairing normal and attack-related behavior with an unsafe state would produce a trace violating SC1.The proof constructs corresponding supervisor and normal-system traces with matching projections.
- Proof of Proposition 2: If the two forbidden verifier conditions do not occur, the antecedent is false or both SC1 and SC2 hold for a decomposition aligned with fault detection.The proof concludes that LM is safe controllable.
D Proof of Proposition 3
The proof establishes Proposition 3 by comparing the closed-loop language of an all-out attacker with that of an attacker that does not attack continuously. Since the latter language is contained in the former, unsafe behavior under the former would contradict its AE-safe controllability.
- Algorithm 1 constructs an automaton H_a for the all-out attacker, whose associated closed-loop language is L_AA = L(H_a) ∩ L(G_a).
- The non-continuous attacker is modeled by an automaton H′_a representable as a state-split subautomaton of H_a.
- Assuming L_AA is AE-safe controllable while L_SA is not yields a string in L_SA that reaches an unsafe state under the stated event and observation conditions.
- Because L_SA ⊆ L_AA, the same unsafe string belongs to L_AA, contradicting AE-safe controllability; therefore, L_SA is AE-safe controllable.