Rampo: A CEGAR-based Integration of Binary Code Analysis and System Falsification for Cyber-Kinetic Vulnerability Detection

We use the symbols $\mathbb{N}$, $\mathbb{R}$, and $\mathbb{B}$ to denote the set of natural, real, and Boolean numbers, respectively. Additionally, we use the symbol $\mathbb{FP}$ to denote the set of Floating Point numbers. For ease of notation, we do not distinguish between 32-bit (single) or 64-bit (double) floating point numbers. We use $\land$, $\lor$, and $\lnot$ to represent the logical AND, OR, and NOT operators, respectively. Given a sequence $a=\{a_{t}\}_{t=0}^{N}$, we denote by $\texttt{Element}(a,i)$ the $i$th element of the sequence $a$.

We consider nonlinear, discrete-time dynamical systems:

where $x_{t}\in\mathbb{R}^{n}$ is the state of the system at time $t\in\mathbb{N}$, $u_{t}\in\mathbb{FP}^{m}\subset\mathbb{R}^{m}$ is the action at time $t$, and $y_{t}\in\mathbb{FP}^{o}\subset\mathbb{R}^{o}$ is the sensor (output) measurements at time $t$. As a cyber-physical system, we assume that the system is controlled by a control program $g:\mathbb{FP}^{o}\rightarrow\mathbb{FP}^{m}$. Without loss of generality, any program can be decomposed using the so-called path constraints [25] as:

where $c^{(i)}:\mathbb{FP}^{o}\rightarrow\mathbb{B}$ is the $i$th path constraint of the program $g$ and $g^{(i)}:\mathbb{FP}^{o}\rightarrow\mathbb{FP}^{m}$ is the path function, i.e., the function that is executed at the $i$th path of $g$.

Given a control program $g$ that consists of $k$ paths, we denote by $\texttt{PATH}:\mathbb{FP}^{o}\rightarrow\{1,\ldots,k\}$ the function that returns the path index of an input $y$. That is:

Note that the function PATH is well defined since path constraints are mutually exclusive, and hence, an input $y$ can only be processed by only one path inside the code.

Using this notation, we can now define the cyber trajectory of a system as the index of the control program’s path taken at different time instances as follows.

We are interested in enumerating all cyber trajectories that can lead to physical system trajectories that violate a safety requirement $\varphi$. In this paper, we assume that the safety requirement $\varphi$ is captured by a Signal Temporal Logic (STL) formula. For the formal definition of STL syntax and semantics, we refer the reader to [26]. Using this notation, the problem of interest can be defined as follows.

In other words, a cyber trajectory $\psi_{p}$ is considered a cyber-kinetic vulnerability if there exists an associated trajectory of the physical system $\psi_{x}$ that violates the safety requirement $\varphi$.

While Problem III.2 focuses on finding vulnerabilities in the controller program that lead to violation of safety requirements, we are also interested in generalizing this problem into scenarios when an attacker is capable of manipulating the physical sensor measurements $h(x_{t})$ before it is processed by the control program $g$ [27, 28, 29, 30, 31, 32]. Typically, these sensor manipulations are of relatively small magnitude $\overline{s}$ compared to the sensor noise levels to avoid being detected. That is, we consider the system:

where $s_{t}$ is the physical attack signal at time $t$ with $\|s_{t}\|\leq\overline{s}$. In such a setup, given a trajectory of the physical system $\psi_{x}$ and a trajectory of the physical attack signal $\psi_{s}=\{s_{t}\}_{t=0}^{H}$, the corresponding cyber trajectory $\psi_{p}$ is defined as $\psi_{p}=\{\texttt{PATH}(h(x_{t})+s_{t})\}_{t=0}^{H}$.

As pictorially shown in Figure 3, given a binary-level control program $g$, our first step is to extract the path constraints $c^{(1)},\ldots,c^{(k)}$ from $g$. To this end, we use off-the-shelf symbolic code execution engines that can extract SMT constraints representing different paths in the control program (Line 5 in Algorithm 1).

The next step is to analyze the extracted paths to find cyber trajectories that can lead to cyber-kinetic vulnerabilities. Nevertheless, and as motivated in Figure 2, the number of cyber trajectories increases exponentially as a function of the number of paths $k$ and the length of the trajectory $H$. In particular, for trajectories of length $H$ and a control program with $k$ paths, our tool is now challenged with analyzing all $k^{H}$ possible cyber trajectories. To harness the combinatorial explosion, we resort to an iterative Counter-Example Guided Abstraction Refinement (CEGAR) process. In this process, cyber trajectories go through several levels of abstraction that will be iteratively refined later in the process to ensure coverage of all possible cyber trajectories.

The first level of abstraction is to consider the “range” of the control signal $u$ that each program path can produce. Without loss of generality, and for the sake of notation, we will assume that control signal $u$ is scalar — nevertheless, our framework is designed to support multidimensional control signals. For such a case, the maximum and minimum of the control signal $u$ within the $i$th path $p$ of $g$, denoted by $\overline{u}_{p}$ and $\underline{u}_{p}$, can be computed by solving the following optimization problem:

Thanks to the current advances in SMT solvers (e.g., Z3 [33]), one can efficiently solve the optimization problem above to obtain the path ranges $R=\{(\overline{u}_{1},\underline{u}_{1}),\ldots,(\overline{u}_{k},\underline{u}_{k})\}$. Given these path ranges, we can now abstract a cyber trajectory using the ranges of control signals at each time step. That is, for any cyber trajectory $\psi_{p}=\{p_{t}\}_{t=0}^{H}$, the corresponding “range” of control signals within this trajectory is defined as:

The second level of abstraction combines multiple cyber trajectories into an “abstract cyber trajectory”. Such abstraction is done by combining the ranges of control signals across different cyber trajectories.

In particular, the first iteration of Rampo abstracts all cyber trajectories into one. The ranges of control signals along all cyber trajectories are used to augment the STL-based safety requirements $\varphi$ as follows:

The logical negation $\lnot$ is motivated by the fact that falsification engines aim to find a violation of $\phi$, and hence, the encoding above forces the control signal to be within the ranges of interest.

Next, Rampo uses these abstractions to guide a system falsification engine. System falsification refers to a set of tools that take as input a dynamical system $f$ and an STL formula $\phi$ and find a physical-level trajectory $\psi_{x}=\{x_{t}\}_{t=0}^{H}$ that violates $\phi$, i.e.,

If $\overline{\psi}_{x}$ is not empty, then the computed trajectory $\psi_{x}$ is guaranteed to violate the STL requirements $\phi$, i.e., $\psi_{x}\not\models\phi$. Note that the bar in $\overline{\psi}_{x}$ is used to emphasize the fact that $\overline{\psi}_{x}$ is not a concrete vulnerability since it was computed based on the abstraction of cyber trajectories using control signal ranges (Lines 11-12, Algorithm 1).

Since the abstraction of cyber trajectories using range of control signals is a sound approximation, then whenever $\overline{\psi}_{x}$ is empty, one can conclude that the system is free from all cyber-kinetic vulnerabilities. On the other hand, if $\overline{\psi}_{x}$ is not empty, then our tool will extract the cyber trajectory corresponding to $\overline{\psi}_{x}$ as follows:

We refer to $\overline{\psi}_{p}$ as an abstract vulnerability (Lines 13-16, Algorithm 1).

Since the abstract vulnerability $\overline{\psi}_{p}$ is extracted from a physical trajectory that violated the safety requirements, it is likely a concrete vulnerability may exist in the system. To that end, Rampo will explore $\overline{\psi}_{p}$ by iteratively refining the control signal ranges around $\overline{\psi}_{p}$. In particular, Rampo provides two different strategies for the iterative abstraction refinement of $\overline{\psi}_{p}$ that are explained in detail in Section V and Algorithm 1. These abstraction refinement approaches can either find concrete cyber vulnerabilities $\psi_{p}$, find other abstract cyber trajectories $\overline{\psi}^{*}_{p}$ that need to be subsequently refined, or certify that a set of abstract trajectories $\underline{\psi}_{p}$ will not lead to a vulnerability (Lines 19-23, Algorithm 1).

Finally, Rampo will search for new abstract vulnerabilities over the unexplored abstract trajectories. This is achieved by forcing the falsification engine to search over the control signal ranges that are not considered yet by encoding them in the STL formula as:

where $\varphi$ is the original safety requirements and $\underline{\Psi}_{p}$ is the set of the abstract trajectories explored so far (Lines 25-30, Algorithm 1).

By refining the abstractions of the explored cyber vulnerabilities and searching over unexplored abstract trajectories, Rampo will iteratively identify new abstract cyber trajectories and search for concrete vulnerabilities within those abstract cyber trajectories until all cyber trajectories are covered. This process is summarized in Algorithm 1 and Figure 3.

The soundness and completeness of Algorithm 1 relies on the soundness and completeness of the falsification engine (Falsify). This follows from the fact that Rampo uses sound abstraction of the cyber trajectories and relies on the falsification engine to discard abstract trajectories when no abstract physical-level trajectory violates the safety requirements. Unfortunately, off-the-shelf falsification engines rely on stochastic optimization to reason about non-convex constraints, and hence, these falsification engines are sound but not complete, rendering Rampo to be sound but not complete.

Algorithm 1 can be directly extended to enumerate cyber-physical-kinetic vulnerabilities. As captured by Problem III.3, the main difference between cyber-kinetic vulnerabilities and cyber-physical-kinetic vulnerabilities is the need to find additional sensor manipulation signals $\{s_{t}\}_{t=0}^{H}$ that can lead to violation of safety requirements. To that end, one can treat the signal $s$ as an additional input signal to the falsification engine and rely on the falsification engine to simultaneously search for $\psi_{x}$ and $\psi_{s}$. An example of this extension is provided in the numerical examples in Section VI-D.

In the first abstraction refinement approach, given an abstract vulnerability $\overline{\psi}_{p}$ of length $l\leq H$, our tool concretizes/refines the ranges around this specific $\overline{\psi}_{p}$. This can be encoded in the STL formula $\phi$ as follows:

The falsification engine then uses $\phi$ to search for a trajectory of the physical system. Note that even if a trajectory is found, this does not account for a concrete vulnerability since the behavior of the control program $g$ is still abstracted as a range of control signals (recall the two levels of abstractions in Section 4.1). This requires another call to the Falsification engine, this time using the physical model $f$ augmented with the control program $g$ constrained to the path constraints $c^{(\texttt{Element}(\overline{\psi}_{p},1))},\ldots,c^{(\texttt{Element}(\overline{\psi}_{p},l))}$. If a concrete vulnerability $\psi_{x}$ was found, then it is added to the set of concrete cyber-kinetic vulnerabilities. Regardless of whether a concrete vulnerability is found, the abstract trajectory $\overline{\psi}_{p}$ is added to the set of explored trajectories $\underline{\psi}_{p}$ (Lines 2-11, Algorithm 2).

If a concrete vulnerability is not found by the process above, we iteratively reduce the abstraction refinement by removing the range constraints in $\phi$ (as pictorially illustrated in Figure 4). That is, starting from $i=1$ until $i=l$, we will iteratively call the falsification engine to find a trajectory of the physical system that violates the safety requirements by encoding these range constraints in $\phi$ as follows:

Whenever the falsification engine fails to find a violation of $\phi$ (for $i=1,\ldots,l$), the truncated version of $\overline{\psi}_{p}$ (i.e., $\{p_{t}\}_{t=0}^{i}$) is added to the set of explored trajectories $\underline{\psi}_{p}$. Similarly, whenever the falsification engine finds an abstract vulnerability, the newly discovered abstract vulnerability is added to $\overline{\psi}^{*}_{p}$. This process is summarized in Figure 4 and Algorithm 2.

While Algorithm 2 relaxes the range constraints along $\overline{\psi}_{p}$ in a linear fashion, our second approach for abstraction refinement is to relax the range constraints in a binary-search fashion. That is, we replace the loop in Step 14 of Algorithm 2 with one that starts with $i=l/2$ and then selects the next value of $i$ based on the success/failure of finding an abstract vulnerability. Compared to the linear-search-based approach, this binary search is more suitable for traversing trees with high values of $l$ (hence the height of the tree being explored by the abstraction refinement).

We start by comparing Rampo to S-TaLiRo, one of the state-of-the-art CPS falsification tools. While we use S-TaLiRo internally within Rampo to find falsifying trajectories of the open-loop system $f$ (up to specified path constraints), S-TaLiRo can also be used to falsify the entire closed-loop system (the dynamical system $f$ along with the controller $g$). In this experiment, we show that analyzing the controller $g$ away from the dynamical system $f$ (using our approach) will lead to identifying a more significant number of vulnerabilities in the system compared to the as-is use of S-TaLiRo.

To that end, we consider a model of a drone moving vertically. We use a simple double integrator dynamical system $f$ to capture the vertical movement of the drone. The safety requirement is for the drone’s position to be always below $0.98$. We also consider the following control program, which implements a gain scheduling controller:

Note that S-TaLiRo aims to find only one falsifying trajectory while our aim in Problem III.2 is to enumerate all possible cyber-kinetic vulnerabilities. To that end, we ran S-TaLiRo 50 times with random seeds to force it to explore different vulnerabilities. We ran Rampo while restricting the number of calls to the Falsify function to 50. Our experiments show that Rampo was able to identify 14 cyber-kinetic vulnerabilities while S-TaLiRo-alone was able to find only 9 of those vulnerabilities. The execution time of Rampo was $191$ seconds, while for S-TaLiRo-alone was $147$ seconds. This result shows one of the main benefits of combining falsification and code analysis tools. By splitting the analysis between the two domains (cyber and physical domains), one can achieve better coverage of the different cyber trajectories in the system.

Our second experiment aims to evaluate the scalability of our tool with respect to the number of states in the dynamical model $f$. To that end, we use the same control program in Listing 1, and we vary the number of integrators in the system from $1$ to $10$.

To obtain a baseline for comparison, we perform an exhaustive search by partitioning the space of initial states (used to find falsifying trajectories by S-TaLiRo) into hypercubes. By constraining S-TaLiRo to find falsifying trajectories that start from different initial states, we can increase the number of identified vulnerabilities. Nevertheless, and as shown in Figure 5 (left), this brute force search scales poorly as the number of states increases and as the granularity of the partitioning increases.

On the other hand, as shown in Figure 5 (middle and right), our tool with the linear- and binary-search-based abstraction refinement shows a similar trend to the baseline in terms of their ability to identify cyber-kinetic vulnerabilities while avoiding the exponential increase in the execution time. In general, the execution time of Rampo remained almost constant as the number of states increased. We repeated the same experiment multiple times while changing some of the internal parameters to the Falsify function on Rampo (which as explained above, is implemented using S-TaLiRo but with open-loop dynamics and path constraints). In particular, different plots in Figure 5 show different settings where the number before the multiplication operator indicates the number of optimization steps taken in one falsification, and the latter numbers are the number of calls to S-TaLiRo per one call to the Falsify function.

For the same number of identified vulnerabilities, Rampo achieved a speedup that ranges from $3\times$ to $98\times$.

In this experiment, we study the scalability of Rampo as we increase the length of the cyber trajectories $H$. Recall that increasing $H$ results in an exponential growth in the number of cyber trajectories that need to be explored. Figure 6 (top) shows the number of identified vulnerabilities as $H$ increases for both the linear- and binary-search-based abstraction refinement approaches. As expected, the number of vulnerabilities increases as $H$ increases. Moreover, the number of vulnerabilities found by the linear- and binary-search-based abstraction refinement approaches are comparable among the different settings for the Falsify function.

On the other hand, 6 (bottom) shows the execution time for both the linear- and binary-search-based abstraction refinement approaches. As expected, the benefits of the binary search start to grow as the depth $H$ increases, resulting in an average of $2\times$ speedup for the binary-search-based abstraction refinement compared to the linear-search-based abstraction refinement approach. Moreover, and most importantly, the execution time of both the linear- and binary-search-based abstraction refinement approaches does not increase exponentially with $H$, albeit with the exponential growth in the number of cyber trajectories. We hypothesize that this pattern is due to the CEGAR approach used by Rampo  which can reason about several cyber trajectories simultaneously, which harnesses the exponential growth in the number of cyber trajectories.

In this experiment, we evaluate the ability of Rampo to identify both cyber-kinetic and cyber-physical-kinetic vulnerabilities in complex systems. To that end, we use a model for a vehicle control signal (shown in Figure 7). The model has two inputs, $Speed$ and $RPM$, and the one output, $Throttle$. The control program for this model is shown in Listing 2 which has a total of $k=4$ paths. The safety requirement $\varphi$ is “Either the $Speed$ or the $RPM$ is below a specified threshold.”

We started by searching for cyber-kinetic vulnerabilities using Rampo. Figure 8 shows the only cyber-kinetic vulnerability found by the binary-search-based abstraction refinement approach. This vulnerability corresponds to the cyber trajectory $(p_{0}=1,p_{1}=4,p_{2}=4,p_{3}=4)$. The corresponding trajectories of $\psi_{x_{1}}$ and $\psi_{x_{2}}$ are shown in Figure 8 where cross the bars that indicate corresponding paths.

Next, we examine whether a small amount of physical attack signals can lead to other kinetic attacks, i.e., can a small amount of physical attack signal force the control program to go through a different cyber trajectory that can lead to a new kinetic attack? To that end, we restrict the physical attack signal $\psi_{s}$ to be $\leq 2.0\%$ of the original sensor signals ($Speed$ and $RPM$). We considered three different configurations. In the first one, the attacker can change only $Speed$, in the second one, the attacker can only change $RPM$, while in the last configuration, the attacker can affect both $Speed$ and $RPM$.

For the first two settings (attacking either $Speed$ alone or $RPM$ alone), our tool was not able to find any new cyber trajectory that can lead to vulnerability (other than the one shown in Figure 8). On the other hand, by allowing the attacker to corrupt both the $Speed$ and $RPM$, our tool identified another cyber trajectory that $(p_{0}=1,p_{1}=4,p_{2}=2,p_{3}=4)$ that can lead to vulnerabilities. The cyber-physical-kinetic vulnerability is shown in Figure 9.

By analyzing the third time step in Figure 9, one can notice that the $\psi_{x_{2}}$ trajectory is close to violating the constraints of $p=2$. That is, a small perturbation in the sensor signal (either intentional by an attacker or by noise) can force the code to execute a different path in the control program $g$. This shows the effectiveness of our tool to identify these corner cases, which can be used to fix the control program to be more robust and secure.