SMT-Based Observer Design for Cyber Physical Systems under Sensor Attacks

Yasser Shoukry, Michelle Chong, Masashi Wakiaki, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Sanjit A. Seshia, Joao. P. Hespanha, and Paulo Tabuada. SMT-Based Observer Design for Cyber Physical Systems under Sensor Attacks. In Proceedings of the International Conference on Cyber-Physical Systems (ICCPS), April 2016.
Best Paper Award.

Download

[pdf] 

Abstract

We introduce a scalable observer architecture to estimate the states of a discrete-time linear-time-invariant (LTI) system whose sensors can be manipulated by an attacker. Given the maximum number of attacked sensors, we build on previous results on necessary and sufficient conditions for state estimation, and propose a novel multi-modal Luenberger (MML) observer based on efficient Satisfiability Modulo Theory (SMT) solving. We present two techniques to reduce the complexity of the estimation problem. As a first strategy, instead of a bank of distinct observers, we use a family of filters sharing a single dynamical equation for the states, but different output equations, to generate estimates corresponding to different subsets of sensors. Such an architecture can reduce the memory usage of the observer from an exponential to a linear function of the number of sensors. We then develop an efficient SMT-based decision procedure that is able to reason about the estimates of the MML observer to detect at runtime which sets of sensors are attack-free, and use them to obtain a correct state estimate. We provide proofs of convergence for our algorithm and report simulation results to compare its runtime performance with alternative techniques. Our algorithm scales well for large systems (including up to 5000 sensors) for which many previously proposed algorithms are not implementable due to excessive memory and time requirements. Finally, we illustrate the effectiveness of our algorithm on the design of resilient power distribution systems.

BibTeX

@inproceedings{shoukry-iccps16,
 author = {Yasser Shoukry and Michelle Chong and Masashi Wakiaki and Pierluigi Nuzzo and Alberto Sangiovanni-Vincentelli and Sanjit A. Seshia and Joao. P. Hespanha and Paulo Tabuada},
 title = {SMT-Based Observer Design for Cyber Physical Systems under Sensor Attacks},
 booktitle = {Proceedings of the International Conference on Cyber-Physical Systems (ICCPS)}, 
 OPTpages = "22--31",
 month = "April",
 year = {2016},
 wwwnote = {<b>Best Paper Award</b>.},
 abstract = {We introduce a scalable observer architecture to 
estimate the states of a discrete-time linear-time-invariant (LTI) 
system whose sensors can be manipulated by an attacker. Given 
the maximum number of attacked sensors, we build on previous 
results on necessary and sufficient conditions for state estimation, 
and propose a novel multi-modal Luenberger (MML) observer 
based on efficient Satisfiability Modulo Theory (SMT) solving. We 
present two techniques to reduce the complexity of the estimation 
problem. As a first strategy, instead of a bank of distinct 
observers, we use a family of filters sharing a single dynamical 
equation for the states, but different output equations, to generate 
estimates corresponding to different subsets of sensors. Such an 
architecture can reduce the memory usage of the observer from 
an exponential to a linear function of the number of sensors. 
We then develop an efficient SMT-based decision procedure that 
is able to reason about the estimates of the MML observer to 
detect at runtime which sets of sensors are attack-free, and use 
them to obtain a correct state estimate. We provide proofs of 
convergence for our algorithm and report simulation results to 
compare its runtime performance with alternative techniques. 
Our algorithm scales well for large systems (including up to 5000 
sensors) for which many previously proposed algorithms are not 
implementable due to excessive memory and time requirements. 
Finally, we illustrate the effectiveness of our algorithm on the 
design of resilient power distribution systems.},
}

Generated by bib2html.pl (written by Patrick Riley ) on Thu Jan 12, 2017 16:01:14