PaperlayerView exact revision on arXiv

Source-linked AI summary

Supervisor Synthesis to Thwart Cyber Attack with Bounded Sensor Reading Alterations

Rong Su

arXiv:1608.04103v2cs.FLcs.CR

TL;DR

Cyber-physical systems can be compromised when attackers alter sensor readings to mislead supervisors into issuing unsafe commands. The paper formulates ABSRA, proves computability of its supremal form for finite-state models, and synthesizes supervisors that detect or contain such attacks.

  • Problem

    The paper addresses sensor-reading deception attacks that can trick a discrete-event-system supervisor into driving a plant toward undesirable states.

  • Method

    It models bounded sensor-reading alterations as ABSRAs and develops attack and supervisor synthesis algorithms using finite-state plant and supervisor models.

  • Results

    The supremal ABSRA exists and is computable under the stated finite-state modeling conditions, and the synthesized supervisor is ABSRA-robust.

  • Takeaways & Limitations

    The synthesized supervisor ensures that an ABSRA is either detectable or cannot lead the system to a bad state.

  • Takeaways & Limitations

    Under weaker observability properties such as standard observability, the supremal ABSRA may no longer exist, although ABSRA existence remains decidable and computable.

Abstract

from arXiv · show

One of the major challenges about cyber physical systems is how to prevent cyber attacks to ensure system integrity. There has been a large number of different types of attacks discussed in the modern control and computer science communities. In this paper we aim to investigate one special type of attacks in the discrete-event system framework, where an attacker can arbitrarily alter sensor readings after intercepting them from a target system in order to trick a given supervisor to issue control commands improperly, driving the system to an undesirable state. We first consider the cyber attack problem from an attacker point of view, and formulate an attack with bounded sensor reading alterations (ABSRA) problem. We then show that the supremal (or least restrictive) ABSRA exists and can be synthesized, as long as the plant model and the supervisor model are regular, i.e., representable by finite-state automata. Upon the synthesis of the supremal ABSRA, we present a synthesis algorithm, which ensures that a computed supervisor will be ABSRA-robust , i.e., either an ABSRA will be detectable or will not lead the system to an undesirable state.

I. INTRODUCTION

The paper studies bounded sensor-reading alterations in discrete-event systems, where attackers manipulate observations to mislead supervisors and drive plants toward undesirable states. It formulates ABSRA and develops synthesis results for attacks and ABSRA-robust supervisors.

  • Cyber attacks can tamper with data collection and interfere with safety-critical decisions in networked cyber-physical systems.
  • ABSRA models attackers that intercept observable sensor measurements and alter each observation sequence within a bounded length.
  • The attacker uses altered observations and prior knowledge of the supervisor to covertly guide the plant toward undesirable states without changing the supervisor.
  • The supremal, or least restrictive, ABSRA exists and is computable when the plant and supervisor are finitely representable.
  • A synthesized supervisor is ABSRA-robust by ensuring attacks are either revealed through abnormal executions or unable to inflict damage.
  • Unlike adaptive approaches that rely on real-time diagnosis, the proposed method embeds attack-robustness features using prior attack-model knowledge.

II. AN ABSRA PROBLEM

This section introduces ABSRA within the supervisory-control framework and states that its supremal form is computable for regular plant and supervisor models.

  • The section recalls supervisory-control concepts before formulating the ABSRA synthesis problem.
  • The ABSRA synthesis algorithm shows that the supremal ABSRA is computable when both the plant model and supervisor are regular.
  • Regularity means that the plant model and given supervisor are finitely representable.

A. Preliminaries on supervisory control

The preliminaries define finite-state plant models, event observability and controllability, supervisory maps, and legality conditions that prevent bad marker states.

  • A target plant is modeled as a deterministic finite-state automaton with states, events, transitions, an initial state, and marker states.
  • Plant behavior is represented by closed and marked languages, with nonblocking behavior defined when the two languages coincide.
  • Marker states are partitioned into desirable and bad states, distinguishing acceptable terminal outcomes from forbidden ones.
  • Under partial observation, a feasible supervisor cannot disable uncontrollable events and must apply identical control patterns to observationally indistinguishable strings.
  • A finitely representable supervisor is an automaton whose closed-loop behavior matches the supervised plant behavior.
  • The assumed legal supervisor ensures that the supervised plant never reaches a bad marker state.

B. A sensor attack model

The paper models sensor attacks as finite-state transducers that intercept observable plant events, replace them with bounded observable strings, and send altered readings to a known supervisor. It then composes the attack with the supervisor and plant to characterize attack effects, canonicalize attacks, and illustrate the construction on a single-tank system.

  • Attack model: An attacker intercepts observable plant events and replaces each with an observable string whose inserted length is bounded by a natural number n.The attack model permits arbitrary sensor-reading alterations subject to a bound on the length of inserted observable sequences.
  • Attack-supervisor composition: Sequential composition A ◦S represents the attacker-supervisor combination that receives plant events, emits altered readings, and generates supervisor control commands.Undefined supervisor transitions lead to a dump state, whose incoming transitions may reveal the attack and should be avoided by an intelligent attacker.
  • Attack model: The attack transducer maps plant events to sensor outputs, while unobservable events self-loop with empty output because the attacker cannot observe them.The transducer uses input and output maps to project event-output pairs onto plant-event and sensor-output strings.
  • Closed-loop impact: The closed-loop impact of an attack is modeled by composing the plant G with A ◦S, yielding G × (A ◦S) over plant events and sensor outputs.The composed system tracks plant and attack-supervisor states and includes the dump state when the attack-supervisor transition is undefined.
  • Canonical attacks: Every attack has a canonical attack with the same effect, obtained as Prefix(G × (A ◦S)); canonical attacks are easier to compute but may be structurally more complex.The canonical model is restricted to plant-consistent behavior, while simplifying the attack model from a canonical one remains an open future-work problem.
  • Single-tank illustration: In the single-tank example, changing medium, high, and extremely high water-level events to low can trick the supervisor and allow the tank to reach the extremely high level.The supervisor opens the valve only at high water level, whereas the attack always reports low, making the system appear safe to the supervisor.

C. An ABSRA model

The ABSRA model formalizes bounded sensor-reading alterations that can fool a supervisor while preserving the supervisor’s event enablement. The supremal ABSRA exists as a regular, computable attack language.

  • ABSRA properties: An ABSRA alters observable events covertly and can cause the plant to reach a bad state or potentially reach one.The model considers sensor attacks rather than actuator attacks, so the attack does not change supervisor event enablement.
  • ABSRA properties: An ABSRA is a nonempty attack model satisfying four specified properties for plant G and supervisor S.These properties include covert insertions, damage potential, and preservation of supervisor enablement under sensor-only attacks.
  • ABSRA construction: Sequential composition with the supervisor can satisfy the ABSRA properties even when the attack model alone violates one property.The canonical attack Prefix(G × (A ◦S)) is then also an ABSRA.
  • Existence: The union of any collection of ABSRAs satisfies the four defining properties, establishing that the least restrictive attack language exists.The theorem applies even to a possibly infinite collection of ABSRAs.
  • Existence: The union theorem alone does not show that the supremal language is regular or recognizable by a finite-state transducer.The paper therefore formulates the problem of designing an ABSRA and subsequently shows regularity and computability.

III. SYNTHESIS OF AN ABSRA

The synthesis framework represents plants and attacks with finite-state structures and uses controllability and normality under observation. Because attack alterations are controllable, the attack synthesis does not explicitly require controllability, while ABSRA properties retain plant-side controllability constraints.

  • Framework: The framework permits finite-state automata or transducers over a general alphabet with designated uncontrollable and observable subalphabets.For product alphabets, observability is defined through the corresponding natural projection.
  • Controllability and normality: A sublanguage qualifies for the synthesis collection when it is controllable with respect to the plant and normal with respect to observation.The supremal controllable and normal sublanguage exists for regular requirements.
  • Attack modeling: Since the attacker can choose any observable alteration or omit it, every attack event is treated as controllable and the attack uncontrollable alphabet is empty.The synthesis therefore does not explicitly require controllability for attack events.
  • Attack modeling: ABSRA Property (4) implicitly enforces controllability with respect to the plant’s uncontrollable events by preserving supervisor enablement.The supervisor already ensures controllability with respect to the plant’s uncontrollable alphabet.
  • Protected observations: The framework can designate protected observable events that an ABSRA cannot alter, and it then initiates the ABSRA synthesis procedure.For protected events, the attack output must equal the original event.

Procedure 1: (ABSRA Synthesis )

Procedure 1 iteratively constructs an attack model using the plant, supervisor, protected observations, and bad-state requirement. The procedure terminates finitely and returns the supremal ABSRA.

  • Inputs and initialization: Procedure 1 takes a plant, supervisor, and protected observable alphabet as input, initializes an attack model, and defines a bad-state requirement.The requirement selects marked strings whose plant state belongs to the bad marked-state set.
  • Iteration: The procedure iterates over candidate languages, checks ABSRA Property (4), and outputs A∗ when the iteration completes.The output attack recognizes the language Kk+1.
  • Termination: The transducer state sets form a monotonic non-increasing sequence under set inclusion, so a fixed sub-transducer is reached after finitely many iterations.This establishes finite termination of Procedure 1.
  • Correctness: Theorem 2 states that the attack A∗ obtained by Procedure 1 is the supremal ABSRA of (G, S).The proof first establishes that A∗ satisfies the ABSRA properties and then shows every other ABSRA language is contained in L(A∗).
  • Illustration: In the illustrative case where all events are observable, A∗ can be chosen as Prefix(G × (A0 ◦S)) and is a canonical attack.Theorem 2 identifies this constructed attack as the supremal ABSRA.
  • Illustration: The example concludes that L(A∗)=K∗ and that A∗ is the supremal ABSRA for the illustrated plant and supervisor.Figure 7 represents the transducer recognizing K∗, with the bad marker state determined by the requirement.

IV. SYNTHESIS OF AN ABSRA-ROBUST SUPERVISOR

The paper synthesizes a supervisor by protecting selected observable events from alteration. The resulting supervisor is ABSRA-robust: attacks are either detectable or do not damage the system.

  • Robustness guarantee: The proposed supervisor is robust in the sense that an ABSRA is either not covert or incurs no damage to the system.This is the stated robustness objective of the supervisor synthesis approach.
  • Protection rationale: Protecting observable events can deter ABSRAs because unnoticeable alteration of those events is prevented.An observable event represents a specific set of strongly associated measurements.
  • Practical trade-offs: Adding sensors or secure transmission can make event alteration harder, but these protections introduce financial considerations.The paper therefore identifies selective protection of critical observable events as an attractive industrial solution.
  • Practical trade-offs: Protecting only critical observable events can yield a supervisor robust to any ABSRA.The protected events are those whose external alteration would otherwise matter to system safety.
  • Problem formulation: The robust-supervisor problem is to synthesize S for plant G and requirement E so that the closed loop has no ABSRA.The synthesis also takes a protected observable alphabet as part of the problem specification.

Procedure 2: (ABSRA-Robust Supervisor Synthesis)

Procedure 2 synthesizes a supervisor that is robust to bounded sensor reading alterations by using a protected observable alphabet and checking whether an ABSRA exists. It also seeks a minimum-size protected alphabet when needed.

  • Procedure 2: (ABSRA-Robust Supervisor Synthesis): Procedure 2 takes a plant G, requirement E, and protected observable alphabet Σo,p as inputs, then outputs a recognizer S.The procedure first computes ˆK = supCN(G, E), and terminates if ˆK is empty.
  • Procedure 2: (ABSRA-Robust Supervisor Synthesis): The procedure computes A∗ through Procedure 1 using Kk = supCN(G × (A0 ◦ˆS), Ek).This calculation tests the attack language associated with the synthesized supervisor.
  • Procedure 2: (ABSRA-Robust Supervisor Synthesis): If the synthesized supervisor has a nonempty marked language, Theorem 3 states that no ABSRA exists for the resulting closed-loop system.The condition is expressed as supCN(G × (A0 ◦S), Ek) = ∅, where Ek is defined by Procedure 1.
  • Procedure 2: (ABSRA-Robust Supervisor Synthesis): An ABSRA may nevertheless reveal itself through abnormal executions before reaching its goal, or fail to drive the system to a bad state.The paper notes that contingent actions such as system shutdown are outside its scope.
  • Procedure 2: (ABSRA-Robust Supervisor Synthesis): If the protected alphabet is insufficient, the synthesis problem is to find a minimum-size Σo,p that permits a nonempty ABSRA-robust supervisor.Enumerating all subsets of Σo and applying Procedure 2 yields a terminating brute-force method, exponential in |Σo| and polynomial in the sizes of G and E.
  • Procedure 2: (ABSRA-Robust Supervisor Synthesis): The single-tank example uses Σo,p = {h=H}; the resulting supervisor is ABSRA-robust, and no protected alphabet of size less than 1 can suffice.The constructed product contains no bad marker state in Xb,m.

V. CONCLUSIONS

The paper introduces ABSRA and develops synthesis results for attacks and supervisors under partial observation. It establishes computability under regular plant and supervisor models, while identifying weaker observability as a boundary to supremal existence.

  • V. CONCLUSIONS: The paper introduces ABSRA as a cyber-attack model for supervisory control under partial observation.The conclusions frame ABSRA as the starting point for the subsequent synthesis problems.
  • V. CONCLUSIONS: The supremal ABSRA exists and is computable when the plant G and supervisor S are finitely representable, with regular languages.This provides the existence and computability condition for the least restrictive attack.
  • V. CONCLUSIONS: The paper formulates synthesis of an ABSRA-robust supervisor and shows that a minimum protected observable sub-alphabet may render such a supervisor possible.The protected sub-alphabet is used in the supervisor synthesis approach aimed at countering ABSRA.
  • V. CONCLUSIONS: Replacing the ABSRA model's third property with standard observability may eliminate the existence of a supremal ABSRA.Existence remains decidable and computable, potentially with higher computational complexity.
Loading 1608.04103v2…