Secure State Estimation For Cyber Physical Systems Under Sensor Attacks: A Satisfiability Modulo Theory Approach
This work addresses security issues in cyber-physical systems, such as unmanned vehicles, by providing a method to ensure reliable state estimation under sensor attacks, though it appears incremental as it builds on existing formal methods.
The paper tackles the problem of detecting and mitigating malicious sensor attacks in linear dynamical systems by developing a novel algorithm using a Satisfiability-Modulo-Theory approach to isolate compromised sensors and estimate the system state, with simulation results showing runtime performance comparisons and an application to controlling an unmanned ground vehicle.
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.