SMT-Based Observer Design for Cyber-Physical Systems Under Sensor Attacks
Yasser Shoukry, Michelle Chong, Masashi Wakaiki, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Sanjit Seshia, Joao P. Hespanha, Paulo Tabuada

Citation
Yasser Shoukry, Michelle Chong, Masashi Wakaiki, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Sanjit Seshia, Joao P. Hespanha, Paulo Tabuada. "SMT-Based Observer Design for Cyber-Physical Systems Under Sensor Attacks". ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2016), 11, April, 2016.

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 a multi-modal observer 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, obtained out of potentially corrupted sensors, 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.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Yasser Shoukry, Michelle Chong, Masashi Wakaiki, Pierluigi
  Nuzzo, Alberto Sangiovanni-Vincentelli, Sanjit Seshia, Joao
  P. Hespanha, Paulo Tabuada. <a
  href="http://www.terraswarm.org/pubs/735.html"
  >SMT-Based Observer Design for Cyber-Physical Systems
  Under Sensor Attacks</a>, ACM/IEEE International
  Conference on Cyber-Physical Systems (ICCPS 2016), 11,
  April, 2016.

• Plain text

  Yasser Shoukry, Michelle Chong, Masashi Wakaiki, Pierluigi
  Nuzzo, Alberto Sangiovanni-Vincentelli, Sanjit Seshia, Joao
  P. Hespanha, Paulo Tabuada. "SMT-Based Observer Design
  for Cyber-Physical Systems Under Sensor Attacks".
  ACM/IEEE International Conference on Cyber-Physical Systems
  (ICCPS 2016), 11, April, 2016.

• BibTeX

  @inproceedings{ShoukryChongWakaikiNuzzoSangiovanniVincentelliSeshia16_SMTBasedObserverDesignForCyberPhysicalSystemsUnder,
      author = {Yasser Shoukry and Michelle Chong and Masashi
                Wakaiki and Pierluigi Nuzzo and Alberto
                Sangiovanni-Vincentelli and Sanjit Seshia and Joao
                P. Hespanha and Paulo Tabuada},
      title = {SMT-Based Observer Design for Cyber-Physical
                Systems Under Sensor Attacks},
      booktitle = {ACM/IEEE International Conference on
                Cyber-Physical Systems (ICCPS 2016)},
      day = {11},
      month = {April},
      year = {2016},
      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 a multi-modal observer 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, obtained out of potentially
                corrupted sensors, 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.},
      URL = {http://terraswarm.org/pubs/735.html}
  }
  

Posted by Elizabeth Coyne on 8 Feb 2016.
Groups: tools