Secure State Estimation for Cyber Physical Systems under Sensor Attacks: A Satisfiability Modulo Theory Approach

Yasser Shoukry, Alberto Puggelli, Pierluigi Nuzzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, and Paulo Tabuada. Secure State Estimation for Cyber Physical Systems under Sensor Attacks: A Satisfiability Modulo Theory Approach. IEEE Transactions on Automatic Control, 62(10):4917–4932, 2017.

Download

[pdf] 

Abstract

Secure state estimation is the problem of estimating the state of a dynamical system from a set of noisy and adversarially-corrupted measurements. Intrinsically a combinatorial problem, secure state estimation has been traditionally addressed either by brute force search, suffering from scalability issues, or via convex relaxations, using algorithms that can terminate in polynomial time but are not necessarily sound. In this paper, we present a novel algorithm that uses a satisfiability modulo theory approach to harness the complexity of secure state estimation. We leverage results from formal methods over real numbers to provide guarantees on the soundness and completeness of our algorithm. Moreover, we discuss its scalability properties, by providing upper bounds on the runtime performance. Numerical simulations support our arguments by showing an order of magnitude decrease in execution time with respect to alternative techniques. Finally, the effectiveness of the proposed algorithm is demonstrated by applying it to the problem of controlling an unmanned ground vehicle.

BibTeX

@ARTICLE{shoukry-ieeetac17, 
  title    = {Secure State Estimation for Cyber Physical Systems under Sensor Attacks: A Satisfiability Modulo Theory Approach},
  author     = {Yasser Shoukry and Alberto Puggelli and Pierluigi Nuzzo and Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia and Paulo Tabuada},
  journal   = {IEEE Transactions on Automatic Control},
  volume    = {62},
  number    = {10},
  pages     = {4917--4932},
  year      = {2017},
    Abstract = {Secure state estimation is the problem of estimating 
the state of a dynamical system from a set of noisy and 
adversarially-corrupted measurements. Intrinsically a combinatorial 
problem, secure state estimation has been traditionally 
addressed either by brute force search, suffering from scalability 
issues, or via convex relaxations, using algorithms that can 
terminate in polynomial time but are not necessarily sound. In 
this paper, we present a novel algorithm that uses a satisfiability 
modulo theory approach to harness the complexity of secure 
state estimation. We leverage results from formal methods 
over real numbers to provide guarantees on the soundness 
and completeness of our algorithm. Moreover, we discuss its 
scalability properties, by providing upper bounds on the runtime 
performance. Numerical simulations support our arguments by 
showing an order of magnitude decrease in execution time with 
respect to alternative techniques. Finally, the effectiveness of the 
proposed algorithm is demonstrated by applying it to the problem 
of controlling an unmanned ground vehicle.},
}

Generated by bib2html.pl (written by Patrick Riley ) on Tue Apr 24, 2018 09:06:47