PRECISE Seminar: Secure State Estimation for CPS Under Sensor Attacks - A Satisfiability Modulo Theory Approach

Motivated by the need to secure critical infrastructure against sensor attacks, in this talk I will focus on a problem known as "secure state estimation”. It consists of estimating the state of a dynamical system when a subset of its sensors is arbitrarily corrupted by an adversary. Although of critical importance, this problem is combinatorial in nature since the subset of attacked sensors in unknown. Previous work in this area can be classified into two broad categories. The first category is based on numerical optimization techniques. These techniques are well suited to handle the continuous part of the problem, estimating the real-valued variable describing the sate, if the combinatorial part of the problem has been solved. The second category is based on Boolean reasoning which is well suited to handle the combinatorial part of the problem, if the continuous part of the problem has been solved. However, since we need to simultaneously solve the combinatorial and the continuous part of the secure state estimation problem, the existing approaches result in algorithms with worst case exponential time complexity.

In this talk, I will present a novel and efficient algorithm for the secure state estimation problem that uses the lazy SMT approach in order to combine the power of both SAT solving as well as convex optimization. While SAT solving is used to perform the combinatorial search, convex optimization techniques are used to reason more efficiently about the real-valued state of the system and/or generating theory lemmas explaining conflicts in the combinatorial search. We show that by splitting the reasoning between the two domains (Booleans and Reals) and intermixing a powerful tool from each domain, we obtain a new suite of tools that scales more favorably compared to the previous techniques. I will start by discussing the simplest case when the underlying dynamics are linear, sensors are perfect (noise-less), and only data collected over a finite window is considered. I will then move forward by showing several extensions to handle noisy measurements, recursive implementations (data over infinite windows) and nonlinear dynamics.