Secure State Estimation For Cyber Physical Systems Under Sensor Attacks: A Satisfiability Modulo Theory Approach

TL;DR

This paper introduces an efficient Satisfiability-Modulo-Theory based algorithm for detecting and mitigating sensor attacks in linear dynamical systems, providing guarantees and demonstrating its effectiveness through simulations and application to unmanned vehicle control.

Contribution

It presents a novel SMT-based method for secure state estimation that guarantees soundness and completeness, improving robustness against sensor attacks.

Findings

Algorithm effectively isolates compromised sensors.

Provides formal guarantees on detection accuracy.

Demonstrates practical application to unmanned vehicle control.

Abstract

We address the problem of detecting and mitigating the effect of malicious attacks to the sensors of a linear dynamical system. We develop a novel, efficient algorithm that uses a Satisfiability-Modulo-Theory approach to isolate the compromised sensors and estimate the system state despite the presence of the attack, thus harnessing the intrinsic combinatorial complexity of the problem. By leveraging results from formal methods over real numbers, we provide guarantees on the soundness and completeness of our algorithm. We then report simulation results to compare its runtime performance with alternative techniques. Finally, we demonstrate its application to the problem of controlling an unmanned ground vehicle.