Seminars‎ > ‎

SMT

Abstract

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 three extensions to
handle noisy measurements, recursive implementations (data over
infinite windows) and nonlinear dynamics.

Comments