Attacking the V: On the Resiliency of Adaptive-Horizon MPC

TL;DR

This paper introduces a new adaptive-horizon model predictive control method for flocking dynamics, analyzing its resilience against various strategic attacks through statistical model checking.

Contribution

It proposes Adaptive-Horizon MPC (AMPC) for flocking control and evaluates its robustness against different attacker strategies using extensive simulations.

Findings

AMPC enables controllers to almost always achieve V-formation under ideal conditions.

Resource constraints significantly increase attacker success probability.

Intelligent AMPC-enabled attackers outperform naive strategies in disrupting flocking.

Abstract

We introduce the concept of a V-formation game between a controller and an attacker, where controller's goal is to maneuver the plant (a simple model of flocking dynamics) into a V-formation, and the goal of the attacker is to prevent the controller from doing so. Controllers in V-formation games utilize a new formulation of model-predictive control we call Adaptive-Horizon MPC (AMPC), giving them extraordinary power: we prove that under certain controllability assumptions, an AMPC controller is able to attain V-formation with probability 1. We define several classes of attackers, including those that in one move can remove R birds from the flock, or introduce random displacement into flock dynamics. We consider both naive attackers, whose strategies are purely probabilistic, and AMPC-enabled attackers, putting them on par strategically with the controllers. While an AMPC-enabled controller is expected to win every game with probability 1, in practice, it is resource-constrained: its maximum prediction horizon and the maximum number of game execution steps are fixed. Under these conditions, an attacker has a much better chance of winning a V-formation game. Our extensive performance evaluation of V-formation games uses statistical model checking to estimate the probability an attacker can thwart the controller. Our results show that for the bird-removal game with R = 1, the controller almost always wins (restores the flock to a V-formation). For R = 2, the game outcome critically depends on which two birds are removed. For the displacement game, our results again demonstrate that an intelligent attacker, i.e. one that uses AMPC in this case, significantly outperforms its naive counterpart that randomly executes its attack.

Tables

Table 1. Table 1: Results of 2,000 game executions for removing 1 bird with h 𝑚𝑎𝑥 =  5 subscript ℎ 𝑚𝑎𝑥 5 h_{\mathit{max}}\,{=}\,5 , m =  40 𝑚 40 m\,{=}\,40

			Ctrl. success rate, %			Avg. convergence duration			Avg. horizon
Bird 4			$99.9$			$12.75$			$3.64$
Bird 3			$99.8$			$18.98$			$4.25$
Bird 2			$100$			$10.82$			$3.45$

Table 2. Table 2: Results of 2,000 game executions for removing 2 birds with h 𝑚𝑎𝑥 =  5 subscript ℎ 𝑚𝑎𝑥 5 h_{\mathit{max}}\,{=}\,5 , m =  30 𝑚 30 m\,{=}\,30

			Ctrl. success rate, %			Avg. convergence duration			Avg. horizon
Birds 2 and 3			$0.8$			$25.18$			$4.30$
Birds 2 and 4			$83.1$			$11.11$			$2.94$
Birds 2 and 5			$80.3$			$9.59$			$2.83$
Birds 2 and 6			$98.6$			$7.02$			$2.27$
Birds 3 and 4			$2.0$			$22.86$			$4.30$
Birds 3 and 5			$92.8$			$11.8$			$3.43$

Table 3. Table 3: Results of 2,000 game executions for random displacement and AMPC attacks with h 𝑚𝑎𝑥 =  5 subscript ℎ 𝑚𝑎𝑥 5 h_{\mathit{max}}\,{=}\,5 and m =  40 𝑚 40 m\,{=}\,40 (attacker runs for 20 steps)

Range of noise			Ctrl. success rate, %			Avg. convergence duration			Avg. horizon
			Random displacement game
$[0,0.50]\times [0,2\pi ]$			$99.9$			$3.33$			$1.07$
$[0,0.75]\times [0,2\pi ]$			$97.9$			$3.61$			$1.11$
$[0,1.00]\times [0,2\pi ]$			$92.3$			$4.14$			$1.18$
			AMPC game
$[0,0.50]\times [0,2\pi ]$			$97.5$			$4.29$			$1.09$
$[0,0.75]\times [0,2\pi ]$			$63.4$			$5.17$			$1.23$
$[0,1.00]\times [0,2\pi ]$			$20.0$			$7.30$			$1.47$

Equations

$${\mathbf{x}}_i(t+1)$$

$${\mathbf{v}}_i(t+1)$$

$$J(s)=(CV(s)-{CV}^{\ast }{)}^2+(VM(s)-{VM}^{\ast }{)}^2+(UB(s)-{UB}^{\ast }{)}^2.$$

$$G$$

$${\text{opt-a}}^h(t)=\underset{{\mathbf{a}}^h(t)}{\mathrm{argmin}}J(s_{{\mathbf{a}}^h}(t+h)).$$

$${\mathbf{v}}^j(t+1)=\omega \cdot {\mathbf{v}}^j(t)$$

$$+y_2\cdot {\mathbf{u}}_2(t+1)\otimes ({\mathbf{x}}_G^j(t)-{\mathbf{x}}^j(t)),$$

$$\text{Fitness}(\mathcal{M},{\mathbf{a}}^h,h)=\underset{1⩽\tau ⩽h}{\min }J(s_{{\mathbf{a}}^h}^{\tau })$$

$${\mathbf{x}}_i(t+1)$$

$${\mathbf{v}}_i(t+1)$$

$${\mathbf{x}}_i(t+1)$$

$${\mathbf{v}}_i(t+1)$$

$$\mathrm{Pr}\left[{\mu }_Z-\epsilon ⩽{\tilde{\mu }}_Z⩽{\mu }_Z+\epsilon )\right]⩾1-\delta ,$$

$$Z=\left\{\begin{array}[]{ll}1,&\text{if}\>\>\exists t\in[0,m],J(s(t))<\varphi,\\ 0,&\text{otherwise}.\end{array}\right.$$

Full text

We define several classes of attackers, including those that in one move can remove $R$ birds from the flock, or introduce random displacement into flock dynamics. We consider both naive attackers, whose strategies are purely probabilistic, and AMPC-enabled attackers, putting them on par strategically with the controllers. While an AMPC-enabled controller is expected to win every game with probability 1, in practice, it is resource-constrained: its maximum prediction horizon and the maximum number of game execution steps are fixed. Under these conditions, an attacker has a much better chance of winning a V-formation game.

Our extensive performance evaluation of V-formation games uses statistical model checking to estimate the probability an attacker can thwart the controller. Our results show that for the bird-removal game with $R\,{=}\,1$, the controller almost always wins (restores the flock to a V-formation). For $R\,{=}\,2$, the game outcome critically depends on which two birds are removed. For the displacement game, our results again demonstrate that an intelligent attacker, i.e. one that uses AMPC in this case, significantly outperforms its naive counterpart that randomly executes its attack.

1 Introduction

Many Cyber-Physical Systems (CPSs) are highly distributed in nature, comprising a multitude of computing agents that can collectively exhibit emergent behavior. A compelling example of such a distributed CPS is the drone swarm, which are beginning to see increasing application in battlefield surveillance and reconnaisance [3]. The emergent behavior they exhibit is that of flight formation.

A particularly interesting form of flight formation is V-formation, especially for long-range missions where energy conservation is key. V-formation is emblematic of migratory birds such as Canada geese, where a bird flying in the upwash region of the bird in front of it can enjoy significant energy savings. The V-formation also offers a clear view benefit, as no bird’s field of vision is obstructed by another bird in the formation. Because of the V-formation’s intrinsic appeal, it is important to quantify the resiliency of the control algorithms underlying this class of multi-agent CPSs to various kinds of cyber-attacks. This question provides the motivation for the investigation put forth in this paper.

Problem Statement and Summary of Results.

We introduce the concept of V-formation games, where the goal of the controller is to maneuver the plant (a simple model of flocking dynamics) into a V-formation, and the goal of the attacker is to prevent the controller from doing so. Controllers in V-formation games utilize a new formulation of model-predictive control we call Adaptive Receding-Horizon MPC (AMPC), giving them extraordinary power: we prove that under certain controllability conditions, an AMPC controller can attain V-formation with probability 1.

We define several classes of attackers, including those that in one move can remove a small number $R$ of birds from the flock, or introduce random displacement (perturbation) into the flock dynamics, again by selecting a small number of victim agents. We consider both naive attackers, whose strategies are purely probabilistic, and AMPC-enabled attackers, putting them on par strategically with the controllers. The architecture of a V-formation game with an AMPC-enabled attacker is shown in Figure 1. While an AMPC-enabled controller is expected to win every game with probability 1, in practice, it is resource-constrained: its maximum prediction horizon and the maximum number of game execution steps are fixed in advance. Under these conditions, an attacker has a much better chance of winning a V-formation game.

AMPC is a key contribution of the work presented in this paper. Traditional MPC uses a fixed finite prediction horizon to determine the optimal control action. Hence, it may get stuck in local minima. The AMPC procedure chooses it dynamically. Thus, AMPC can adapt to the severity of the action played by its adversary by choosing its own horizon accordingly. The AMPC procedure is inspired by an adaptive optimization procedure recently presented in [9].

Our extensive performance evaluation of V-formation games uses statistical model checking to estimate the probability that an attacker can thwart the controller. Our results show that for the bird-removal game with $R\,{=}\,1$, the controller almost always wins (restores the flock to a V-formation). For $R\,{=}\,2$, the game outcome critically depends on which two birds are removed. For the displacement game, our results again demonstrate that an intelligent attacker, i.e. one that uses AMPC in this case, significantly outperforms its naive counterpart that randomly executes its attack.

Traditional feedback control is, by design, resilient to noise, and also certain kinds of attacks; as our results show, however, it may not be resilient against smart attacks. Adaptive-horizon control helps to guard against a larger class of attacks, but it can still falter due to limited resources. Our results also demonstrate that statistical model checking represents a promising approach toward the evaluation CPS resilience against a wide range of attacks.

The rest of the paper is organized as follows. Section 2 introduces our dynamic model of V-formation in a flock of autonomous agents, and Section 3 defines our controller-attacker stochastic games. Section 4 presents AMPC, and Section 5 shows how AMPC is used in the V-formation games we consider. Section 6 gives a critical analysis of our results, and Section 7 discusses related work. Section 8 offers our concluding remarks and directions for future work.

2 V-Formation

We consider the problem of bringing a flock of $B$ birds from a random initial configuration to an organized V-formation. Recently, Lukina et al. [9] have modeled this problem as a deterministic Markov Decision Process (MDP) $\mathcal{M}$, where the goal was to generate actions that caused $\mathcal{M}$ to reach a desired state.

In our case, $\mathcal{M}$ is an MDP. The state of each bird in the flock is modeled using 4 variables: a 2-dimensional vector ${\boldsymbol{x}}$ denoting the position of the bird in a 2D space, and a 2-dimensional vector ${\boldsymbol{v}}$ denoting the velocity of the bird. Thus, the state space of ${\mathcal{M}}$ is $\mathbb{R}^{4B}$ representing a flock of $B$ birds. The control actions of each bird are 2-dimensional accelerations ${\boldsymbol{a}}$ and 2-dimensional position displacements ${\boldsymbol{d}}$ (see discussion of ${\boldsymbol{a}}$ and ${\boldsymbol{d}}$ below). Both are random variables.

Let ${\boldsymbol{x}}_{i}(t),{\boldsymbol{v}}_{i}(t),{\boldsymbol{a}}_{i}(t)$, and ${\boldsymbol{d}}_{i}(t)$ denote the position, velocity, acceleration, and displacement of the $i$-th bird at time $t$, respectively. Then, the transition relation of the MDP $\mathcal{M}$ is given as follows:

[TABLE]

Once the current acceleration and displacement are sampled, the next state is uniquely determined by (2) from the current state in ${\mathcal{M}}$ [9].

The problem of whether we can go from a random flock to a V-formation is a reachability question. The reachability goal is the set of states representing a V-formation. A key assumption in [9] was that the reachability goal can be specified using a fitness function $J$, which assigns a non-negative real (fitness) value to each state in ${\mathcal{M}}$.

The fitness of a state was determined by the following three terms:

• •

Clear View (${\it CV}$). A bird’s visual field is a cone with angle $\theta$ that can be blocked by the wings of other birds. The clear-view metric is defined by accumulating the percentage of a bird’s visual field that is blocked by other birds. The CV for the flock is the sum of the clear-view metric of all birds. The minimum value of ${\it CV}$ is ${\it CV}^{*}{=}\,0$, and this value is attained in a perfect V-formation where all birds have clear view.

• •

Velocity Matching (${\it VM}$). ${\it VM}$ is defined as the difference between the velocity of a given bird and all other birds, summed up over all birds in the flock. The minimum value for ${\it VM}$ is ${\it VM}^{*}{=}\,0$, and this value is attained in a perfect V-formation where all birds have the same velocity.

• •

Upwash Benefit (${\it UB}$). The trailing upwash is generated near the wingtips of a bird, while downwash is generated near the center of a bird. An upwash measure $um$ is defined on the 2D space using a Gaussian-like model that peaks at the appropriate upwash and downwash regions. For bird $i$ with upwash $um_{i}$, the upwash-benefit metric ${\it UB}_{i}$ is defined as $1\,{-}um_{i}$, and ${\it UB}$ for the flock is the sum of all ${\it UB}_{i}$ $\forall~{}i\,{\in}\,\{1,\ldots,B\}$. The upwash benefit ${\it UB}$ of a flock in V-formation is ${\it UB}^{*}\,{=}\,1$, as all birds, except for the leader, have minimum upwash-benefit metric (${\it UB}_{i}=0,um_{i}=1$), while the leader has upwash-benefit metric of $1$ (${\it UB}_{i}=1,um_{i}=0$).

Let $s=\{{\boldsymbol{x}}_{i},{\boldsymbol{v}}_{i}\}_{i=1}^{B}$ be a state of a flock with $B$ birds. Given the above metrics, the overall fitness (cost) metric $J$ is of a sum-of-squares combination of ${\it VM}$, ${\it CV}$, and ${\it UB}$ defined as follows:

[TABLE]

A state $s^{*}$ is considered to be a V-formation whenever $J(s^{*})\,{<}\,\varphi$, for a certain small threshold $\varphi$.

Given the above flocking model, the goal is to bring the flock from any configuration to a V-formation. Recall that we had two sets of control variables: accelerations $\vec{a}$ and displacements $\vec{d}$ for each bird of the flock. We consider the scenario where the accelerations are under the control of one agent (the controller), and the displacements (position perturbations) are under the control of a second malicious agent (the attacker). This partition of the actions of the MDP into disjoint sets gives rise to a stochastic game on an MDP, which is described next.

3 Controller-Attacker Games: Problem Definition

We are interested in games between a controller and an attacker, where the goal of the controller is to take the system to a desired set of states, and the goal of the attacker is to keep the system outside these states. We formulate our problem by using a Markov Decision Processes (MDP) such that the controller and the attacker jointly determine the transition probabilities.

Definition 1

A Markov Decision Process (MDP) ${\mathcal{M}}$ is a tuple $(S,A,T,J)$ consisting of: (1) a set $S$ of states, (2) a set $A$ of actions, (3) a function $T:S\,{\times}\,A\,{\times}\,S\,{\mapsto}\,[0,1]$, where $T(s,a,s^{\prime})$ is the probability of transitioning from state $s$ to state $s^{\prime}$ under action $a$, and (4) a function $J:S\,{\mapsto}\,\mathbb{R}$, where $J(s)$ is the reward (fitness) associated to state $s$.

In a stochastic game [15], the transition probability from state $s$ to state $s^{\prime}$ is controlled jointly by two players, a controller and an attacker in our case. To view an MDP as a stochastic game, we assume that the set of actions $A$ is given as a product $C\,{\times}\,D$, where the controller chooses the $C$-component of an action ${\boldsymbol{a}}$ and the attacker chooses the $D$-component of ${\boldsymbol{a}}$. We assume that the game is played in parallel by the controller and the attacker; i.e., they both take the state $s(t)\in{S}$ of the system at time $t$, compute their respective actions $c(t)\in C$ and $d(t)\in D$, and then use the composed action $(c(t),d(t))$ to determine the next state $s(t+1)\in{S}$ of the system (based on the transition function $T$).

We consider randomized strategies for both the controller and the attacker. A randomized strategy is a mapping taking every state $s$ to a probability distribution $P(a\,{|}\,s)$ over the (available) actions. Once we fix a randomized strategy for the controller, and a randomized strategy for the attacker, the MDP reduces to a Markov chain on the state space $S$. Thus, the controller and attacker jointly fix the probability of transitioning from a state $s$ to a state $s^{\prime}$.

In this paper, we consider reachability games only. In other words, we are given a set $G$ of “good” states and the goal of the controller is to reach a state in $G$. Let $s_{0}\,{\rightarrow}\,s_{1}\,{\rightarrow}\,s_{2}\,{\rightarrow}\,\cdots$ be a sequence of states (a run of the system). The controller wins on this run if $\exists{i}:s_{i}\in G$, and the attacker wins otherwise.

We are interested in discrete-time continuous-space dynamical systems. Formally, the state space $S$ is $\mathbb{R}^{n}$ and the action space $A$ is in $\mathbb{R}^{m}$. In the bird flocking example, $n\,{=}\,m\,{=}\,4\,{\cdot}\,B$, where $B$ is the number of birds. We have four state variables and four action variables, respectively for each bird. They represent the $x$- and the $y$-components of the position ${\boldsymbol{x}}_{i}$, velocity ${\boldsymbol{v}}_{i}$, acceleration ${\boldsymbol{a}}_{i}$, and displacement ${\boldsymbol{d}}_{i}$ of each bird $i$, respectively.

A classical problem in the study of games pertains to determining the existence of an optimal winning strategy (e.g. a Nash equilibrium) for a player. We are not concerned with such problems in this paper. Due to the uncountably many states in the state- and action-space, solving such problems for our games of interest is extremely challenging. Instead, we focus on the problem of determining the likely winner of a game where the strategy of the two players is fixed. Since we consider randomized strategies, determining the likely winner is a statistical model checking problem. In other words, we want to evaluate the resilience of certain controllers under certain attack models.

We are now ready to formally define the problem we would like to solve.

Definition 2 (Stochastic-game verification problem)

Let ${\mathcal{M}}\,{=}\,(S,A,T,J)$ be an MDP, where $A\,{=}\,C\,{\times}\,D$, and randomized strategies $\sigma_{C}:S\,{\mapsto}\,PD(C)$ and $\sigma_{D}:S\,{\mapsto}\,PD(D)$ mapping states $S$ to probability distributions over $C$ and $D$. The stochastic-game verification problem is to determine the probability of reaching a state in $G\,{\subset}\,S$ in $m$ steps, for a given $m$, starting from an initial state (taken from a given probability distribution) in the underlying Markov chain induced by strategies $\sigma_{C},\sigma_{D}$ on the MDP ${\mathcal{M}}$.

Let us specify the randomized strategies. For a strategy $\sigma$, we assume that we are given a randomized algorithm that takes a state $s$ and returns an action consistent with the probability distribution $\sigma(s)$.

Our main interest here is in evaluating the resilience of a specific controller algorithm $\sigma_{C}$. The key assumption that the controller and the attacker algorithms make is the existence of a fitness function $J:S\,{\mapsto}\,\mathbb{R}^{+}$ such that

[TABLE]

Given such a fitness metric $J$, the controller works by minimizing the fitness of states reachable, in one or more steps, as it is done in model-predictive control (MPC). Since the fitness function is highly nonlinear, the controller uses an optimization procedure based on randomization to search for a minimum. Hence, our controller is a randomized procedure. One possible attack strategy we consider (for an advanced attacker) is based on the fitness function as well: the attacker tries to maximize the fitness of reachable states.

A key contribution of our work is an adaptive MPC procedure called AMPC. Recall that traditional MPC uses a fixed finite horizon to determine the best control action. The AMPC procedure chooses it dynamically. Thus, AMPC can adapt to the severity of the action played by its adversary by choosing its own horizon accordingly. The AMPC procedure is inspired by an adaptive optimization procedure recently presented in [9], which dynamically changes the amount of the effort it uses to search for a better solution in each step. The motivation for adaptation in [9] however was different, namely to take the optimizer out of a local minimum, and thus, ensure convergence to a global optimum.

4 The Adaptive-Horizon MPC Algorithm

We now present our new adaptive-horizon model-predictive-control algorithm, we call AMPC. We will use this algorithm as the controller strategy in the stochastic game on MDPs. We will also consider attack strategies that use AMPC. Since AMPC is an adaptive MPC procedure based on particle-swarm optimization (PSO), we first briefly present background material on MPC and PSO.

4.1 Background on Model-Predictive Control

Model-predictive control (MPC) determines the control action at current time $t$ by looking $h$ steps into the future and finding the best $h$-length sequence of control actions that can take the system from its current state $s(t)$ to a new state that has the lowest fitness. (Since we assume existence of a fitness metric $J$ that we are trying to minimize, we specialize the description of MPC to this case.) If ${s}_{{\boldsymbol{a}}^{h}}(t+h)$ denotes the state reached from state ${s}(t)$ in time $h$ following the actions ${\boldsymbol{a}}^{h}$ of length $h$, then in the MPC approach, at each time step $t$, the following minimization is performed to find the optimal set of actions

[TABLE]

Since the model is an approximation of the system, only the first action {\boldsymbol{a}}(t)=\textbf{opt-{\boldsymbol{a}}}^{1}(t) is applied as the action at time $t$, and the remaining future $h-1$ actions found by the optimizer are ignored. After the control action ${\boldsymbol{a}}(t)$ is applied, the system is left to evolve, and the process is repeated at $t\,{+}\,1,t\,{+}\,2,$ and so on.

The MPC approach can be used for achieving a V-formation, as was outlined in [17, 16]. These earlier works, however, did not use an adaptive dynamic window, and did not consider the adversarial control problem.

In MPC, optimization problem (3) is additionally subject to constraints that bound the set of possible actions and states. For example, in our flocking model, the magnitude of velocity and acceleration for each of the $B$ birds is bounded: $||{\boldsymbol{v}}_{i}(t)||\,{\leqslant}\,{\boldsymbol{v}}_{max},||{\boldsymbol{a}}^{h}_{i}(t)||\,{\leqslant}\,\rho||{\boldsymbol{v}}_{i}(t)||$ $\forall$ $i\,{\in}\,\{1,\ldots,B\}$, where ${\boldsymbol{v}}_{max}$ is a predefined constant and $\rho\,{\in}\,(0,1)$.

We use a particle-swarm-optimization algorithm to solve the optimization problems generated by the MPC procedure.

4.2 Background on Particle Swarm Optimization

Particle Swarm Optimization (PSO) is a randomized approximation algorithm for determining the parameters that minimize a possibly nonlinear and possibly discontinuous cost (or fitness) function. PSO was first introduced by [8]. In an interesting twist of events, PSO took its original inspiration from bird flocking.

The PSO procedure is best described using the metaphor of a swarm of insects collaboratively trying to find the location of food. The insects, also called particles, live in the space defined by all possible valuations of the unknown parameters (of the optimization problem). The food is located at the position where the objective function is minimized. PSO works by having a swarm of particles, which have the same goal of finding food (the reward) without knowing its location. Each particle is informed about its distance to the food (value of the objective function). The PSO algorithm repeatedly redistributes each particle towards the one closest to the food, with a speed proportional to the distance separating them, until all particles converge to the same position.

AMPC employs Matlab’s toolbox particleswarm, which performs the classical version of PSO. A swarm of $p$ particles is sampled uniformly at random within a given bound on their positions and velocities. In the bird flocking example, if we try to find acceleration vectors by optimization over horizon $h$, then one “particle” represents $h$ 2-dimensional vectors for each of the $B$ birds, along with a vector of values that determine how these $h\cdot B$ acceleration vectors will be updated. After choosing a neighborhood of random size for each particle $j$, $j\,{\in}\,\{1,\ldots,p\}$, PSO computes the value of the given fitness function for each particle, and stores two vectors for each particle $j$: its so-far personal-best position $\mathbf{x}_{P}^{j}(t)$, and the position of its fittest neighbor $\mathbf{x}_{G}^{j}(t)$. The positions and velocities of the particle swarm $j\,{\in}\,\{1,\ldots,p\}$ are updated the following way:

[TABLE]

where $\omega$ is an inertia weight, which quantifies the trade-off between global and local exploration of the swarm (the value of $\omega$ is proportional to the exploration range); $y_{1}$ and $y_{2}$ are the self adjustment and the social adjustment, respectively; $\mathbf{u_{1}},\mathbf{u_{2}}\,{\in}\,{\rm Uniform}(0,1)$ are random variables; and $\otimes$ is the vector dot product, that is, $\forall$ random vector $\mathbf{z}$: $(\mathbf{z}_{1},\ldots,\mathbf{z}_{b})\otimes(\mathbf{x}_{1}^{j},\ldots,\mathbf{x}_{b}^{j})=(\mathbf{z}_{1}\mathbf{x}_{1}^{j},\ldots,\mathbf{z}_{b}\mathbf{x}_{b}^{j})$.

If the value of the fitness computed at each step of the PSO for $\mathbf{x}^{j}(t+1)\,{=}\,\mathbf{x}^{j}(t)\,{+}\,\mathbf{v}^{j}(t+1)$ falls below the one for $\mathbf{x}_{P}^{j}(t)$, then $\mathbf{x}^{j}(t+1)$ is reassigned to $\mathbf{x}_{P}^{j}(t+1)$. A global best for the next iteration is determined as the particle with the best fitness among $j\,{\in}\,\{1,\ldots,p\}$. The stopping criterion of the PSO algorithm is either reaching the maximum number of iterations set in advance, or reaching the set time bound, or satisfying the minimum criterion.

PSO can be used to solve any optimization problem. We use it to solve the optimization problem generated in the MPC approach. In a V-formation game, it can be used to obtain the birds’ best accelerations, or even the best displacements, at each time step – depending on whether MPC/PSO is being used by the controller or the attacker.

Remark. We assume that PSO is fair, in the sense that it has a chance to sample all the points in the parameter space, and therefore it has the chance to find the optimal solution with probability one, given enough time.

4.3 The Main Algorithm of AMPC

We propose the main algorithm of AMPC. This algorithm performs step-by-step control of a given MDP ${\mathcal{M}}$ by looking $h$ steps ahead and predicting the next best state to move to. We use PSO to identify the potentially best actions ${\boldsymbol{a}}^{h}$ in the current state achieving the optimal value of the fitness function in the next state. For bird flocking, the fitness function, Fitness$({\mathcal{M}},{\boldsymbol{a}}^{h},h)$ of ${\boldsymbol{a}}^{h}$ is defined as the minimum fitness metric $J$ obtained within $h$ steps by applying ${\boldsymbol{a}}^{h}$ on ${\mathcal{M}}$. Formally, we have

[TABLE]

where $s_{{\boldsymbol{a}}^{h}}^{\tau}$ is the state after apply the $\tau$th action of ${\boldsymbol{a}}^{h}$ on ${\mathcal{M}}$. For horizon $h$, PSO searches for the best sequence of 2-dimensional acceleration vector of length $h$, thus having $2Bh$ parameters to be optimized. The number of particles used in PSO is proportional to the number of parameters, i.e., $p=2\beta Bh$.

The pseudocode for the AMPC algorithm is given in Algorithm 1. A novel feature of AMPC is that, unlike classical MPC that uses a fixed horizon $h$, AMPC adaptively chooses an $h$ depending on whether it is able to reach a fitness value that is lower than the current fitness by our chosen quanta $\Delta_{i}$, $\forall~{}i\,{\in}\,\{0,\ldots,m\}$.

AMPC is hence an adaptive MPC procedure that uses level-based horizons. It employs PSO to identify the potentially best next actions. If the chosen actions improve (decrease) the fitness of the next state $J(s_{k+h})$, $\forall~{}k\,{\in}\,\{0,\ldots,m\cdot h_{\mathit{max}}\}$, in comparison to the fitness of the previous state $J(s_{k})$ by the predefined $\Delta_{i}$, the controller considers these actions to be worthy of leading the flock towards or keeping it in the V-formation.111We focus our attention on bird flocking, since the details generalize naturally to other MDPs that come with a fitness metric.

In this case, the controller applies the actions to each bird and transitions to the next state of the MDP. The threshold $\Delta_{i}$ determines the next level $\ell_{i}\,{=}\,J(s_{k+\widehat{h}})$ of the algorithm, where $\widehat{h}\leqslant h$ is the horizon with the best fitness. The prediction horizon $h$ is increased iteratively if the fitness has not been decreased enough. Upon reaching a new level, the horizon is reset to one (see Algorithm 1). Having a horizon $\widehat{h}\,{>}\,1$ means it will take multiple transitions in the MDP in order to reach a solution with improved fitness. However, when finding such a solution with $\widehat{h}\,{>}\,1$, we only apply the first action to transition the MDP to the next state. This is explained by the need to allow the other player (environment or an adversary) to apply their action before we obtain the actual next state. If no new level is reached within $h_{\mathit{max}}$ horizons, the first action of the best ${\boldsymbol{a}}^{h}$ using horizon $h_{\mathit{max}}$ is applied.

The dynamic threshold $\Delta_{i}$ is defined as in [9]. Its initial value $\Delta_{0}$ is obtained by dividing the fitness range to be covered into $m$ equal parts, that is, $\Delta_{0}\,{=}\,(\ell_{0}\,{-}\,\ell_{m})\,{/}\,m$, where $\ell_{0}\,{=}\,J(s_{0})$ and $\ell_{m}\,{=}\,\varphi$. Subsequently, $\Delta_{i}$ is determined by the previously reached level $\ell_{i-1}$, as $\Delta_{i}\,{=}\,\ell_{i-1}{/}(m\,{-}\,i\,{+}\,1)$. This way AMPC advances only if $\ell_{i}\,{=}\,J(s_{k+\widehat{h}})$ is at least $\Delta_{i}$ apart from $\ell_{i-1}\,{=}\,J(s_{k})$.

This approach allows us to force PSO to escape from a local minimum, even if this implies passing over a bump, by gradually increasing the exploration horizon $h$. We assume that the MDP is controllable and that the set $G$ of good states is not empty, which means, that from any state, it is possible to reach a state whose fitness decreased by at least $\Delta_{i}$. Algorithm 1 illustrates our approach.

Theorem 4.1 (AMPC Convergence)

Given an MDP ${\mathcal{M}}\,{=}\,(S,A,T,J)$ with positive and continuous fitness function $J$, and a nonempty set of target states $G\,{\subset}\,S$ with $G\,{=}\,\{s\,|\,J(s)\,{<}\,\varphi\}$. If the transition relation $T$ is controllable with actions in $A$, then there is a finite maximum horizon $h_{\mathit{max}}$ and a finite number of execution steps $m$, such that AMPC is able to find a sequence of actions $a_{1},\ldots,a_{m}$ that brings a state in $S$ to a state in $G$ with probability one.

Proof

In each (macro) step of horizon length $h$, from level $\ell_{i-1}\,{=}\,J(s_{k})$ to level $\ell_{i}\,{=}\,J(s_{k+\widehat{h}})$, AMPC decreases the distance to $\varphi$ by $\Delta_{i}\,{\geqslant}\,\Delta$, where $\Delta\,{>}\,0$ is fixed by the number of steps $m$ chosen in advance. Hence, AMPC converges to a state in $G$ in a finite number of steps, for a properly chosen $m$. AMPC is able to decrease the fitness in a macro step by $\Delta_{i}$ by the controllability assumption and the fairness assumption about the PSO algorithm. Since AMPC is a randomized algorithm, the result is probabilistic.

Note that AMPC is a general procedure that performs adaptive MPC using PSO for dynamical systems that are controllable, come with a fitness metric, and have at least one optimal solution. In an adversarial situation two players have opposing objectives. The question arises what one player assumes about the other when computing its own action, which we discuss next.

5 Stochastic Games for V-Formation

We describe the specialization of the stochastic-game verification problem to V-formation. In particular, we present the AMPC-based control strategy for reaching a V-formation, and the various attacker strategies against which we evaluate the resilience of our controller.

The MDP ${\mathcal{M}}$ for V-formation was presented in Section 2. The state variables of the MDP are the positions and velocities of the birds, and the control variables (defining the actions) are the accelerations and displacements. In the transition relation given in equation (1), the attacker chooses the displacement $\vec{d}(t)$ it needs to manipulate the position of the birds, whereas the controller chooses the acceleration $\vec{a}(t)$ to apply. Together, the pair $(\vec{a}(t),\vec{d}(t))$ defines the action that transforms one MDP state to another. We now define the controller’s and attacker’s strategies.

5.1 Controller’s Adaptive Strategies

Given current state $(\vec{x}(t),\vec{v}(t))$, the controller’s strategy $\sigma_{C}$ returns a probability distribution on the space of all possible accelerations (for all birds). As mentioned above, this probability distribution is specified implicitly via a randomized algorithm that returns an actual acceleration (again for all birds). This randomized algorithm is the AMPC algorithm, which inherits its randomization from the randomized PSO procedure it deploys.

When the controller computes an acceleration, it assumes that the attacker does not introduce any disturbances; i.e., the controller uses the following model:

[TABLE]

where ${\boldsymbol{a}}(t)$ is the only control variable. Note that the controller chooses its next action ${\boldsymbol{a}}(t)$ based on the current configuration $({\boldsymbol{x}}(t),{\boldsymbol{v}}(t))$ of the flock using MPC. The current configuration may have been influenced by the disturbance $\vec{d}(t-1)$ introduced by the attacker in the previous time step. Hence, the current state need not be the state predicted by the controller when performing MPC in step $t-1$. Moreover, depending on the severity of the attacker action $\vec{d}(t-1)$, the AMPC procedure dynamically adapts its behavior, i.e. the choice of horizon $h$, in order to enable the controller to pick the best control action $\vec{a}(t)$ in response.

5.2 Attacker’s Strategies

We are interested in evaluating the resilience of our V-formation controller when it is threatened by an attacker that can remove a certain number of birds from the flock, or manipulate a certain number of birds by taking control of their actuators (modeled by the displacement term in equation (2)). We assume that the attack lasts for a limited amount of time, after which the controller attempts to bring the system back into the good set of states. When there is no attack, the system behavior is the one given by equation (6).

Note that there can be many different criteria for evaluating the success of an attack, but in our experiments, the controller is declared the winner if it can bring the flock to V-formation. We consider three attack strategies (but see the future work discussion in Section 8), each of which defines a V-formation game.

Remove Birds Game.

In an RBG, the attacker selects a subset of $R$ birds, where $R\,{\ll}\,B$, and removes them from the flock. The removal of bird $i$ from the flock at time $t\,{=}\,0$ can be simulated in our framework by allowing the attacker to set the displacement ${\boldsymbol{d}}_{i}(0)$ for bird $i$ to $\infty$. We assume that the flock is in a V-formation at time $t\,{=}\,0$. Thus, the goal of the controller is to bring the flock back into a V-formation consisting of $B\,{-}\,R$ birds. In an RBG, the attacker plays only one move. When picking birds, the attacker is able to decide which birds will have the greatest negative impact on the flock’s fitness when removed from the flock. Apart from seeing if the controller can bring the flock back to a V-formation, we also analyze the time it takes the controller to do so.

Random Displacement Game.

In an RDG, the attacker chooses the displacement vector for a fixed number $R$ of birds uniformly from the space $[0,M]\times[0,2\pi]$. This means that the magnitude of the displacement vector is picked from the interval $[0,M]$, and the direction of the displacement vector is picked from the interval $[0,2\pi]$. We vary $M$ in our experiments. The $R$ birds that are picked in different steps are not necessarily the same, as the attacker makes this choice uniformly at random at runtime as well. The game starts from an initial V-formation. The attacker is allowed a fixed number of moves, say $20$, after which the displacement vector is identically [math] for all birds. The controller, which has been running in parallel with the attacker, is then tasked with moving the flock back to a V-formation, if necessary.

AMPC Game.

An AMPC game is similar to an RDG except that the attacker does not use a uniform distribution to determine the displacement vector. The attacker is advanced and calculates the displacement (that will be the worst for the controller) using the AMPC procedure. See Figure 1. In detail, the attacker applies AMPC, but assumes the controller applies zero acceleration. Thus, the attacker uses the following model of the flock dynamics:

[TABLE]

Note that the attacker is still allowed to have ${\boldsymbol{d}}_{i}(t)$ be nonzero for a small number $R$ of birds. However, it can choose which $R$ birds it picks in each step. It uses the AMPC procedure to simultaneously pick the $R$ birds and their displacements.

Theorem 5.1 (AMPC resilience in a C-A game)

Given a controller-attacker game, there is a finite maximum horizon $h_{\mathit{max}}$ and a finite maximum number of game-execution steps $m$ such that AMPC controller will win the controller-attacker game in $m$ steps with probability one.

Proof

Since the flock MDP (defined by Equation 6) is controllable, the PSO algorithm we use is fair, and the attack has a bounded duration, the proof of the theorem follows from Theorem 4.1.

Remark 1

While Theorem 5.1 states that the controller is expected to win with probability one, we expect winning probability to be possibly lower than one in many cases because: (1) the maximum horizon $h_{\mathit{max}}$ is fixed in advance, and so is (2) the maximum number of execution steps $m$; (3) the underlying PSO algorithm is also run with bounded number of particles and time.

6 Statistical MC Evaluation of V-Formation Games

As discussed in Section 3, the stochastic-game verification problem we address in the context of the V-formation-AMPC algorithm is formulated as follows. Given a flock MDP ${\mathcal{M}}$ (we consider the case of $B\,{=}\,7$ birds), acceleration actions ${\boldsymbol{a}}$ of the controller, displacement actions ${\boldsymbol{d}}$ of the attacker, the randomized strategy $\sigma_{C}:S\,{\mapsto}\,PD(C)$ of the controller (the AMPC algorithm), and a randomized strategy $\sigma_{D}:S\,{\mapsto}\,PD(D)$ for the attacker, determine the probability of reaching a state $s$ where the fitness function $J(s)\,{<}\,\varphi$ (V-formation in a 7-bird flock), starting from an initial state (in this case this is a V-formation), in the underlying Markov chain induced by strategies $\sigma_{C}$, $\sigma_{D}$ on ${\mathcal{M}}$.

Since the exact solution to this reachability is intractable due to the infinite/continuous space of states and actions, we solve it approximately with classical statistical model-checking (SMC). The particular SMC procedure we use is described in [6] and based on an additive or absolute-error $(\varepsilon,\delta)$-Monte-Carlo-approximation scheme. This technique requires running $N$ i.i.d. game executions, each for a given maximum time horizon, computing if these executions reach a V-formation, and returning the average number of times this occurs.

The $N$ i.i.d. experiments determine the random variables $Z_{1},...,Z_{N}$, where the sample mean $\mu_{Z}\,{=}\,(Z_{1}\,{+}\,{\ldots}\,{+}\,Z_{N})/N$ is assumed to be sufficiently greater than 0. In this case, one can exploit the Bernstein’s inequality and fix $N$ to $\Upsilon\,{\propto}\,ln(1/\delta)/\varepsilon^{2}$. This results in an additive-error $(\varepsilon,\delta)$-approximation scheme:

[TABLE]

where $\widetilde{\mu}_{Z}$ approximates $\mu_{Z}$ with absolute error $\varepsilon$ and probability $1-\delta$. In our case, each $Z_{i}$ is a Bernoulli random variable, where 1 means that the execution ends in a V-formation, and 0 means the opposite:

[TABLE]

This allows us to use the Chernoff-Hoeffding instantiation of the Bernstein’s inequality, and fix the proportionality constant to $\Upsilon\,{=}\,4\,ln(2/\delta)/\varepsilon^{2}$, as in [7].

Each of the games described in Section 5 is executed 2,000 times. For a confidence ratio $\delta\,{=}\,0.01$, we thus obtain an additive error of $\varepsilon\,{=}\,0.1$.

We use the following parameters in the game executions: number of birds $B\,{=}\,7$, threshold on the fitness $\varphi\,{=}\,10^{-3}$, maximum horizon $h_{\mathit{max}}\,{=}\,5$, number of particles in PSO $p\,{=}\,20\,B\,h$. In RBG, the controller is allowed to run for a maximum of $30$ steps. In RDG and AMPC game, the attacker and the controller run in parallel for $20$ steps, after which the displacement becomes [math], and the controller has a maximum of $20$ more steps to restore the flock to a V-formation.

To perform SMC evaluation of our AMPC approach we designed the above experiments in C and ran them on the Intel Core i7-5820K CPU with 3.30 GHz and with 32GB RAM available.

6.1 Discussion of the Results

To demonstrate the resilience of our adaptive controller, for each game introduced in Section 5, we performed a number of experiments to estimate the probability of the controller winning. Moreover, for the runs where the controller wins, the average number of steps required by the controller to bring the flock to a V-formation is reported as average convergence duration, and the average length of the horizon used by AMPC is reported as average horizon.

The numbering of the birds in Tables 1 and 2 is given in Figure 2. Bird-removal scenarios that are symmetric with the ones in the tables are omitted. The results presented in Table 1 are for the RBG game with $R\,{=}\,1$. In this case, the controller is almost always able to bring the flock back to a V-formation, as is evident from Table 1. Note that removing Bird $1$ (or $7$) is a trivial case that results in a V-formation.

In the case when $R\,{=}\,2$, shown in Table 2, the success rate of the controller depends on which two birds are removed. Naturally, there are cases where dropping two birds does not break the V-formation; for example, after dropping Birds 1 and 2, the remaining birds continue to be in a V-formation. Such trivial cases are not shown in Table 2. Note that the scenario of removing Bird $1$ (or $7$) and one other bird can be viewed as removing one bird in flock of $6$ birds, thus not considered in this table. Among the other nontrivial cases, the success rate of controller drops slightly in four cases, and drops drastically in remaining two cases. This suggests that attacker of a CPS system can incur more damage by being prudent in the choice of the attack.

Impressively, whenever the controller wins, the controller needs about the same number of steps to get back to V-formation (as in the one-bird removal case). On average, removal of two birds results in a configuration that has worse fitness compared to an RBG with $R\,{=}\,1$. Hence, the adaptive controller is able to make bigger improvements (in each step) when challenged by worse configurations. Furthermore, among the four cases where the controller win rate is high, experimental results demonstrate that removing two birds positioned asymmetrically with respect to the leader poses a stronger, however, still manageable threat to the formation. For instance, the scenarios of removing birds 2 and 6 or 3 and 5 give the controller a significantly higher chance to recover from the attack, $98.6\%$ and $92.8\%$, respectively.

Table 3 explores the effect of making the attacker smarter. Compared to an attacker that makes random changes in displacement, an attacker that uses AMPC to pick its action is able to win more often. This again shows that an attacker of a CPS system can improve its chances by cleverly choosing the attack. For example, the probability of success for the controller to recover drops from $92.3\%$ to $20.0\%$ when the attacker uses AMPC to pick displacements with magnitude in $[0,1]$ and direction in $[0,2\pi]$. The entries in the other two columns in Table 3 reveal two even more interesting facts.

First, in the cases when the controller wins, we clearly see that the controller uses a longer look-ahead when facing a more challenging attack. This follows from the observation that the average horizon value increases with the strength of attack. This gives evidence for the fact that the adaptive component of our AMPC plays a pivotal role in providing resilience against sophisticated attacks. Second, the average horizon still being in the range $1$-$1.5$, means that the adaptation in our AMPC procedure also helps it perform better than a fixed-horizon MPC procedure, where usually the horizon is fixed to $h\,{\geqslant}\,2$. When a low value of $h$ (say $h\,{=}\,1$) suffices, the AMPC procedure avoids unnecessary calculation that using a fixed $h$ might incur.

In the cases where success rate was low (Row 5 in Table 2 and Row 6 in Table 3), we observed improved success rate ($9\%$ and $30.8\%$ respectively across $500$ runs) when we increased $h_{\mathit{max}}$ to $10$ and $m$ to $40$. This shows that success rate of AMPC improves as it is given more resources, as predicted by Theorem 4.1.

7 Related Work

In the field of CPS security, one of the most widely studied attacks is sensor spoofing. When sensors measurements are compromised, state estimation becomes challenging, which inspired a considerable amount of work on attack-resilient state estimation [5, 14, 12, 13, 4]. In these approaches, resilience to attacks is typically achieved by assuming the presence of redundant sensors, or coding sensor outputs. In our work, we do not consider sensor spoofing attacks, but assume the attacker gets control of the displacement vectors (for some of the birds/drones). We have not explicitly stated the mechanism by which an attacker obtains this capability, but it is easy to envision ways (radio controller, attack via physical medium, or other channels [2]) for doing so.

Adaptive control, and its special case of adaptive model predictive control, typically refers to the aspect of the controller updating its process model that it uses to compute the control action. The field of adaptive control is concerned with the discrepancy between the actual process and its model used by the controller. In our adaptive-horizon MPC, we adapt the lookahead horizon employed by the MPC, and not the model itself. Hence, the work in this paper is orthogonal to what is done in adaptive control [10, 1].

A key focus in CPS security has also been detection of attacks. For example, recent work considers displacement-based attacks on formation flight [11], but it primarily concerned with detecting which UAV was attacked using an unknown-input-observer based approach. We are not concerned with detecting attacks, but establishing that the adaptive nature of our controller provides attack-resilience for free. Moreover, in our setting, for both the attacker the and controller the state of the plant is completely observable.

We are unaware of any work that uses statistical model checking to evaluate the resilience of adaptive controllers against (certain classes of) attacks.

8 Conclusions

We have introduced AMPC, a new model-predictive controller that unlike MPC, comes with provable convergence guarantees. The key innovation of AMPC is that it dynamically adapts its receding horizon (RH) to get out of local minima. In each prediction step, AMPC calls PSO with an optimal RH and corresponding number of particles. We used AMPC as a bird-flocking controller whose goal is to achieve V-formation despite various forms of attacks, including bird-removal, bird-position-perturbation, and advanced AMPC-based attacks. We quantified the resiliency of AMPC to such attacks using statistical model checking. Our results show that AMPC is able to adapt to the severity of an attack by dynamically changing its horizon size and the number of particles used by PSO to completely recover from the attack, given a sufficiently long horizon and execution time (ET). The intelligence of an attacker, however, makes a difference in the outcome of a game if RH and ET are bounded before the game begins.

Future work includes the consideration of additional forms of attacks, including: Energy attack, when the flock is not traveling in a V-formation for a certain amount of time; Collisions, when two birds are dangerously close to each other due to sensor spoofing or adversarial birds; and Heading change, when the flock is diverted from its original destination (mission target) by a certain degree.