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
For additional information, see the Publications FAQ or contact webmaster at terraswarm org.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.