×

Verification of approximate opacity for switched systems: a compositional approach. (English) Zbl 1478.93298

Summary: The security in information-flow has become a major concern for cyber-physical systems (CPSs). In this work, we focus on the analysis of an information-flow security property, called opacity. Opacity characterizes the plausible deniability of a system’s secret in the presence of a malicious outside intruder. We propose a methodology of checking a notion of opacity, called approximate opacity, for networks of discrete-time switched systems. Our framework relies on compositional constructions of finite abstractions for networks of switched systems and their approximate opacity-preserving simulation functions. Those functions characterize how close concrete networks and their finite abstractions are in terms of the satisfaction of approximate opacity. We show that such simulation functions can be obtained compositionally by assuming some small-gain type conditions and composing local simulation functions constructed for each switched subsystem separately. Additionally, assuming certain stability property of switched systems, we also provide a technique on constructing their finite abstractions together with the corresponding local simulation functions. Finally, we illustrate the effectiveness of our results through an example.

MSC:

93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
93C55 Discrete-time control/observation systems
93B70 Networked control
93C83 Control/observation systems involving computers (process control, etc.)
93A15 Large-scale systems

References:

[1] Cardenas, A.; Amin, S.; Sinopoli, B.; Giani, A.; Perrig, A., Challenges for securing cyber physical systems, (Workshop on Future Directions in Cyber-Physical Systems Security, 5 (2009))
[2] Ashibani, Y.; Mahmoud, Q. H., Cyber physical systems security: Analysis, challenges and solutions, Comput. Secur., 68, 81-97 (2017)
[3] Mazaré, L., Using unification for opacity properties, (Proceedings of Workshop on Issues in the Theory of Security (2004)), 165-176
[4] Lafortune, S.; Lin, F.; Hadjicostis, C. N., On the history of diagnosability and opacity in discrete event systems, Annu. Rev. Control, 45, 257-266 (2018)
[5] C.N. Hadjicostis, Estimation and Inference in Discrete Event Systems, Springer. http://dx.doi.org/10.1007/978-3-030-30821-6. · Zbl 1436.93002
[6] Ramasubramanian, B.; Cleaveland, W. R.; Marcus, S., Notions of centralized and decentralized opacity in linear systems, IEEE Trans. Automat. Control, 65, 4, 1442-1455 (2019) · Zbl 1533.93053
[7] Ramasubramanian, B.; Cleaveland, R.; Marcus, S. I., Opacity for switched linear systems: Notions and characterization, (Proceedings of the 56th Conference on Decision and Control (2017), IEEE), 5310-5315
[8] An, L.; Yang, G.-H., Opacity enforcement for confidential robust control in linear cyber-physical systems, IEEE Trans. Automat. Control, 65, 3, 1234-1241 (2019) · Zbl 1533.93126
[9] Zhang, K.; Yin, X.; Zamani, M., Opacity of nondeterministic transition systems: A (bi) simulation relation approach, IEEE Trans. Automat. Control, 64, 12, 5116-5123 (2019) · Zbl 1482.93403
[10] Yin, X.; Zamani, M.; Liu, S., On approximate opacity of cyber-physical systems, IEEE Trans. Automat. Control, 66, 4, 1630-1645 (2021) · Zbl 1536.93344
[11] Liu, S.; Yin, X.; Zamani, M., On a notion of approximate opacity for discrete-time stochastic control systems, (American Control Conference (2020), IEEE), 5413-5418
[12] Pola, G.; Pepe, P.; Benedetto, M. D.D., Symbolic models for networks of control systems, IEEE Trans. Automat. Control, 61, 11, 3663-3668 (2016) · Zbl 1359.93039
[13] Meyer, P. J.; Girard, A.; Witrant, E., Compositional abstraction and safety synthesis using overlapping symbolic models, IEEE Trans. Automat. Control, 63, 6, 1835-1841 (2017) · Zbl 1395.93398
[14] Kim, E. S.; Arcak, M.; Zamani, M., Constructing control system abstractions from modular components, (Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week) (2018)), 137-146 · Zbl 1417.93056
[15] Swikir, A.; Zamani, M., Compositional synthesis of finite abstractions for networks of systems: A small-gain approach, Automatica, 107, 11, 551-561 (2019) · Zbl 1429.93143
[16] Mallik, K.; Schmuck, A.; Soudjani, S.; Majumdar, R., Compositional synthesis of finite-state abstractions, IEEE Trans. Automat. Control, 64, 6, 2629-2636 (2019) · Zbl 1482.93263
[17] Swikir, A.; Zamani, M., Compositional synthesis of symbolic models for networks of switched systems, IEEE Control Syst. Lett., 3, 4, 1056-1061 (2019)
[18] Swikir, A.; Zamani, M., Compositional abstractions of interconnected discrete-time switched systems, (18th European Control Conference (2019)), 1251-1256
[19] Pola, G.; De Santis, E.; Di Benedetto, M. D.; Pezzuti, D., Design of decentralized critical observers for networks of finite state machines: A formal method approach, Automatica, 86, 174-182 (2017) · Zbl 1375.93014
[20] Liu, S.; Zamani, M., Compositional synthesis of opacity-preserving finite abstractions for interconnected systems (2020), ArXiv Preprint ArXiv:2004.00131 · Zbl 1478.93018
[21] Liu, S.; Swikir, A.; Zamani, M., Compositional verification of initial-state opacity for switched systems, (59th IEEE Conference on Decision and Control (2020)), 2146-2151
[22] Liberzon, D., Switching in Systems and Control (2003), Birkhäuser Basel · Zbl 1036.93001
[23] Tabuada, P., Verification and Control of Hybrid Systems: A Symbolic Approach (2009), Springer Science & Business Media · Zbl 1195.93001
[24] Tazaki, Y.; Imura, J.-i., Bisimilar finite abstractions of interconnected systems, (International Workshop on Hybrid Systems: Computation and Control (2008), Springer), 514-527 · Zbl 1144.93301
[25] Barequet, G.; Har-Peled, S., Efficiently approximating the minimum-volume bounding box of a point set in three dimensions, J. Algorithms, 38, 1, 91-109 (2001) · Zbl 0969.68166
[26] Yin, X.; Lafortune, S., A new approach for the verification of infinite-step and K-step opacity using two-way observers, Automatica, 80, 162-171 (2017) · Zbl 1370.93174
[27] Saboori, A.; Hadjicostis, C. N., Verification of initial-state opacity in security applications of discrete event systems, Inform. Sci., 246, 115-132 (2013) · Zbl 1320.68119
[28] Angeli, D., A Lyapunov approach to incremental stability properties, IEEE Trans. Automat. Control, 47, 3, 410-421 (2002) · Zbl 1364.93552
[29] Girard, A.; Pola, G.; Tabuada, P., Approximately bisimilar symbolic models for incrementally stable switched systems, IEEE Trans. Automat. Control, 55, 1, 116-126 (2009) · Zbl 1368.93413
[30] Vu, L.; Chatterjee, D.; Liberzon, D., Input-to-state stability of switched systems and switching adaptive control, Automatica, 43, 4, 639-646 (2007) · Zbl 1261.93049
[31] Zamani, M.; Mohajerin Esfahani, P.; Majumdar, R.; Abate, A.; Lygeros, J., Symbolic control of stochastic systems via approximately bisimilar finite abstractions, IEEE Trans. Automat. Control, 59, 12, 3135-3150 (2014) · Zbl 1360.93445
[32] Dashkovskiy, S.; Rüffer, B.; Wirth, F., Small gain theorems for large scale systems and construction of ISS Lyapunov functions, SIAM J. Control Optim., 48, 6, 4089-4118 (2010) · Zbl 1202.93008
[33] Eaves, B. C., Homotopies for computation of fixed points, Math. Program., 3, 1, 1-22 (1972) · Zbl 0276.55004
[34] Ruffer, B. S., Monotone dynamical systems, graphs, and stability of largescale interconnected systems, (Fachbereich 3, Mathematik Und Informatik (2007), UniversitÄt Bremen: UniversitÄt Bremen Germany), (Ph.D. thesis)
[35] Jiang, Z.-P.; Mareels, I. M.; Wang, Y., A Lyapunov formulation of the nonlinear small-gain theorem for interconnected ISS systems, Automatica, 32, 1, 1211-1215 (1996) · Zbl 0857.93089
[36] Saboori, A.; Hadjicostis, C. N., Verification of infinite-step opacity and complexity considerations, IEEE Trans. Automat. Control, 57, 5, 1265-1269 (2012) · Zbl 1369.93110
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.