TY - GEN
T1 - Stealthy attacks formalized as STL formulas for Falsification of CPS Security
AU - Chandratre, Aniruddh
AU - Acosta, Tomas Hernandez
AU - Khandait, Tanmay
AU - Pedrielli, Giulia
AU - Fainekos, Georgios
N1 - Funding Information:
This work is supported by the DARPA ARCOS program under contract FA8750-20-C-0507.
Publisher Copyright:
© 2023 Copyright held by the owner/author(s). Publication rights licensed to ACM.
PY - 2023/5/9
Y1 - 2023/5/9
N2 - We propose a framework for security vulnerability analysis for Cyber-Physical Systems (CPS). Our framework imposes only minimal assumptions on the structure of the CPS. Namely, we consider CPS with feedback control loops, state observers, and anomaly detection algorithms. Moreover, our framework does not require any knowledge about the dynamics or the algorithms used in the CPS. Under this common CPS architecture, we develop tools that can identify vulnerabilities in the system and their impact on the functionality of the CPS. We pose the CPS security problem as a falsification (or Search Based Test Generation (SBTG)) problem guided by security requirements expressed in Signal Temporal Logic (STL). We propose two different categories of security requirements encoded in STL: (1) detectability (stealthiness) and (2) effectiveness (impact on the CPS function). Finally, we demonstrate in simulation on an inverted pendulum and on an Unmanned Aerial Vehicle (UAV) that both specifications are falsifiable using our SBTG techniques.
AB - We propose a framework for security vulnerability analysis for Cyber-Physical Systems (CPS). Our framework imposes only minimal assumptions on the structure of the CPS. Namely, we consider CPS with feedback control loops, state observers, and anomaly detection algorithms. Moreover, our framework does not require any knowledge about the dynamics or the algorithms used in the CPS. Under this common CPS architecture, we develop tools that can identify vulnerabilities in the system and their impact on the functionality of the CPS. We pose the CPS security problem as a falsification (or Search Based Test Generation (SBTG)) problem guided by security requirements expressed in Signal Temporal Logic (STL). We propose two different categories of security requirements encoded in STL: (1) detectability (stealthiness) and (2) effectiveness (impact on the CPS function). Finally, we demonstrate in simulation on an inverted pendulum and on an Unmanned Aerial Vehicle (UAV) that both specifications are falsifiable using our SBTG techniques.
KW - CPS Security
KW - Falsification
KW - Signal Temporal Logic
KW - Test Generation
UR - http://www.scopus.com/inward/record.url?scp=85160525532&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85160525532&partnerID=8YFLogxK
U2 - 10.1145/3575870.3587122
DO - 10.1145/3575870.3587122
M3 - Conference contribution
AN - SCOPUS:85160525532
T3 - HSCC 2023 - Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, Part of CPS-IoT Week
BT - HSCC 2023 - Proceedings of the 26th ACM International Conference on Hybrid Systems
PB - Association for Computing Machinery, Inc
T2 - 26th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2023, Part of CPS-IoT Week 2023
Y2 - 10 May 2023 through 12 May 2023
ER -