Imhotep-SMT
A novel SMT-based solver for secure state estimation
Tutorial: Securing an Unmanned Ground Vehicle
In this tutorial, we are going to demonstrate how to use Imhotep-SMT to secure the control of an unmanned ground vehicle (UGV) against attacks to its sensors. The UGV has two state variables: the position $x(t)$ and the velocity $v(t)$. A model for the time evolution of these variables, as derived using energy conservation laws, can be expressed as follows: \begin{equation*} \begin{bmatrix} \dot{x} \\ \dot{v} \end{bmatrix} = \begin{bmatrix}0 & 1\\0 & \frac{-B}{M} \end{bmatrix} \begin{bmatrix} x(t) \\ v(t) \end{bmatrix} + \begin{bmatrix} 0 \\ \frac{1}{M}\end{bmatrix} F(t), \end{equation*} where $M$ and $B$ denote, respectively, the mechanical mass and the translational friction coefficients, while $F(t)$ is the input force to the UGV at time $t$. The UGV is equipped with a GPS sensor, which measures its position, and two motor encoders, which measure the translational velocity. The resulting output equation is: \begin{equation*} \begin{bmatrix} y_{\text{GPS}}(t) \\ y_{\text{right encoder}}(t) \\ y_{\text{left encoder}}(t) \end{bmatrix} = \begin{bmatrix} 1 & 0 \\ 0 & 1 \\ 0 & 1 \end{bmatrix} \begin{bmatrix} x(t) \\ v(t) \end{bmatrix} + \begin{bmatrix}\psi_{\text{GPS}}(t) \\ \psi_{\text{right encoder}}(t) \\ \psi_{\text{left encoder}}(t)\end{bmatrix}, \end{equation*} where $\psi$ is the measurement noise at each sensor. These sensor measurements are used to estimate the states of the UGV. However, we assume that an adversarial attacker is manipulating one of the UGV sensors in order to deceive the state estimator. In the remaining of this tutorial, we will show how Imhotep-SMT can be used to detect the existence of such an attacker, and estimate the actual state of the UGV.
The Matlab files for this tutorial can be downloaded from here.
Step 0: Download Imhotep-SMT
- Download the latest version of Imhotep-SMT from github as a zip file.
- Extract the contents of the zip file to "folder_path/ImhotepSMT".
- Open Matlab, add "folder_path/ImhotepSMT/" to your Matlab path (e.g. by selecting "File->Set path->Add folder" from the main Menu in Matlab).
Step 1: Initialize the Solver
From the Matlab terminal, create a new instance of the Imhotep-SMT solver as follows:
smt = ImhotepSMT();
Step 2: Offline Configuration of the Solver
Imhotep-SMT must be configured offline by specifying:
- A discrete-time dynamical model of the system in the state space, e.g. by specifying how the state evolves over time as well as how the sensor measurements are related to the system state.
- The maximum number of sensors that can be under attack for the estimation to be theoretically feasible.
- A set of sensors which is known to be attack-free a priori (this is an optional parameter).
- The upper bound on the magnitude (norm) of the measurement noise.
1- Discrete-time dynamic model. Since our solver only accepts discrete-time models, we start by discretizing the UGV model. For $M = 0.8$ and $B = 1$ and a sampling time $T_s = 100 ms$, we obtain: \begin{equation*} \begin{bmatrix} x(t+1) \\ v(t+1) \end{bmatrix} = \begin{bmatrix}1.0000 & 0.0099\\0 & 0.9876 \end{bmatrix} \begin{bmatrix} x(t) \\ v(t) \end{bmatrix} + \begin{bmatrix} 0.0001 \\ 0.0124\end{bmatrix} F(t), \end{equation*} which can be specified in Matlab as:
A = [1 0.0099; 0 0.9876]; B = [0.0001; 0.0124]; C = [1 0; 0 1; 0 1]; ugv = ss(A,B,C,0,0.001);
2- Maximum number of sensors that can be under attack. As discussed above, the attacker can attack only one sensor. This can be specified as follows:
max_sensors_under_attack = int8(1);
3- Set of safe sensors. To show how Imhotep-SMT analyzes the system specification, we initially assume that the attacker can attack any of the three sensors. We will then show how Imhotep-SMT can actually identify which sensors must be secured for the UGV to operate safely.
safe_sensors = [];
4- Upper bound on measurement noise. In general, each sensor measurement suffers from noise. The bound on this noise is an important parameter which affects the capability of Imhotep-SMT to distinguish between noise and attack. In this example, we assume that all sensors are ideal and are not affected by noise, as follows:
noise_bound = [0; 0; 0];
We can now initialize the SMT solver using the init() method as:
smt.init(ugv, max_sensors_under_attack, safe_sensors, noise_bound);
Imhotep-SMT will check the security index for the system, and make sure it matches the specified maximum number of sensors under attack. In this case, the following report is generated:
The maximum number of attacks specified by the user is: 1 Theoretical upper bound on maximum number of attacks is: 0 ERROR: System structure does not match the maximum number of attacked sensors specified by the user Sensors that can improve system security are: Sensor#1
The generated report warns the user that the specified system can not tolerate any attacks on its sensors. The structure of the system is such that a corruption to the sensor measurements can preclude any security algorithm from detecting the attack. In other words, if all the sensors are allowed to be attacked, it is theoretically not possible to detect the attack. To avoid this situation, Imhotep-SMT suggests that the security level of the system can be potentially increased if the GPS signal (sensor 1) is not attacked. Therefore, we re-define the set of safe sensors as:
safe_sensors = [1];
and initialize the solver again as follows:
smt.init(ugv, max_sensors_under_attack, safe_sensors, noise_bound);
The maximum number of attacks specified by the user is: 1 Theoretical upper bound on maximum number of attacks is: 2 Disclaimer: Correction of the solver outputs is guaranteed if and only if the system passes the s-sparse observability test. To run this combinatorial test, call the checkObservabilityCondition()
The final step to complete the offline configuration phase consists in checking the sparse observability condition. This is the necessary and sufficient condition to guarantee the correctness of the results. Depending on the structure of the system, the test may take some time. This step can be skipped if the user knows that the sparse observability condition holds for the specified system.
smt.checkObservabilityCondition();
INFO: The sparse observability test ensures that the system is observable after removing every combination of 2 sensors. This requires checking the observability of 1 combinations ... This may take some time Iteration number 1 out of 1 combinations ... PASS! Sparse observability condition passed! Solver is ready to run!
Step 2- Online State Estimation
To detect the attack, we need to provide the solver with the input and output signals
of the system to be controlled, as shown in the figure below.
Since the solver is implemented within Matlab, we need to use the capabilities embedded in
the "Real-time toolbox" of Matlab to deploy it on a real application while
guaranteeing real-time operation. However, for the purpose of this tutorial, we simply
use Matlab to simulate the dynamical system as follows.
x = randn(2,1); %unknown initial condition
attacked_sensor_index = 2; % the attacker chooses to attack the second sensor.
for t = 1 : 1000 % simulate the system for 1000 time steps
y = C*x; % the system measurements
% the attacker corrupts the second sensor with random data
y(attacked_sensor_index) = y(attacked_sensor_index) + 50*randn(1);
F = 1; % the force supplied to the UGV
x = A*x + B*F; % simulate the system
[xhat, sensor_under_attack] = smt.addInputsOutputs(F, y);
error = norm(xhat - x)
sensor_under_attack
end
Except for the first iteration, the code above results into the following output at each iteration of the simulation:
error =
8.8818e-16
sensor_under_attack =
2
In general, for the first $n-1$ iterations (where $n$ is the number of state variables of the system), the output of the solver may be incorrect since the information stored is not enough to correctly compute the state and determine which sensors are under attack.