Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthesis of State-Attack Strategies for Anonymity and Opacity Violation in Discrete Event Systems

Xiaoyan Li, Christoforos N. Hadjicostis

TL;DR

The paper studies state-attacks in fully observable discrete-event systems modeled as NFAs to assess current-state anonymity and opacity under a bounded number of attacks. It develops an attack-observer framework comprising system-attack models, a number-attack model, and a game-structure automaton to verify anonymity/opacity violations and to detect attack-enforced violations. It provides necessary and sufficient conditions, complexity bounds, and algorithms for verification and for synthesizing attack-enforced anonymity-violation strategies expressed as Mealy automata. The results enable systematic assessment of security and privacy threats in cyber-physical systems and support proactive defense design by anticipating attacker strategies under resource constraints.

Abstract

Attacks, including the manipulation of sensor readings and the modification of actuator commands, pose a significant challenge to the security and privacy of automated systems. This paper considers discrete event systems that can be modeled with nondeterministic finite state automata that are susceptible to state attacks. A state attack allows an intruder to learn whether or not the current state of a system falls into certain subsets of states. The intruder has a limited total number of state attacks at its disposal, but can launch state attacks at arbitrary instants of its choosing. We are interested on violations of current-state anonymity (resp. opacity), i.e., situations where the intruder, based on the sequence of observations generated by the system and the outcome of any performed state attacks, can ascertain the exact current state of the system (resp. that the current state of the system definitely resides in a subset of secret states). When the system violates current-state anonymity (resp. opacity) under a bounded number of state attacks, a subsequent question is whether the intruder can design an attack strategy such that anonymity-violating (resp. opacity-violating) situations will always be reached. In this latter case, we also design an attack strategy that guarantees that the system will reach a violating situation regardless of system actions. We provide pertinent complexity analysis of the corresponding verification algorithms and examples to illustrate the proposed methods.

Synthesis of State-Attack Strategies for Anonymity and Opacity Violation in Discrete Event Systems

TL;DR

The paper studies state-attacks in fully observable discrete-event systems modeled as NFAs to assess current-state anonymity and opacity under a bounded number of attacks. It develops an attack-observer framework comprising system-attack models, a number-attack model, and a game-structure automaton to verify anonymity/opacity violations and to detect attack-enforced violations. It provides necessary and sufficient conditions, complexity bounds, and algorithms for verification and for synthesizing attack-enforced anonymity-violation strategies expressed as Mealy automata. The results enable systematic assessment of security and privacy threats in cyber-physical systems and support proactive defense design by anticipating attacker strategies under resource constraints.

Abstract

Attacks, including the manipulation of sensor readings and the modification of actuator commands, pose a significant challenge to the security and privacy of automated systems. This paper considers discrete event systems that can be modeled with nondeterministic finite state automata that are susceptible to state attacks. A state attack allows an intruder to learn whether or not the current state of a system falls into certain subsets of states. The intruder has a limited total number of state attacks at its disposal, but can launch state attacks at arbitrary instants of its choosing. We are interested on violations of current-state anonymity (resp. opacity), i.e., situations where the intruder, based on the sequence of observations generated by the system and the outcome of any performed state attacks, can ascertain the exact current state of the system (resp. that the current state of the system definitely resides in a subset of secret states). When the system violates current-state anonymity (resp. opacity) under a bounded number of state attacks, a subsequent question is whether the intruder can design an attack strategy such that anonymity-violating (resp. opacity-violating) situations will always be reached. In this latter case, we also design an attack strategy that guarantees that the system will reach a violating situation regardless of system actions. We provide pertinent complexity analysis of the corresponding verification algorithms and examples to illustrate the proposed methods.
Paper Structure (10 sections, 4 theorems, 17 equations, 12 figures, 5 algorithms)

This paper contains 10 sections, 4 theorems, 17 equations, 12 figures, 5 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Anonymity and opacity under a bounded number of state attacks
  4. Problem setup
  5. Problem formulation
  6. Current-state anonymity (opacity)
  7. Verification of current-state anonymity violation under a bounded number of state attacks
  8. Verification of attack-enforced anonymity violation
  9. Synthesis of an attack-enforced anonymity violation strategy
  10. Conclusions

Key Result

Theorem 1

location_privacy Consider an NFA $G=(X,E,\delta,X_{0})$ with all events being observable and its observer $Obs(G)=(X_{obs}, E, f_{obs}, x_{0,{obs}})$. The system $G$ is current-state anonymous if and only if Given a set of secret states $X_{S}\subset X$, $G$ is current-state opaque if and only if where $X_{NS}=X\setminus X_{S}$ is the set of non-secret states. $\blacksquare$

Figures (12)

  • Figure 1: Fully-observable NFA and its observer.
  • Figure 2: System attack model for the NFA in Fig. \ref{['fig:system']} when $X_{A}=\{2,4\}$.
  • Figure 3: Observer for the NFA in Fig. \ref{['fig:system-attack']}.
  • Figure 4: Number attack model for maximum number of $D\in \mathbb{N}$ state attacks.
  • Figure 5: Game structure between the intruder and the system in the presence of state attacks.
  • ...and 7 more figures

Theorems & Definitions (41)

  • Definition 1
  • Definition 2
  • Definition 3
  • Theorem 1
  • Example 1
  • Definition 4
  • Definition 5
  • Example 2
  • Definition 6
  • Definition 7
  • ...and 31 more