Securing State Estimation Under Sensor and Actuator Attacks: Theory and Design

TL;DR

This paper introduces a new condition called sparse strong observability for secure state estimation in linear systems under arbitrary sensor and actuator attacks, and proposes a scalable estimator based on satisfiability modulo theory solving.

Contribution

It defines sparse strong observability as a necessary and sufficient condition for attack-resilient state reconstruction and develops a novel estimator leveraging satisfiability modulo theory solving.

Findings

The proposed estimator effectively reconstructs states under adversarial attacks.

Sparse strong observability is essential for secure state estimation.

Numerical simulations show the estimator's effectiveness and scalability.

Abstract

This paper discusses the problem of estimating the state of a linear time-invariant system when some of its sensors and actuators are compromised by an adversarial agent. In the model considered in this paper, the malicious agent attacks an input (output) by manipulating its value arbitrarily, i.e., we impose no constraints (statistical or otherwise) on how control commands (sensor measurements) are changed by the adversary. In the first part of this paper, we introduce the notion of sparse strong observability and we show that is a necessary and sufficient condition for correctly reconstructing the state despite the considered attacks. In the second half of this work, we propose an estimator to harness the complexity of this intrinsically combinatorial problem, by leveraging satisfiability modulo theory solving. Numerical simulations demonstrate the effectiveness and scalability of our estimator.

Tables

Table 1. Table 1: Average performance of the proposed observer

	Overall execution time	Number of calls to the SAT solver
${\Phi }_{\text{cert}}^1$	$0.22s$	$20.05$
${\Phi }_{\text{cert}}^2$	$0.21s$	$7.95$

Equations

$$x(t+1)$$

$$y(t)$$

$${\mathcal{O}}_{(A,C)}$$

$${\mathcal{N}}_{(A,B,C,D)}$$

$${\mathbb{Y}}^{\tau }(t)$$

$${\mathbb{U}}^{\tau }(t)$$

$$x(t+1)=Ax(t)+B{u}_S(t),$$

$$y_S(t)=Cx(t)+D{u}_S(t).$$

$$\{\begin{array}{ll}{u}_S(t)& =u(t)+w(t),\\ y(t)& =y_S(t)+a(t),\end{array}$$

$$\mathrm{supp}(\{w^{(i)}(t)\})\subseteq {\Gamma }_u^{(i)},\mathrm{supp}(\{a^{(i)}(t)\})\subseteq {\overline{\Gamma }}_y^{(i)},$$

$$\{\begin{array}{l}{u}_S^{(1)}(t)=u(t)+w^{(1)}(t)\\ u_S^{(2)}(t)=u(t)+w^{(2)}(t)\end{array},$$

$$\mathrm{supp}(\{u_S^{(1)}(t)-u_S^{(2)}(t)\})$$

$$\subseteq {\Gamma }_u^{(1)}\cup {\Gamma }_u^{(2)}.$$

$${\Gamma }_u^{(1)}\cup {\Gamma }_u^{(2)}\subseteq {\Gamma }_u,{\Gamma }_y\subseteq {\Gamma }_y^{(1)}\cap {\Gamma }_y^{(2)}.$$

$$\Delta u(t)$$

$$\Delta y(t)$$

$$\{\begin{array}{ll}\Delta y^{(i)}(t){|}_{{\overline{\Gamma }}_y^{(i)}}& :=\Delta y(t){|}_{{\overline{\Gamma }}^{(i)}}\\ \Delta y^{(i)}(t){|}_{{\Gamma }_y^{(i)}}& :=0\end{array},\text{for}i\in \{1,2\}.$$

$$\{\begin{array}{ll}{u}_S^{(1)}(t)& =\Delta u(t)\\ y_S^{(1)}(t)& =\Delta y(t)\end{array},\{\begin{array}{ll}{u}_S^{(2)}(t)& =0\\ y_S^{(2)}(t)& =0\end{array}$$

$$\{\begin{array}{ll}{x}^{(1)}(0)& =\Delta x\\ x^{(2)}(0)& =0\end{array},$$

$$\{\begin{array}{ll}{w}^{(1)}(t)& =\Delta u^{(1)}(t)\\ a^{(1)}(t)& =-\Delta y^{(1)}(t)\end{array},\{\begin{array}{ll}{w}^{(2)}(t)& =-\Delta u^{(2)}(t)\\ a^{(2)}(t)& =\Delta y^{(2)}(t)\end{array}.$$

$$\mathbb{Y}{|}_{{\Gamma }_y}(t)={\mathcal{O}}_{{\Gamma }_y}\hat{x}+{\mathcal{N}}_{{\Gamma }_u\to {\Gamma }_y}\hat{\mathbb{U}}.$$

$$\mathbb{Y}{|}_{{\Gamma }_y\cap {\Gamma }_y^{\ast }}=$$

$$+$$

$$\mathbb{Y}{|}_{{\Gamma }_y\cap {\Gamma }_y^{\ast }}=O_{{\Gamma }_y\cap {\Gamma }_y^{\ast }}\hat{x}+{\mathcal{N}}_{{\Gamma }_u\to {\Gamma }_y\cap {\Gamma }_y^{\ast }}\hat{\mathbb{U}}+{\mathcal{N}}_{{\Gamma }_u^{\ast }\setminus {\Gamma }_u\to {\Gamma }_y\cap {\Gamma }_y^{\ast }}0,$$

$$\underset{\hat{\mathbb{U}},\hat{x}}{\min }\Vert \mathbb{Y}{|}_{{\Gamma }_y}-{\mathcal{O}}_{{\Gamma }_y}\hat{x}-{\mathcal{N}}_{{\Gamma }_u\to {\Gamma }_y}\hat{\mathbb{U}}\Vert \le ϵ,$$

$${\Phi }_B:=(\sum _{i=1}^m{\mathbf{b}}_i\le r)\bigwedge (\sum _{j=1}^p{\mathbf{c}}_i\le s).$$

$${\Phi }_{\text{naive-cert}}:=\sum _{i\in \overline{\text{supp}(b)}}{\text{b}}_i+\sum _{j\in \overline{\text{supp}(c)}}{\text{c}}_j\ge 1.$$

$${\text{slack}}_u(j):=$$

$$\Vert {\mathcal{N}}_{j\to {\Gamma }_y^{\text{SAT}}}$$

$${\text{slack}}_y(i):=\Vert \mathbb{Y}{|}_i-{\mathcal{O}}_i\hat{x}-{\mathcal{N}}_{{\Gamma }_u^{\text{SAT}}\to \{i\}}\mathbb{U}\Vert ,i\in {\Gamma }_y^{\text{SAT}}.$$

$$\sum _{i\in {\Gamma }_u^{\text{SAT}}}{\text{slack}}_y(i)=\underset{\hat{\mathbb{U}},\hat{x}}{\min }\Vert \mathbb{Y}{|}_{{\Gamma }_y^{\text{SAT}}}-{\mathcal{O}}_{{\Gamma }_y^{\text{SAT}}}\hat{x}-{\mathcal{N}}_{{\Gamma }_u^{\text{SAT}}\to {\Gamma }_y^{\text{SAT}}}\hat{\mathbb{U}}\Vert .$$

$$\frac{dx}{dt}$$

$$y$$

$$\left[\begin{array}{c}\mathbb{Y}{|}_{{\Gamma }_y^{\text{temp}}}\\ \mathbb{Y}{|}_{{\Gamma }_y^1}\end{array}\right]$$

$$\left[\begin{array}{c}\mathbb{Y}{|}_{{\Gamma }_y^{\text{temp}}}\\ \mathbb{Y}{|}_{{\Gamma }_y^2}\end{array}\right]$$

Full text

††thanks: This paper was not presented at any IFAC meeting. Corresponding author M. Showkatbakhsh Tel. +213 364-8655.

, , ,

1 Introduction

Cyber-Physical Systems (CPS) are characterized by the tight interconnection of cyber and physical components. CPS are not only prone to actuator and sensor failures but also to adversarial attacks on the control and sensing modules. Security of CPS is no longer restricted to the cyber domain, and recent incidents such as the StuxNet malware [20] and the security flaws reported on modern cars [13, 19] motivated the recent interest in security of CPS, (see for example, [6, 41, 1, 26] and references therein). During the last decade, a number of security problems have been tackled by the control community, e.g., denial-of-service [45, 8, 34, 14], replay attacks [27], man-in-the-middle attacks [40], false data injection [25], etc.

This paper addresses the problem of state estimation when several sensors and actuators are under attack. We broadly refer to state estimation in the adversarial environment as secure state estimation. Our attack model is quite general and we impose no constraints on the magnitude, statistical properties, or temporal characteristics of the signals manipulated by the adversary.

Secure state estimation has gained the attention of the control community over the past decade [12]. In one line of work, the problem of state estimation and control under sensor attacks is investigated and the authors derived necessary and sufficient conditions under which estimation and stabilization are possible [11]. Shoukry et. al. [36] further refined this condition and called it sparse observability. Chong et. al. [7] found an equivalent condition for continuous-time systems and called it observability under attack. Nakahira et. a. [29] investigated a similar problem while considering the asymptotic correctness of state estimation. The authors relaxed the sparse observability condition to sparse detectability and showed it is a necessary and sufficient condition for asymptotic correctness. The noisy version of this problem has been investigated in the literature [3, 2, 24, 28, 23]. Mishra et. al. [23] derived the optimal solution for Gaussian noise. In this paper, we solve the more general problem of actuator and sensor attacks that includes, as a special case, sensors attacks.

Under the sparse attack model in which an adversary can only target a bounded number of actuators and sensors, state estimation is intrinsically a combinatorial problem. Shoukry et. al. [35] proposed a novel secure state estimator using the Satisfiability Modulo Theory (SMT) paradigm, called Imhotep-SMT. The authors only considered attacks on sensors. In this paper we address the more general problem of sensor and actuator attacks and build an SMT-based estimator that can correctly reconstruct the state under both types of attacks.

In another line of work, the problem of secure state estimation has been studied when the exact model of the system is not available [43, 30]. Tiwari et. al. [42] proposed an online learning method by building so-called safety envelopes as it receives attack-free data to detect abnormality in the data when the system is prone to attacks. In [39, 38] the authors considered system identification under sensors attacks. In all of these works, the adversarial agent is restricted to only attacking sensors.

Pasqualetti et. al. [31] investigated the problem of attack detection and identification. The authors related the undetectable and unidentifiable attacks to the zero-dynamics of the underlying system. The proposed attack identification mechanism consists of a number of fault-monitor filters that provide formal guarantees for the existence of the attack. The number of filters, however, grows exponentially with the number of attacked sensors/actuators, and therefore hinders scalability. In another work [33], the authors investigated detectibility and identifiability of attacks in the presence of disturbances and the concept of security index is generalized to dynamical systems. The proposed method is inherently combinatorial and does not scale well with the number of attacked sensors and actuators. In this paper, by leveraging the SMT paradigm, we design a state estimator that scales well with the number of sensors and actuators.

Fault isolation and fault detection filters are classical control topics closely related to secure state estimation. The traditional fault tolerant filters can detect faults on actuators and sensors, however, they are not adequate for the purpose of security. Some of these filters assume a priori knowledge (statistical or temporal) of the fault signals [5], an assumption that does not hold in the security framework. The classical fault detection filters [17] do not guarantee identification of all possible adversarial signals and zero-dynamics attacks remain stealthy. As an alternative approach, robustification has been used in order to estimate the state despite sparse attacks by either deploying Kalman filters or principle component analysis [22, 10]. The main drawback of these methods is the absence of formal guarantees for the correctness of the state. In contrast, the method proposed in this paper is guaranteed to construct the state correctly in spite of attacks on sensors and/or actuators if the number of attacked components is below a specified threshold that depends on the system. In a recent work [15], Harirchi et. al. proposed a novel fault detection approach using techniques from model invalidation. The authors pursued a worst-case scenario approach and therefore their framework is suitable for security. However, necessary and sufficient conditions for state estimation in a general adversarial setting were not investigated in [15]. In this paper, we precisely characterize the class of systems, by providing necessary and sufficient conditions, for which state reconstruction is possible despite sensor and/or actuator attacks.

The contributions of this paper can be summarized as follows:

• •

We introduce the notion of sparse strong observability by drawing inspiration from sparse observability [11, 36] and the classical notion of strong observablity [16]. We show this is the relevant property when the adversarial agent not only compromises sensor measurements but can also attack inputs.

• •

We develop an observer by leveraging the SMT approach to harness the exponential complexity of the problem. Our observer consists of two blocks interacting iteratively until the true state is found (see Section 4 for a detailed explanation of the observer’s architecture).

• •

We propose two methods to further decrease the running time of the proposed algorithm by reducing the number of iterations of the observer. The first method exploits heuristics that can be efficiently computed at each iteration. The second method is inspired by the QuickXplain algorithm [18] that efficiently finds an irreducibly inconsistent set (see Section 4 for a detailed discussion on the aforementioned methods). We demonstrate the scalability of our proposed observer by several numerical simulations.

A preliminary version of some of the results in this paper were presented in [37] where we introduced the notion of sparse strong observability and drew the connection to secure state estimation. However, the formal proofs were not provided due to space limitations. Furthermore, we propose a new observer that outperforms the observer introduced in [37]. This paper is organized as follows. Section 2 introduces notation followed by the attack model and the precise problem formulation. In Section 3, we introduce the notion of sparse strong observability and relate this notion to the problem of state reconstruction when some of the inputs and outputs are under adversarial attacks. This section concludes with the main theoretical contribution of this paper that is Theorem 8. Section 4 is devoted to designing an observer by exploiting the SMT paradigm. Section 5 provides the simulation results followed by Section 6 that concludes the paper.

2 Problem Definition

2.1 Notation

We denote the sets of real, natural and binary numbers by $\mathbb{R}$, $\mathbb{N}$ and $\mathbb{B}$. We represent vectors and real numbers by lowercase letters, such as $u$, $x$, $y$, and matrices with capital letters, such as $A$. Given a vector $x\in\mathbb{R}^{n}$ and a set $O\subseteq\{1,\ldots,n\}$, we use $x|_{O}$ to denote the vector obtained from $x$ by removing all elements except those indexed by the set $O$. Similarly, for a matrix $C\in\mathbb{R}^{n_{1}\times n_{2}}$ we use $C|_{(O_{1},O_{2})}$ to denote the matrix obtained from $C$ by eliminating all rows and columns except the ones indexed by $O_{1}$ and $O_{2}$, respectively, where $O_{i}\subseteq\{1,\ldots,n_{i}\}$ with $n_{i}\in\mathbb{N}$ for $i\in\{1,2\}$. In order to simplify the notation, we use $C|_{(.,O_{2})}:=C|_{(\{1,\ldots,n_{1}\},O_{2})}$ and $C|_{(O_{1},.)}:=C|_{(O_{1},\{1,\ldots,n_{2}\})}$. We denote the complement of $O$ by $\overline{O}:=\{1,\ldots,n\}\setminus O$. We use the notation $\{x(t)\}_{t=0}^{T-1}$ to denote the sequence $x(0),\ldots,x(T-1)$, and we drop the sub(super)scripts whenever it is clear from the context.

A Linear Time Invariant (LTI) system is described by the following equations:

[TABLE]

where $u(t)\in\mathbb{R}^{m}$, $x(t)\in\mathbb{R}^{n}$ and $y(t)\in\mathbb{R}^{p}$ are the input, state and output variables, respectively, $t\in\mathbb{N}\cup\{0\}$ denotes time, and $A$, $B$, $C$ and $D$ are system matrices with appropriate dimensions. We use $(A,B,C,D)$ to denote the system described by (1). The order of an LTI system is defined as the dimension of its state space. A trajectory of the system consists of an input sequence with its corresponding output sequence. For an LTI system,

[TABLE]

are the observability and invertibility matrices, respectively, where $n$ is the order of the underlying system. In this paper, we often work with subsets of inputs and outputs. For a subset of outputs $\Gamma_{y}\subseteq\{1,\ldots,p\}$, we use the notation $\mathcal{O}_{\Gamma_{y}}:=\mathcal{O}_{(A,C|_{(\Gamma_{y},.)})}$ to denote the observability matrix of outputs in the set ${\Gamma_{y}}$. For a set of inputs ${\Gamma_{u}}\subseteq\{1,\ldots,m\}$, we use the notation $\mathcal{N}_{{\Gamma_{u}}\to{\Gamma_{y}}}$ to denote $\mathcal{N}_{(A,B_{(.,{{\Gamma_{u}}})},C_{({\Gamma_{y}},.)},D_{({\Gamma_{y}},{\Gamma_{u}})})}$. For $x\in\mathbb{R}^{n}$, we define its support set as the set of indices of its non-zero components, denoted by $\operatorname{supp}(x)$. Similarity we define the support of the sequence $\{x(t)\}$ as $\operatorname{supp}(\{x(t)\}):=\cap_{t}\operatorname{supp}(x(t))$. The observer proposed in this paper uses batches of inputs and outputs in order to reconstruct the state. We reserve capital bold letters to denote these batches,

[TABLE]

where $\tau\leq n$. Whenever $\tau$ is the order of the underlying system, we may drop the superscript for ease of notation. For a subset of outputs (inputs), denoted by $\Gamma_{y}\subseteq\{1,\ldots,p\}$ ($\Gamma_{u}\subseteq\{1,\ldots,m\}$), we use the notation $\mathbb{Y}^{\tau}|_{\Gamma_{y}}(t)$ ($\mathbb{U}^{\tau}|_{\Gamma_{u}}(t)$) for the batches of length $\tau$ that only consists of outputs (inputs) in the set $\Gamma_{y}$ ($\Gamma_{u}$). For a vector $x\in\mathbb{R}^{n}$, we denote a generic norm, $l_{2}$-norm and $l_{1}$-norm of $x$ by $\|x\|$, $\|x\|_{2}$ and $\|x\|_{1}$.

2.2 System and Attack model

This work is concerned with the problem of state reconstruction of LTI systems. We consider the scenario in which sensors and actuators are both prone to adversarial attacks. The ultimate goal is to reconstruct the state despite these attacks. In this part, we define the attack model and conclude this section with the precise problem statement. The system $S$, is described by the following equations:

[TABLE]

Without loss of generality we assume $\begin{bmatrix}B^{T}&D^{T}\end{bmatrix}^{T}$ to be of full column rank.

Each actuator (sensor) corresponds to one input (output) and we use input (output) instead of actuator (sensor) in the rest of this paper. In this set up the adversary can attack both inputs and outputs. We model these attacks by additive terms and by imposing a sparsity constraint on them,

[TABLE]

where $u(t)\in\mathbb{R}^{m}$ and $y(t)\in\mathbb{R}^{p}$ are the controller-designed input and the observed output, respectively, and $w(t)\in\mathbb{R}^{m}$ and $a(t)\in\mathbb{R}^{p}$ are signals injected by the malicious agent. In the rest of this paper, we refer to these signals $\left(w\left(t\right),a(t)\right)$ as the attack of the adversarial agent. We use the subscript $S$ for signals that directly come from/to the system. The controller can only observe $y(t)$ and compute the input $u(t)$. This generic attack model is depicted in Figure 1.

When the adversary attacks an input (output) it can change its value to any arbitrary number without explicitly revealing its presence. The only limitation that we impose on the power of the malicious agent is the maximal number of inputs and outputs that can be attacked.

Assumption 1** (Bound on the number of attacks).**

The number of inputs and outputs under attack are bounded by $r$ and $s$, respectively.

Therefore, the malicious agent can attack a subset of inputs and outputs denoted by $\Gamma_{u}\subseteq\{1,\ldots,m\}$ and $\overline{\Gamma}_{y}\subseteq\{1,\ldots,p\}$,111For ease of exposition, we use $\Gamma_{u}$ to denote under-attack inputs while using $\Gamma_{y}$ for the set of attack-free outputs, i.e., the set of under-attack outputs is represented by $\overline{\Gamma}_{y}:=|\{1,\ldots,p\}\setminus\Gamma_{y}$ in this paper. respectively, with $|\Gamma_{u}|\leq r$ and $|\overline{\Gamma}_{y}|\leq s$, such that $\operatorname{supp}(\{w(t)\})\subseteq\Gamma_{u}$ and $\operatorname{supp}(\{a(t)\})\subseteq\overline{\Gamma}_{y}$. Note that these sets are not known to the controller and only upper bounds on their cardinality are given. Once the adversary chooses these sets, inputs and outputs outside these sets remain attack-free. This assumption is realistic when the time it takes for the adversarial agent to attack new inputs and outputs is large compared to the time scale of the system.

We now precisely define the main problem we tackle in this paper.

Problem 2** (Secure state estimation).**

For the linear system defined by (6) under the attack model defined by (7), what are necessary and sufficient conditions under which the state of the compromised system (6) can be reconstructed with bounded delay?

It is well-known that the secure state estimation problem, when only outputs are under adversarial attacks, is combinatorial and belongs to the class of NP-hard problems [35, 31]. Therefore we are motivated to design an observer that harness the complexity of this problem.

Problem 3** (Secure observer design).**

Assumming conditions in Problem 2 are satsified, how can we design an observer that reconstructs the state of the compromised system?

3 Conditions for Secure State Estimation

In this section, we solve Problem 2, i.e., we provide conditions on the system described by (6) under which state reconstruction (with bounded delay) is possible. We first develop the notion of sparse strong observability. This section concludes with Theorem 8 that relates this notion to the solution of Problem 2.

In the absence of attacks, the problem of estimating the state of a system while some of the inputs are unknown has been studied and the notion of strong observability was introduced in the literature [16]. For strongly observable systems, it is possible to estimate the state of the system without the knowledge of inputs. The following definition formalizes this concept.

Definition 4** (Strong observability).**

An LTI system is called strongly observable if for any initial state $x(0)\in\mathbb{R}^{n}$ and any input sequence $\{u(t)\in\mathbb{R}^{m}\}_{t=0}^{\infty}$ there exists an integer $\tau\in\mathbb{N}\cup\{0\}$ such that $x(0)$ can be uniquely recovered from $\{y(t)\}_{t=0}^{\tau}$.

Note that $\tau$ is always upper-bounded by the order of the system. Linearity implies the following lemma.

Lemma 5**.**

An LTI system is strongly observable if and only if $y(t)=0$ $\forall t\in\mathbb{N}\cup\{0\}$ implies that $x(0)=0$.

{pf}

Please refer to Appendix.

It is straightforward to conclude the following corollary.

Corollary 6**.**

An LTI system is not strongly observable if and only if there exist a non-zero intial state and an input sequence such that $y(t)=0$ for $t\in\mathbb{N}\cup\{0\}$.

{pf}

Follows directly from Lemma 5.

It is well-understood that when the adversary is restricted to attacking outputs, state reconstruction is possible only if there is enough redundancy in the outputs of the system. This redundancy can be stated in terms of observability of the system while removing a number of outputs. This property has been formalized in [11] and is called sparse observability [36]. By analogy with sparse observability, we define the notion of $(r,s)$-sparse strong observability as follows:

Definition 7** ($(r,s)$-sparse strong observability).**

An LTI system $(A,B,C,D)$ with $m$ inputs and $p$ outputs is $(r,s)$-sparse strongly observable if for any $\Gamma_{u}\subseteq\{1,\ldots,m\}$ and ${\Gamma}_{y}\subseteq\{1,\ldots,p\}$ with $|\Gamma_{u}|\leq r$ and $|{\Gamma}_{y}|\geq p-s$, the system $(A,B_{(.,{\Gamma_{u}})},C_{(\Gamma_{y},.)},D_{(\Gamma_{y},\Gamma_{u})})$ is strongly observable.

Note that in Definition 7, the value of $r$ and $s$ are upper bounded by the number of inputs and outputs, respectively. This modified notion of strong observability is the key for formalizing redundancy across inputs and outputs. We show that a necessary and sufficient condition for secure state estimation can be stated using this property. Note that $(0,s)$-sparse strong observability is equivalent to the notion of $s$-sparse observability that was introduced before in the literature [11, 36, 23]. The following theorem is the main theoretical result in this paper.

Theorem 8**.**

Let the number of attacked inputs and outputs be bounded by $r$ and $s$, respectively. Under the attack model (7), the state can be reconstructed (possibly with delay) if and only if the underlying system is $(2r,2s)$-sparse strongly observable.

Remark 9**.**

It is worth mentioning that the maximum number of attacked outputs, $s$, cannot be greater than $\left\lfloor{\frac{p}{2}}\right\rfloor$ and it is an inherent limitation of LTI systems with $p$ outputs [11]. However the maximum number of attacked inputs is not inherently restricted by $\left\lfloor{\frac{m}{2}}\right\rfloor$ and can take values up to $m$, depending on the specific system under the consideration.

Remark 10**.**

*Pasqualetti et. al. [31] addressed the problem of attack detection and identification in the presence of adversarial inputs and outputs for continuous-time LTI systems. They showed that attack identification is possible if and if for any $\Gamma_{u}\subseteq\{1,\ldots,m\}$ and ${\Gamma}_{y}\subseteq\{1,\ldots,p\}$ with $|\Gamma_{u}|\leq 2r$ and $|{\Gamma}_{y}|\geq p-2s$, the system $(A,B_{(.,{\Gamma_{u}})},C_{(\Gamma_{y},.)},D_{(\Gamma_{y},\Gamma_{u})})$ does not have any invariant zeros.

It is clear that from the state and the dynamics of the system, the attack can be identified, therefore the attack identification comes free with the solution to the secure estimation problem. Strongly observable LTI systems do not have any invariant zeros (see, for example Theorem 1.8 in [16]). Therefore this theorem shows that under this sparse-attack model, the conditions for identifying the attack also enable one to reconstruct the state, i.e., characterizations of attack identifiability and secure state estimation are equivalent for LTI systems. Putting these together, secure state estimation also comes with the solution to the attack identification problem. However, we provide a direct proof that does not require this machinery.*

{pf}

First we show that $(2r,2s)$-sparse strong observability is a sufficient condition for correctly estimating the state. For the sake of the contradiction, assume that the state cannot be reconstructed, i.e., there exist two different (initial) states, denoted by $x^{(1)}$ and $x^{(2)}$, that cannot be distinguished under this attack model. More precisely, there exist two attack strategies that will lead to the same exact (observed) trajectories. We reserve superscripts $.^{(1)}$ and $.^{(2)}$ for variables across those scenarios. Let us denote the adversarial additive terms by $\{w^{(1)}(t)\},\{a^{(1)}(t)\}$ and $\{w^{(2)}(t)\},\{a^{(2)}(t)\}$. We represent the corresponding inputs and outputs of the system by $\{u^{(1)}_{S}(t)\},\{y^{(1)}_{S}(t)\}$ and $\{u^{(2)}_{S}(t)\},\{y^{(2)}_{S}(t)\}$, and the common (corrupted) measured output and the controller input sequences are denoted by $\{y(t)\}$ and $\{u(t)\}$, respectively.

By the assumption of the attack model (7), there exist $\Gamma_{u}^{(i)},\overline{\Gamma}_{y}^{(i)}$ for $i\in\{1,2\}$ with bounded cardinality such that

[TABLE]

for $i\in\{1,2\}$. Note that

[TABLE]

where $u(t)$ is the controller designed input. Therefore

[TABLE]

Similarly, it is straightforward to conclude that $\operatorname{supp}(\{y^{(1)}_{S}(t)-y^{(2)}_{S}(t)\})\subseteq\overline{\Gamma}^{(1)}_{y}\cup\overline{\Gamma}^{(2)}_{y}$. We are ready to reach the contradiction. The underlying system is LTI, thus the input sequence $\{u^{(1)}_{S}(t)-u^{(2)}_{S}(t)\}$ with the initial state $x^{(1)}-x^{(2)}$ generates the output sequence $\{y^{(1)}_{S}(t)-y^{(2)}_{S}(t)\}$. The underlying system is $(2r,2s)$-sparse strongly observable so the sub-system $(A,B_{(.,{\Gamma_{u}})},C_{(\Gamma_{y},.)},D_{(\Gamma_{y},\Gamma_{u})})$ is strongly observable for any $|\Gamma_{u}|=2r$ and $|{\Gamma}_{y}|=p-2s$. Let us choose $\Gamma_{u}$ and ${\Gamma}_{y}$ as any set of $2r$ inputs and $p-2s$ outputs such that,

[TABLE]

Note that $\{y^{(1)}_{S}(t)|_{{\Gamma}_{y}}-y^{(2)}_{S}(t)|_{{\Gamma}_{y}}\}$ is a zero sequence, hence by Lemma 5 we conclude that the corresponding initial state ($x^{(1)}-x^{(2)}$) is zero, which contradicts the assumption of $x^{(1)}\neq x^{(2)}$. Now we prove that $(2r,2s)$-sparse strongly observability is a necessary condition. For the sake of contradiction, suppose that the system described by (6) is not $(2r,2s)$-sparse strongly observable, however, reconstructing the state (possibly with delays) is still possible. We construct two system trajectories with different (initial) states that have exactly the same input and output sequences under suitable attack strategies (additive terms). This implies that estimating the correct state is indeed impossible thereby establishing the desired contradiction.

By the assumption of the contradiction, the underlying system is not $(2r,2s)$-sparse strongly observable, so there exist subsets of inputs and outputs denoted by $\Gamma_{u}$ with $|\Gamma_{u}|=2r$ and $\Gamma_{y}$ with $|\Gamma_{y}|=p-2s$, respectively, such that $(A,B_{(.,{\Gamma_{u}})},C_{({\Gamma_{y}},.)},D_{({\Gamma_{y}},\Gamma_{u})})$ is not strongly observable. Corollary 6 implies that there exist an initial condition $\Delta x$ and an input sequence $\{\Delta u(t)\}$ (with its support lying inside $\Gamma_{u}$) that generates an output sequence $\{\Delta y(t)\}$ with $\operatorname{supp}(\{\Delta y(t)\})\subseteq\overline{\Gamma}_{y}$. One can rewrite $\Delta u(t)$ and $\Delta y(t)$ as sum of two sparse signals, more precisely:

[TABLE]

where cardinality of $\operatorname{supp}(\{\Delta u^{(i)}(t)\})$ and $\operatorname{supp}(\{\Delta y^{(i)}(t)\})$ are upper-bounded by $r$ and $s$ for $i\in\{1,2\}$, respectively. For example, we can rewrite $\overline{\Gamma}_{y}=\overline{\Gamma}^{(1)}_{y}\cup\overline{\Gamma}^{(2)}_{y}$ where $|\overline{\Gamma}^{(i)}_{y}|\leq s$ for $i\in\{1,2\}$. Then we define

[TABLE]

Now consider the following two different trajectories of the system

[TABLE]

with their initial states

[TABLE]

and their corresponding attack strategies,

[TABLE]

It is straightforward to verify that $\{y^{(1)}(t)\}=\{y^{(2)}(t)\}$ and $\{u^{(1)}(t)\}=\{u^{(2)}(t)\}$, i.e., under the attack model (7) the controlled inputs and the observed outputs are exactly the same for both trajectories while having different states, therefore the proof is complete.

4 Secure Observer Design

In this section, we seek solutions to Problem 3. In the first part, we explain the intuition behind the proposed algorithm that estimates the state despite attacks on inputs and outputs. We give formal guarantees that the algorithm reconstructs the state correctly. In the second part, we introduce the observer by leveraging the SMT paradigm followed by two methods that enhance the run time of state estimation.

Based on the attack model (7), the input to the system is decomposed into two additive terms, the controller-designed input $u(t)$ and the adversarial input $w(t)$. The underlying system (6) is linear and therefore we can easily exclude the effect of the controller-designed input from the output by subtracting its effect. Hence, without loss of generality we assume that the true $u(t)$ is zero.

The proposed algorithm is based on the following proposition.

Proposition 11**.**

Suppose the underlying system is $(2r,2s)$-sparse strongly observable, and the number of attacked inputs and outputs are bounded by $r$ and $s$, respectively. Given any subset of inputs and outputs denoted by ${\Gamma}_{u}$ and ${\Gamma}_{y}$ with $|{\Gamma}_{u}|\leq r$ and $|{\Gamma}_{y}|\geq p-s$, the first statement below implies the second:

There exist $\mathbb{\hat{U}}\in\mathbb{R}^{n|T|}$ and $\hat{x}\in\mathbb{R}^{n}$ such that

[TABLE] 2. 2.

The estimated state $\hat{x}$, is equal to the actual state of the system at time $t-n+1$, $x(t-n+1)$, where $n$ is the order of the underlying system.

Remark 12**.**

The underlying system is $(2r,2s)$-sparse strongly observable therefore $(A,B_{(.,{{\Gamma}_{u}})},C_{({\Gamma}_{y},.)},D_{({\Gamma}_{y},{\Gamma}_{u})})$ is strongly observable. If (17) has a solution, then $\hat{x}$ would be the unique solution for $x$ (see section III-B of [44]).

{pf}

Let us denote the set of attack-free outputs and under-attack inputs by $\Gamma_{y}^{\ast}$ and $\Gamma_{u}^{\ast}$. At most $s$ outputs are under attack, therefore $|{\Gamma}_{y}\cap\Gamma_{y}^{\ast}|\geq p-2s$. Note that $\mathbb{Y}|_{{\Gamma}_{y}\cap\Gamma^{\ast}_{y}}$ can be written as follows:

[TABLE]

On the other hand, we can rewrite (17) by taking only outputs in ${\Gamma}_{y}\cap\Gamma_{y}^{\ast}$,

[TABLE]

where $\mathbb{0}$ is a zero vector with appropriate dimensions. The underlying system is $(2r,2s)$-sparse strongly observable, therefore we conclude that the sub-system $\hat{S}:=(A,B_{(.,{{\Gamma}_{u}\cup\Gamma_{u}^{\ast}})},C_{({\Gamma}_{y}\cap\Gamma_{y}^{\ast},.)},D_{({\Gamma}_{y}\cap\Gamma_{y}^{\ast},{\Gamma}_{u}\cup\Gamma_{u}^{\ast})})$ is strongly observable. One can reinterpret both equations as two (possibly different) valid trajectories of the system $\hat{S}$ that share the same output sequence. Strong observability of $\hat{S}$ implies that $\hat{x}=x(t-n+1)$ which completes the proof.

The main algorithm in this paper builds upon this proposition. We search for a set of inputs and outputs that satisfies equality (17), i.e., we check if there exist $\mathbb{\hat{U}}$ and $\hat{x}$ that make equality (17) hold. Based on Proposition 11, we define a consistency check as follows,

TEST 1** (Consistency Check).**

Given subsets of inputs and outputs denoted by ${\Gamma}_{u}$ and ${\Gamma}_{y}$, TEST$({\Gamma}_{u},{\Gamma}_{y})$ returns true if

[TABLE]

where $\epsilon>0$ is the solver tolerance, due to numerical errors. However, for the sake of clarity, we focus in this paper on the case when $\epsilon$ is negligible222Note that the minimum always exists for (20) as the cost function is a semi-definite quadratic function..

Finding the right subset of inputs and ouputs that satisfies this test is a combinatorial problem in nature and requires exhaustive search. It is well-known that secure state estimation under this attack model is in general NP-hard [35, 31]. This test is depicted in Algorithm 4.1.

In the rest of this section, we introduce an architecture for our observer followed by methods to improve its computational performance. For each input (output), we assign a binary variable $\mathbf{b}_{i}\in\mathbb{B}$ ($\mathbf{c}_{i}\in\mathbb{B}$) that indicates if the corresponding input (output) is under attack or not, i.e., $\mathbf{b}_{i}=1$ ($\mathbf{c}_{i}=1$) if the $i^{\text{th}}$ input (output) is under attack. In the rest of this paper, we use the bold letters ($\mathbf{b}$ and $\mathbf{c}$) to denote these Boolean variables and we reserve non-bold type face ($b$ and $c$) as instances of them. Finding the right assignment of these Boolean variables is combinatorial in nature and in order to efficiently decide which set of inputs and outputs satisfies the TEST in (20), we design an observer using the lazy SMT paradigm [4].

4.1 Overall Architecture

The observer consists of two blocks that interact with each other, a propositional satisfiability (SAT) solver and a theory solver. The former reasons about the combination of Boolean and pseudo-Boolean constraints and produces a feasible instance of $\mathbf{b}\in\mathbb{B}^{m}$ and $\mathbf{c}\in\mathbb{B}^{p}$, based on its current state. The theory solver checks the consistency of Boolean variables using the consistency test, and when the test fails, it encodes the inconsistency as a pseudo-Boolean constraint and returns it to the SAT solver. The general architecture is depicted in Figure 2.

The initial pseudo-Boolean constraint only bounds the number of attacked inputs and outputs, i.e.,

[TABLE]

Initially, the SAT solver generates instances of $\mathbf{b}$ and $\mathbf{c}$ that satisfy $\Phi_{B}$. The theory solver checks whether ${\Gamma_{u}}:={\operatorname{supp}(b)}$ and ${\Gamma_{y}}:=\overline{\operatorname{supp}(c)}$ satisfies the consistency check. If the test is satisfied, then the algorithm terminates and returns the (delayed) estimate of the state. Otherwise, the theory solver outputs UNSAT and generates a reason for the conflict, a certificate, or a counterexample that is denoted by $\Phi_{\text{cert}}$. This counterexample encodes the inconsistency among the chosen inputs and outputs. The following always constitutes a naive certificate.

[TABLE]

On the next iteration, the SAT solver updates the constraint by conjoining $\Phi_{\text{cert}}$ to $\Phi_{B}$, and generates another feasible assignment for $\mathbf{b}$ and $\mathbf{c}$. This procedure is repeated until the theory solver returns SAT as illustrated in Algorithm 4.1.

{algorithm}

[h] Secure state estimator

1:$A,B,C,D$ (system), $Y$ (output), $r,s$ (bounds)

2:status $\leftarrow$ UNSAT

3:$\Phi_{\text{cert}}\leftarrow\text{True}$

4:$\Phi_{B}\leftarrow(\sum\limits_{i\in\{1,\ldots,m\}}\textbf{b}_{i}\leq r)\bigwedge(\sum\limits_{i\in\{1,\ldots,p\}}\textbf{c}_{i}\leq s)$

5:while status $=$ UNSAT do

6:     $\Phi_{B}\leftarrow\Phi_{B}\bigwedge\Phi_{\text{cert}}$

7:     $(b,c)\leftarrow$ SAT-solver($\Phi_{B}$)

8:     (status, x) $\leftarrow$ T-solver.check(${\operatorname{supp}(b)},\overline{\operatorname{supp}(c)}$)

9:     $\Phi_{\text{cert}}\leftarrow$ T-solver.Certificate(${\operatorname{supp}(b)},\overline{\operatorname{supp}(c)}$)

10:return $(x,b,c)$

Note that Proposition 11 implies that the SAT solver eventually produces an assignment that satisfies the consistency test and therefore Algorithm 4.1 always terminates. The size of the certificate plays an important role in the overall execution time of the algorithm [35]. Note that the attack model considered in [35] is restricted to outputs, and the major contribution of our work is to handle both input and output attacks. In the next section, we focus on constructing shorter counterexamples to improve the run time.

{algorithm}

T-solver.check

1:${\Gamma_{u}},{\Gamma_{y}}$

2:Solve: $(\hat{x},\mathbb{\hat{U}})=\text{argmin}_{x,\mathbb{U}}\|\mathbb{Y}|_{{\Gamma_{y}}}-\mathcal{O}_{{\Gamma_{y}}}x-\mathcal{N}_{{\Gamma_{u}}\to{{\Gamma_{y}}}}\mathbb{U}\|$

3:if $\|\mathbb{Y}|_{{\Gamma_{y}}}-\mathcal{O}_{{\Gamma_{y}}}\hat{x}-\mathcal{N}_{{\Gamma_{u}}\to{{\Gamma_{y}}}}\mathbb{\hat{U}}\|\leq\epsilon$ then

4:     status = SAT

5:else

6:     status = UNSAT

7:return $(\text{status},\hat{x})$

4.2 SAT certificate

In this part, we improve the efficiency of Algorithm 4.1 by constructing a shorter certificate (counter-example or conflicts). As it was discussed before, the naive certificate only excludes the current assignment of $\mathbf{b}$ and $\mathbf{c}$ from the search space of the SAT solver, however, by exploiting the structure of the underlying system, we show that we can further decrease the size of the certificate and therefore prune the search space more efficiently.

One of the main results of this paper is to show that we can always find a smaller conflicting subset of inputs and outputs. We propose two methods for generating shorter certificates. The first method reduces the size of the counterexample by at least $s-1$, we explain this method in Lemma 13 and give a formal proof of the existence of such shorter certificate. In practice, however we observe the reduction in the length of conflicts is much larger than this theoretical bound. The second method is inspired by the QuickXplain algorithm. This method generates counter-examples that are irreducible, meaning that we cannot reduce the size of the counter-example by removing some of it’s entries. We also note that by generating multiple certificates at each iteration we can further enhance the execution time. At the end of this section Lemma 15 states that for a generic LTI system the size of the certificate cannot be smaller than $m+1$.

Let us assume that the SAT solver hypothesized $\Gamma_{u}^{\text{SAT}}:={\operatorname{supp}(b)}$ and $\Gamma_{y}^{\text{SAT}}:=\overline{\operatorname{supp}(c)}$ as the set of compromised inputs and safe outputs, respectively. The main intuition behind both methods is to look for $\Gamma_{u}^{\text{cert}}\supseteq\Gamma_{u}^{\text{SAT}}$ and $\Gamma_{y}^{\text{cert}}\subseteq\Gamma_{y}^{\text{SAT}}$ that would not satisfy the consistency test. Note that the certificate consists of inputs in $\overline{\Gamma}_{u}^{\text{cert}}$ and outputs in $\Gamma_{y}^{\text{cert}}$.

4.3 Method I based on heuristics

Method I reduces the size of the certificate by increasing the size of (supposedly under attack) inputs ($\Gamma_{u}^{\text{cert}}$) followed by decreasing the size of (supposedly safe) outputs ($\Gamma_{u}^{\text{cert}}$). The summary of the above procedure of shortening certificates is illustrated in Algorithm 4.3. We begin by adding inputs to $\Gamma_{u}^{\text{SAT}}$ while making sure TEST still returns false and the number of inputs is bounded by $2r$. Let us denote this new set of inputs by $\Gamma_{u}^{\text{cert}}$.

At the second step, we shrink the set of conflicting outputs in order to further shorten the size of the counterexample. Let us denote a subset of $\Gamma_{y}^{\text{SAT}}$ of size $p-2s$ by $\Gamma_{y}^{\text{temp}}$. The following lemma shows we can reduce the size of conflicting outputs at least by $s-1$.

{algorithm}

T-solver.Certificate 1

1:$\Gamma_{u}^{\text{SAT}},\Gamma_{y}^{\text{SAT}}$

2:step 1: Conduct a linear search in the input set

3:Sort $\overline{\Gamma}_{u}^{\text{SAT}}$  

4:$\text{status}\leftarrow\text{UNSAT},j\leftarrow\emptyset,\Gamma_{u}^{\text{cert}}\leftarrow\Gamma_{u}^{\text{SAT}}$  

5:while  status == UNSAT and $|\Gamma_{u}^{\text{cert}}|<2r$  do

6:     $\Gamma_{u}^{\text{cert}}\leftarrow\Gamma_{u}^{\text{cert}}\cup\{j\}$

7:     pick another input $j\in\overline{\Gamma}_{u}^{\text{SAT}}$

8:     $(\text{status},x)\leftarrow$ T-Solver.check$(\Gamma_{u}^{\text{cert}}\cup\{j\},\Gamma_{y}^{\text{SAT}})$

9:step 2: Conduct a linear search in the output set

10:Sort $\Gamma_{y}^{\text{SAT}}$

11:Pick a subset of size $p-2s$: $\Gamma_{y}^{\text{temp}}\subseteq\Gamma_{y}^{\text{SAT}}$

12:$\text{status}\leftarrow\text{SAT},i\leftarrow\emptyset$

13:while  status == SAT  do

14:     $\Gamma_{y}^{\text{cert}}\leftarrow\Gamma_{y}^{\text{temp}}\cup\{i\}$

15:     $(\text{status},x)\leftarrow$ T-Solver.check$(\Gamma_{u}^{\text{cert}},\Gamma_{y}^{\text{cert}})$

16:     Pick another output $i\in\Gamma_{y}^{\text{SAT}}\setminus\Gamma_{y}^{\text{temp}}$

17:$\Phi_{\text{cert}}^{1}\leftarrow\sum\limits_{j\in\overline{\Gamma}_{u}^{\text{cert}}}\mathbf{b}_{j}+\sum\limits_{i\in{\Gamma}_{y}^{\text{cert}}}\mathbf{c}_{i}\geq 1$

18:return $\Phi_{\text{cert}}^{1}$

Lemma 13**.**

Assume that the system $S$ is $(2r,2s)$-sparse strongly observable, and the number of attacked inputs and outputs are bounded by $r$ and $s$, respectively. Pick any subset of inputs and outputs denoted by $\Gamma_{u}^{\text{cert}}$ and $\Gamma_{y}^{\text{SAT}}$ with $|\Gamma_{u}^{\text{cert}}|\leq 2r$ and $|\Gamma_{y}^{\text{SAT}}|\geq p-s$, that do not satisfy the consistency check (20). Given any subset of at most $p-2s$ outputs denoted by $\Gamma_{y}^{\text{temp}}\subseteq\Gamma_{y}^{\text{SAT}}$, one of the following is true:

TEST($\Gamma_{u}^{\text{cert}},\Gamma_{y}^{\text{temp}}$) returns false, 2. 2.

There exists an output $i\in\Gamma_{y}^{\text{SAT}}\setminus\Gamma_{y}^{\text{temp}}$ such that TEST($\Gamma_{u}^{\text{cert}},\Gamma_{y}^{\text{temp}}\cup\{i\}$) returns false.

{pf}

Please refer to Appendix.

We denote this smaller set of conflicting outputs $\Gamma_{y}^{\text{temp}}$(if TEST($\Gamma_{u}^{\text{cert}},\Gamma_{y}^{\text{temp}}$) returns false, otherwise $\Gamma_{y}^{\text{temp}}\cup\{i\}$) by $\Gamma_{y}^{\text{cert}}$. Lemma 13 gives formal guarantees of the existence of shorter certificates which hold no matter how the subsets of inputs and outputs ($\Gamma_{u}^{\text{temp}}$ and $\Gamma_{y}^{\text{temp}}$) are chosen. This lemma shows that Method I reduces the size of the certificate by at least $s-1$.

In practice, we choose these subsets based on heuristics that have for objective a decrease in the overall running time. We assign slack variables to inputs and outputs similarly to [35] and [37], and sort them based on the structure of the system. Recall that Algorithm 4.3 shortens the certificate by reducing the number of inputs followed by the reduction in the number of outputs, i.e., we simultaneously reducing both inputs and outputs in the certificate. We observe that by generating two counterexamples, we can prune the search space of the SAT solver more efficiently. Similarly to Algorithm 4.4, we can find two counterexamples by reducing the number of inputs following a reduction in the number of outputs and vice-verse.

**Sorting $\overline{\Gamma}_{u}^{\text{SAT}}$ and ${\Gamma}_{y}^{\text{SAT}}$:

**Assuming TEST($\Gamma_{u}^{\text{SAT}},\Gamma_{y}^{\text{SAT}}$) returns false, we assign slack variables to inputs in $\overline{\Gamma}_{u}^{\text{SAT}}$ and outputs in $\Gamma_{y}^{\text{SAT}}$, denoted by $\text{slack}_{u}(j)$ and $\text{slack}_{y}(i)$, respectively. Let us denote a solution to the optimization (20) inside TEST($\Gamma_{u}^{\text{SAT}},\Gamma_{y}^{\text{SAT}}$) by $\hat{x}$ and $\hat{\mathbb{U}}$.

We define $\text{slack}_{u}(j)$ for $j\in\overline{\Gamma}_{u}^{\text{SAT}}$ as the norm of the projection of $\mathbb{Y}|_{{\Gamma_{y}^{\text{SAT}}}}-\mathcal{O}_{{\Gamma_{y}^{\text{SAT}}}}\hat{x}-\mathcal{N}_{{\Gamma_{u}^{\text{SAT}}}\to{{\Gamma_{y}^{\text{SAT}}}}}\mathbb{\hat{U}}$ onto the column space of $\mathcal{N}_{j\to{\Gamma}_{y}^{\text{SAT}}}$,

[TABLE]

This slack variable measures how much of the residual can be justified by considering $j$ in addition to ${\Gamma}_{u}^{\text{SAT}}$. Note that we want to append inputs to ${\Gamma}_{u}^{\text{SAT}}$ while having a false TEST. We first normalize these slack variables by the norm of the corresponding invertibility matrix, and $\overline{\Gamma}_{u}^{\text{SAT}}$ is obtained by sorting slack variables in ascending order.

We define $\text{slack}_{y}(i)$ as the residual of each output:

[TABLE]

Note that,

[TABLE]

We first normalize each slack variable by the norm of the corresponding observabality matrix. Recall that we aim to find a smaller subset of $\Gamma_{u}^{\text{SAT}}$ while ensuring TEST returns false. We pick the output with the highest slack variable as the first element of $\Gamma_{u}^{\text{SAT}}$. We sort the rest based on the dimension of the kernel of each observability matrix, following the intuition provided in [35].

4.4 Method II based on QuickXplain

The second method (Algorithm 4.4) is inspired by QuickXplain and generates a counter-example by pruning the naive-certificate (22) to make it irreducible. We formally define this property as follows,

Definition 14** (Irreducible certificate).**

A certificate consisting of inputs $\overline{\Gamma}_{u}$ and outputs $\Gamma_{y}$ is irreducible, if no other subset of it can generate a conflict, i.e., for all subsets denoted by $\overline{\Gamma}^{\prime}_{u}\subseteq\overline{\Gamma}_{u}$ and $\Gamma^{\prime}_{y}\subseteq\Gamma_{y}$ the following are equivalent:

$\overline{\Gamma}^{\prime}_{u}$* and $\Gamma^{\prime}_{y}$ generate a conflict.* 2. 2.

$\overline{\Gamma}^{\prime}_{u}=\overline{\Gamma}_{u}$* and $\Gamma^{\prime}_{y}=\Gamma_{y}$.*

One cannot prune irreducible certificates and each element is necessary for the set to remain a counter-example. Let $\Delta^{\text{SAT}}$ be the elements (consisting of inputs $\overline{\Gamma}_{u}^{\text{SAT}}$ and outputs $\Gamma_{y}^{\text{SAT}}$) of the naive certificate. For ease of exposition we slightly abuse notation to denote $\mbox{TEST}(\Gamma_{u}^{\text{SAT}},\Gamma_{y}^{\text{SAT}})$ by $\mbox{TEST}(\Delta^{\text{SAT}})$. We denote the output of this algorithm by $\Delta_{\text{cert}}$ which consists of inputs $\overline{\Gamma}_{u}^{\text{cert}}$ and outputs $\Gamma_{y}^{\text{cert}}$.

This method consists of an exploration phase in which it finds an element (input or output) that belongs to an irreducible certificate. Let us denote an enumeration of $\Delta^{\text{SAT}}$ by $e_{1},\cdots,e_{k}$, and the internal state by $\Delta_{\text{temp}}\leftarrow\emptyset$. This method begins by adding step-by-step elements of $\Delta^{\text{SAT}}$ to $\Delta_{\text{temp}}$. The first element ($e_{i}\in\Delta^{\text{SAT}}$) that fails TEST$(\Delta_{\text{temp}})$ is part of an irreducible certificate, and therefore is added to $\Delta_{\text{cert}}$.

In order to find further elements of this certificate, we keep $e_{i}$ in the background and the first element that fails the consistency check is added to $\Delta_{\text{cert}}$. This repeated process can be implemented efficiently by using the divide and conquer paradigm as depicted in Algorithm 4.4. When an element $e_{i}$ of $\Delta^{\text{SAT}}$ is detected we divide the the remaining elements into two disjoint subsets $\Delta^{1}:=\{e_{1},\cdots,e_{j}\}$ and $\Delta^{2}:=\{e_{j+1},\cdots,e_{i-1}\}$. We can now recursively apply the algorithm to find a conflict $\Delta_{\text{cert}}^{2}$ among $\Delta^{2}$ by keeping the set $\Delta^{1}$ in the background and a conflict $\Delta_{\text{cert}}^{1}$ among $\Delta^{1}$ by keeping the set $\Delta_{\text{cert}}^{2}$ in the background. This method of finding an irreducible subset is depicted in Algorithm 4.4

Note that the resulting counter-example depends on the initial enumeration of elements in $\Delta^{\text{SAT}}$. If the all the inputs (outputs) are ahead of outputs (inputs), then the resulting counter-example mostly consists of inputs (outputs). In order to have the maximal reduction in the search space of the SAT solver at each iteration, we produce three certificate using this method, putting inputs first, outputs first and mixing both inputs and outputs.

In the last part of this section, we look at the certificate size for a generic LTI system. We observe that the certificate size cannot be smaller that the number of inputs which is stated formally in the following lemma.

{algorithm}

T-solver.QuickXplain

1:$\Delta_{\text{cert}}^{0},\Delta^{0}$

2:if T-solver.check($\Delta_{\text{cert}}^{0}$) = UNSAT or $\Delta^{0}==\emptyset$ then

3:     return $\emptyset$

4:Let $e_{1},\cdots,e_{k}$ be an enumeration of $\Delta^{0}$

5:$i\leftarrow 0$, $\Delta_{\text{temp}}\leftarrow\Delta_{\text{cert}}^{0},$

6:while  T-solver.check($\Delta_{\text{temp}}$) = SAT and $i\leq k$ do

7:     $i\leftarrow i+1$

8:     $\Delta_{\text{temp}}\leftarrow\Delta_{\text{temp}}\cup e_{i}$

9:     $\Delta_{\text{cert}}^{i}\leftarrow\Delta_{\text{temp}}$

10:$\Delta_{\text{cert}}\leftarrow e_{i}$, $j\leftarrow\lfloor\frac{i}{2}\rfloor$

11:$\Delta^{1}\leftarrow\{e_{1},\cdots,e_{j}\}$

12:$\Delta^{2}\leftarrow\{e_{j+1},\cdots,e_{i-1}\}$

13:$\Delta_{\text{cert}}\leftarrow$ $\Delta_{\text{cert}}\cup$ T-solver.QuickXplain($\Delta_{\text{cert}}^{j}\cup\Delta_{\text{cert}},\Delta^{2}$)

14:$\Delta_{\text{cert}}\leftarrow\Delta_{\text{cert}}\cup$ T-solver.QuickXplain($\Delta_{\text{cert}}^{0}\cup\Delta_{\text{cert}},\Delta^{1}$)

15:return $\Delta_{\text{cert}}$

{algorithm}

T-solver.Certificate 2

1:$\Gamma_{u}^{\text{SAT}},\Gamma_{y}^{\text{SAT}}$

2:$\Delta_{\text{cert}}\leftarrow$ T-solver.QuickXplain($\emptyset,\overline{\Gamma}_{u}^{\text{SAT}}\cup\Gamma_{y}^{\text{SAT}}$)

3:Divide $\Delta_{\text{cert}}$ to inputs $\overline{\Gamma}_{u}^{\text{cert}}$ and outputs $\Gamma_{y}^{\text{cert}}$

4:$\Phi_{\text{cert}}^{2}\leftarrow\sum\limits_{j\in\overline{\Gamma}_{u}^{\text{cert}}}\mathbf{b}_{j}+\sum\limits_{i\in\Gamma_{y}^{\text{cert}}}\mathbf{c}_{i}\geq 1$

5:return $\Phi_{\text{cert}}^{2}$

Lemma 15**.**

For a generic LTI system the size of the certificate is always lower bounded by $m+1$, where $m$ is the number of inputs.

{pf}

Please refer to Appendix.

5 Simulation Results

We implemented our SMT-based estimator in Matlab while interfacing with the SAT solver SAT4J [21] and assessed its performance in two case studies, randomly generated LTI systems and a chemical plant. We report the overall running time by using the two proposed methods, Algorithm 4.3 and Algorithm 4.4.

5.1 Random Systems

We randomly generate systems with a fixed state dimension ($n=40$) and increase the number of inputs and outputs. Each system is generated by drawing entries of $(A,B,C,D)$ according to uniform distribution, when necessary we scale $A$ to ensure that the spectral radius is close to one. In each experiment, twenty percent of inputs and outputs are under adversarial attacks, and we generate the support set for the adversarial signals uniformly at random. Attack signals and the initial states are drawn according to independent and normally distributed random variables with zero mean and unit variance. All the systems under experiment satisfy a suitable sparse strong observability condition as described in Section 3.

Figures 3 and 4 report the results of the simulations, each point represents the average of $20$ experiments. All the experiments run on an Intel Core i5 2.7GHz processor with 16GB of RAM. We verify the run-time improvement resulting from using the shorter certificates, $\Phi_{\text{cert}}^{1}$ and $\Phi_{\text{cert}}^{2}$, compared to the theoretical upper-bound of the brute-force approach in Figure 3. For instance, consider the scenario with $p=24$ and $m=10$ in Figures 3 and 4. In the brute-force approach, we require to check all $24\choose 4$ $\times$ $10\choose 2$ $\approx 4.8*10^{5}$ different combinations of inputs and outputs, however, by exploiting either $\Phi_{\text{cert}}^{1}$ or $\Phi_{\text{cert}}^{2}$ we observe a substantial improvement. We observe that although $\Phi_{\text{cert}}^{2}$ gives a worse run time for systems with smaller number of outputs, it scales better compared to $\Phi_{\text{cert}}^{1}$ when the number of inputs and outputs grow.

5.2 Chemical Plant

In this part, we use the proposed observer to detect attacks on inputs and outputs of a simplified version of the Tennessee Eastman control challenge problem [9]. Ricker [32] derived a continuous time LTI model of the plant interaction in its steady state. This system consists of $4$ control inputs and $10$ measured outputs and the linearized model has $8$ state variables. The structure of the continuous-time dynamics is reported below.

[TABLE]

where $\ast$ represents a non-zero entry333For the exact dynamics of the LTI model, see [32], and $x\in\mathbb{R}^{8}$, $u\in\mathbb{R}^{4}$ and $y\in\mathbb{R}^{10}$ are state, input and output variables, respectively. The only known limitation of this LTI model is the system should operate close to its steady-state. We obtain a discrete-time model by discretizing the continuous-time model assuming a zero-order hold for the input $u$, with a time-step of $5s$. The attacker can read all the inputs and outputs and manipulate one control input and two measured outputs. The linearized system is $(2,4)$-sparse strongly observable, therefore our observer can correctly reconstruct the state under this attack model.

We randomly generate attack signals and the initial state according to independent and normally distributed random variables. The support set of attacks are drawn uniformly at random, and in each experiment one input and two outputs are under adversarial attacks.

The proposed observer in this paper can correctly reconstruct the (delayed) state after $8$ samples, and the average performance of $20$ experiments, by using $\Phi_{\text{cert}}^{1}$ and $\Phi_{\text{cert}}^{2}$ is reported in Table 1. The overall execution time is the run time of the observer after receiving all the required samples from the plant, and it does not take the sampling time of the plant into account. We observe that the execution time of the observer to reconstruct the state and to detect attacks is much smaller compared to the sampling time of the plant.

6 Conclusion

In this paper, we considered the problem of secure state estimation when inputs and/or outputs are under adversarial attacks. In this set-up, there is no restriction on how the adversary manipulates inputs and outputs. By introducing the notion of sparse strong observability, we derived necessary and sufficient conditions under which state estimation is possible given bounds on the number of attacked outputs and inputs. Furthermore, we demonstrated the scalability and effectiveness of the proposed estimator with numerical simulations.