Advanced

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

Shoukry, Yasser; Chong, Michelle LU ; Wakaiki, Masashi; Nuzzo, Pierluigi; Sangiovanni-Vincentelli, Alberto L.; Seshia, Sanjit A.; Hespanha, João P. and Tabuada, Paulo (2016) 7th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2016 In 2016 ACM/IEEE 7th International Conference on Cyber-Physical Systems, ICCPS 2016 - Proceedings
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... (More)

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.

(Less)
Please use this url to cite or link to this publication:
author
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
in
2016 ACM/IEEE 7th International Conference on Cyber-Physical Systems, ICCPS 2016 - Proceedings
publisher
Institute of Electrical and Electronics Engineers Inc.
conference name
7th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2016
external identifiers
  • scopus:84979084449
ISBN
9781509017720
DOI
10.1109/ICCPS.2016.7479119
language
English
LU publication?
yes
id
d8199bc8-6f0a-4a62-9da9-e453b5781203
date added to LUP
2017-01-27 11:34:32
date last changed
2017-10-29 04:57:11
@inproceedings{d8199bc8-6f0a-4a62-9da9-e453b5781203,
  abstract     = {<p>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.</p>},
  author       = {Shoukry, Yasser and Chong, Michelle and Wakaiki, Masashi and Nuzzo, Pierluigi and Sangiovanni-Vincentelli, Alberto L. and Seshia, Sanjit A. and Hespanha, João P. and Tabuada, Paulo},
  booktitle    = {2016 ACM/IEEE 7th International Conference on Cyber-Physical Systems, ICCPS 2016 - Proceedings},
  isbn         = {9781509017720},
  language     = {eng},
  month        = {05},
  publisher    = {Institute of Electrical and Electronics Engineers Inc.},
  title        = {SMT-Based Observer Design for Cyber-Physical Systems under Sensor Attacks},
  url          = {http://dx.doi.org/10.1109/ICCPS.2016.7479119},
  year         = {2016},
}