TY - GEN
T1 - Attacking the V
T2 - 15th International Conference on Automated Technology for Verification and Analysis, ATVA 2017
AU - Tiwari, Ashish
AU - Smolka, Scott A.
AU - Esterle, Lukas
AU - Lukina, Anna
AU - Yang, Junxing
AU - Grosu, Radu
N1 - © Springer International Publishing AG 2017. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-68167-2_29
PY - 2017/9/27
Y1 - 2017/9/27
N2 - Inspired by the emerging problem of CPS security, we introduce the concept of controller-attacker games. A controller-attacker game is a two-player stochastic game, where the two players, a controller and an attacker, have antagonistic objectives. A controller-attacker game is formulated in terms of a Markov Decision Process (MDP), with the controller and the attacker jointly determining the MDP’s transition probabilities. We also introduce the class of controller-attacker games we call V-formation games, where the goal of the controller is to maneuver the plant (a simple model of flocking dynamics) into a V-formation, and the goal of the attacker is to prevent the controller from doing so. Controllers in V-formation games utilize a new formulation of model-predictive control we have developed called Adaptive-Horizon MPC (AMPC), giving them extraordinary power: we prove that under certain controllability conditions, an AMPC controller can attain V-formation with probability 1. We evaluate AMPC’s performance on V-formation games using statistical model checking. Our experiments demonstrate that (a) as we increase the power of the attacker, the AMPC controller adapts by suitably increasing its horizon, and thus demonstrates resiliency to a variety of attacks; and (b) an intelligent attacker can significantly outperform its naive counterpart.
AB - Inspired by the emerging problem of CPS security, we introduce the concept of controller-attacker games. A controller-attacker game is a two-player stochastic game, where the two players, a controller and an attacker, have antagonistic objectives. A controller-attacker game is formulated in terms of a Markov Decision Process (MDP), with the controller and the attacker jointly determining the MDP’s transition probabilities. We also introduce the class of controller-attacker games we call V-formation games, where the goal of the controller is to maneuver the plant (a simple model of flocking dynamics) into a V-formation, and the goal of the attacker is to prevent the controller from doing so. Controllers in V-formation games utilize a new formulation of model-predictive control we have developed called Adaptive-Horizon MPC (AMPC), giving them extraordinary power: we prove that under certain controllability conditions, an AMPC controller can attain V-formation with probability 1. We evaluate AMPC’s performance on V-formation games using statistical model checking. Our experiments demonstrate that (a) as we increase the power of the attacker, the AMPC controller adapts by suitably increasing its horizon, and thus demonstrates resiliency to a variety of attacks; and (b) an intelligent attacker can significantly outperform its naive counterpart.
UR - http://www.scopus.com/inward/record.url?scp=85031422199&partnerID=8YFLogxK
UR - https://link.springer.com/chapter/10.1007%2F978-3-319-68167-2_29
U2 - 10.1007/978-3-319-68167-2_29
DO - 10.1007/978-3-319-68167-2_29
M3 - Conference publication
AN - SCOPUS:85031422199
SN - 9783319681665
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 446
EP - 462
BT - Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings
PB - Springer
Y2 - 3 October 2017 through 6 October 2017
ER -