Imhotep-SMT: A Satisfiability Modulo Theory Solver for Secure State Estimation

Yasser Shoukry, Pierluigi Nuzzo, Alberto Puggelli, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Mani Srivastava, and Paulo Tabuada. Imhotep-SMT: A Satisfiability Modulo Theory Solver for Secure State Estimation. In In 13th International Workshop on Satisfiability Modulo Theories (SMT), July 2015.

Download

[pdf] 

Abstract

This paper presents Imhotep-SMT, a solver for the detection and mitigation of sensor attacks in cyber-physical systems. Imhotep-SMT receives as inputs a description of the physical system in the form of a linear difference equation, the system input (control) signal, and a set of output (sensor) measurements that can be noisy and corrupted by a malicious attacker. The output is the solution of the secure state estimation problem, i.e., a report indicating: (i) the corrupted sensors, and (ii) an estimate of the continuous state of the system obtained from the uncorrupted sensors. Based on this estimate, it is then possible to deploy a control strategy, while being resilient to adversarial attacks. The core of our tool relies on the combination of convex programming with pseudo-Boolean satisfiability solving, following the lazy satisfiability modulo theory paradigm. We provide an empirical evaluation of the tool scalability, and demonstrate its application to attack detection and secure state estimation of electric power grids.

BibTeX

@inproceedings{shoukry-smt15,
  author    = {Yasser Shoukry and Pierluigi Nuzzo and Alberto Puggelli and Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia and Mani Srivastava and Paulo Tabuada},
  title     = {{Imhotep-SMT}: A Satisfiability Modulo Theory Solver for Secure State Estimation},
 booktitle = {In 13th International Workshop on Satisfiability Modulo Theories (SMT)},
 month = "July",
 year = {2015},
 OPTpages = {3--13},
 abstract = {This paper presents Imhotep-SMT, a solver for the detection 
and mitigation of sensor attacks in cyber-physical systems.  
Imhotep-SMT receives as inputs a description of the 
physical system in the form of a linear difference equation, the 
system input (control) signal, and a set of output (sensor) 
measurements that can be noisy and corrupted by a malicious 
attacker. The output is the solution of the secure state estimation 
problem, i.e., a report indicating: (i) the corrupted sensors, and 
(ii) an estimate of the continuous state of the system obtained from 
the uncorrupted sensors. Based on this estimate, it is then possible 
to deploy a control strategy, while being resilient to adversarial 
attacks. The core of our tool relies on the combination of 
convex programming with pseudo-Boolean satisfiability solving, 
following the lazy satisfiability modulo theory paradigm.  
We provide an empirical evaluation of the tool scalability, and 
demonstrate its application to attack detection and secure state 
estimation of electric power grids.},
}

Generated by bib2html.pl (written by Patrick Riley ) on Sun May 01, 2016 00:40:09