Attacking the V: On the resiliency of adaptive-horizon MPC

Ashish Tiwari, Scott A. Smolka, Lukas Esterle, Anna Lukina, Junxing Yang*, Radu Grosu

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings
PublisherSpringer
Pages446-462
Number of pages17
ISBN (Print)9783319681665
DOIs
Publication statusE-pub ahead of print - 27 Sep 2017
Event15th International Conference on Automated Technology for Verification and Analysis, ATVA 2017 - Pune, India
Duration: 3 Oct 20176 Oct 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10482 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference15th International Conference on Automated Technology for Verification and Analysis, ATVA 2017
CountryIndia
CityPune
Period3/10/176/10/17

Fingerprint

Resiliency
Horizon
Controller
Controllers
Game
Flocking
Stochastic Games
Markov Decision Process
Model predictive control
Model Predictive Control
Model checking
Controllability
Transition Probability
Model Checking
Demonstrate
Statistical Model
Attack

Bibliographical note

© 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

Cite this

Tiwari, A., Smolka, S. A., Esterle, L., Lukina, A., Yang, J., & Grosu, R. (2017). Attacking the V: On the resiliency of adaptive-horizon MPC. In Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings (pp. 446-462). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10482 LNCS). Springer. https://doi.org/10.1007/978-3-319-68167-2_29
Tiwari, Ashish ; Smolka, Scott A. ; Esterle, Lukas ; Lukina, Anna ; Yang, Junxing ; Grosu, Radu. / Attacking the V : On the resiliency of adaptive-horizon MPC. Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings. Springer, 2017. pp. 446-462 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{e8216d19e1fe4595992d2491958ebca6,
title = "Attacking the V: On the resiliency of adaptive-horizon MPC",
abstract = "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.",
author = "Ashish Tiwari and Smolka, {Scott A.} and Lukas Esterle and Anna Lukina and Junxing Yang and Radu Grosu",
note = "{\circledC} 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",
year = "2017",
month = "9",
day = "27",
doi = "10.1007/978-3-319-68167-2_29",
language = "English",
isbn = "9783319681665",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "446--462",
booktitle = "Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings",
address = "Germany",

}

Tiwari, A, Smolka, SA, Esterle, L, Lukina, A, Yang, J & Grosu, R 2017, Attacking the V: On the resiliency of adaptive-horizon MPC. in Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10482 LNCS, Springer, pp. 446-462, 15th International Conference on Automated Technology for Verification and Analysis, ATVA 2017, Pune, India, 3/10/17. https://doi.org/10.1007/978-3-319-68167-2_29

Attacking the V : On the resiliency of adaptive-horizon MPC. / Tiwari, Ashish; Smolka, Scott A.; Esterle, Lukas; Lukina, Anna; Yang, Junxing; Grosu, Radu.

Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings. Springer, 2017. p. 446-462 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10482 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Attacking the V

T2 - On the resiliency of adaptive-horizon MPC

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 contribution

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

ER -

Tiwari A, Smolka SA, Esterle L, Lukina A, Yang J, Grosu R. Attacking the V: On the resiliency of adaptive-horizon MPC. In Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings. Springer. 2017. p. 446-462. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-68167-2_29