TerraSwarm funded paper, "
SMT-Based Observer Design for Cyber-Physical Systems Under Sensor Attacks," has received best paper award at the IEEE International Conference on Cyber-Physical Systems (
ICCPS 2016), held as part of CPS Week in Vienna, Austria, from April 11-14 2016.
The paper states: This work was partially sponsored by the NSF award 1136174, by DARPA under agreement number FA8750-12-2-0247, by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA, and by the NSF project ExCAPE: Expeditions in Computer Augmented Program Engineering (award 1138996 and 1139138.)
Yasser Shoukry, Michelle Chong, Masashi Wakaiki,
Pierluigi Nuzzo,
Alberto Sangiovanni-Vincentelli,
Sanjit A. 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), Vienna, Austria, April 11, 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.
TerraSwarm funded PI Bjoern Hartmann has been named as the interim faculty director of the Jacobs Institute for Design Innovation at UC Berkeley. PI Bjoern Hartmann is an Assistant Professor in the EECS Department and has served as the chief technology officer for the Jacobs Institute for Design Innovation since its inception. His research on Human-Computer Interaction centers on novel design,
prototyping, and implementation tools for the era of post-personal
computing. 
The Jacobs Institute for Design Innovation works to educate top innovators at the intersection of design and technology, and to provide students with opportunities for hands-on experiences working in interdisciplinary teams to address real world problems. Focusing on human-centered engineering, the Jacobs Institute for Design Innovation facilitates an increased role for design in undergraduate engineering education at UC Berkeley.
