Abstract
We present a controller synthesis algorithm for a reach-avoid problem in the presence of adversaries. Our model of the adversary abstractly captures typical malicious attacks envisioned on cyber-physical systems such as sensor spoofing, controller corruption, and actuator intrusion. After formulating the problem in a general setting, we present a sound and complete algorithm for the case with linear dynamics and an adversary with a budget on the total L2-norm of its actions. The algorithm relies on a result from linear control theory that enables us to decompose and compute the reachable states of the system in terms of a symbolic simulation of the adversary-free dynamics and the total uncertainty induced by the adversary. With this decomposition, the synthesis problem eliminates the universal quantifier on the adversary's choices and the symbolic controller actions can be effectively solved using an SMT solver. The constraints induced by the adversary are computed by solving second-order cone programmings. The algorithm is later extended to synthesize state-dependent controller and to generate attacks for the adversary. We present preliminary experimental results that show the effectiveness of this approach on several example problems.
Original language | English (US) |
---|---|
Pages | 53-62 |
Number of pages | 10 |
DOIs | |
State | Published - 2016 |
Event | Symposium and Bootcamp on the Science of Security, HotSos 2016 - Pittsburgh, United States Duration: Apr 19 2016 → Apr 21 2016 |
Conference
Conference | Symposium and Bootcamp on the Science of Security, HotSos 2016 |
---|---|
Country/Territory | United States |
City | Pittsburgh |
Period | 4/19/16 → 4/21/16 |
Keywords
- constraint-based synthesis
- controller synthesis
- cyber-physical security
ASJC Scopus subject areas
- Software
- Human-Computer Interaction
- Computer Vision and Pattern Recognition
- Computer Networks and Communications