IEEE/CAA Journal of Automatica Sinica
Citation: | Y. Dong, N. Wu, and Z. Li, “State-based opacity verification of networked discrete event systems using labeled Petri nets,” IEEE/CAA J. Autom. Sinica, vol. 11, no. 5, pp. 1274–1291, May 2024. doi: 10.1109/JAS.2023.124128 |
The opaque property plays an important role in the operation of a security-critical system, implying that pre-defined secret information of the system is not able to be inferred through partially observing its behavior. This paper addresses the verification of current-state, initial-state, infinite-step, and K-step opacity of networked discrete event systems modeled by labeled Petri nets, where communication losses and delays are considered. Based on the symbolic technique for the representation of states in Petri nets, an observer and an estimator are designed for the verification of current-state and initial-state opacity, respectively. Then, we propose a structure called an I-observer that is combined with secret states to verify whether a networked discrete event system is infinite-step opaque or K-step opaque. Due to the utilization of symbolic approaches for the state-based opacity verification, the computation of the reachability graphs of labeled Petri nets is avoided, which dramatically reduces the computational overheads stemming from networked discrete event systems.
[1] |
L. Mazaré, “Using unification for opacity properties,” in Proc. Workshop Issues Theory Security, 2004, pp. 165–176.
|
[2] |
J. W. Bryans, M. Koutny, L. Mazaré, and P. Y. Ryan, “Opacity generalised to transition systems,” Int. J. Information Security, vol. 7, no. 6, pp. 421–435, 2008. doi: 10.1007/s10207-008-0058-x
|
[3] |
J. W. Bryans, M. Koutny, and P. Y. Ryan, “Modelling opacity using Petri nets,” Electronic Notes in Theoretical Computer Science, vol. 121, pp. 101–115, 2005. doi: 10.1016/j.entcs.2004.10.010
|
[4] |
A. Saboori and C. N. Hadjicostis, “Notions of security and opacity in discrete event systems,” in Proc. 46th IEEE Conf. Decision and Control, 2007, pp. 5056–5061.
|
[5] |
A. Saboori and C. N. Hadjicostis, “Verification of initial-state opacity in security applications of discrete event systems,” Information Sciences, vol. 246, pp. 115–132, 2013. doi: 10.1016/j.ins.2013.05.033
|
[6] |
A. Saboori and C. N. Hadjicostis, “Verification of K-step opacity and analysis of its complexity,” IEEE Trans. Autom. Science and Engineering, vol. 8, no. 3, pp. 549–559, 2011. doi: 10.1109/TASE.2011.2106775
|
[7] |
A. Saboori and C. N. Hadjicostis, “Verification of infinite-step opacity and complexity considerations,” IEEE Trans. Autom. Control, vol. 57, no. 5, pp. 1265–1269, 2011.
|
[8] |
F. Lin, “Opacity of discrete event systems and its applications,” Automatica, vol. 47, no. 3, pp. 496–503, 2011. doi: 10.1016/j.automatica.2011.01.002
|
[9] |
F. Cassez, J. Dubreil, and H. Marchand, “Dynamic observers for the synthesis of opaque systems,” in Int. Symposium on Automated Technology for Verification and Analysis. Berlin, Germany: Springer, 2009, pp. 352–367.
|
[10] |
C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, 2nd ed. New York, USA: Springer, 2009.
|
[11] |
Y.-C. Wu and S. Lafortune, “Comparative analysis of related notions of opacity in centralized and coordinated architectures,” Discrete Event Dynamic Systems, vol. 23, no. 3, pp. 307–339, 2013. doi: 10.1007/s10626-012-0145-z
|
[12] |
X. Yin and S. Lafortune, “A new approach for the verification of infinite-step and K-step opacity using two-way observers,” Automatica, vol. 80, pp. 162–171, 2017. doi: 10.1016/j.automatica.2017.02.037
|
[13] |
Y. Falcone and H. Marchand, “Enforcement and validation (at runtime) of various notions of opacity,” Discrete Event Dynamic Systems, vol. 25, no. 4, pp. 531–570, 2015. doi: 10.1007/s10626-014-0196-4
|
[14] |
Z. Ma, X. Yin, and Z. Li, “Verification and enforcement of strong infinite- and k-step opacity using state recognizers,” Automatica, vol. 133, p. 109838, 2021. doi: 10.1016/j.automatica.2021.109838
|
[15] |
Y. Tong, Z. Li, C. Seatzu, and A. Giua, “Verification of state-based opacity using Petri nets,” IEEE Trans. Autom. Control, vol. 62, no. 6, pp. 2823–2837, 2016.
|
[16] |
X. Cong, M. P. Fanti, A. M. Mangini, and Z. Li, “On-line verification of current-state opacity by Petri nets and integer linear programming,” Automatica, vol. 94, pp. 205–213, 2018. doi: 10.1016/j.automatica.2018.04.021
|
[17] |
X. Cong, M. P. Fanti, A. M. Mangini, and Z. Li, “On-line verification of initial-state opacity by Petri nets and integer linear programming,” ISA Trans., vol. 93, pp. 108–114, 2019. doi: 10.1016/j.isatra.2019.01.023
|
[18] |
Y. Dong, Z. Li, and N. Wu, “Symbolic verification of current-state opacity of discrete event systems using Petri nets,” IEEE Trans. Systems,Man,and Cyber.: Systems, vol. 52, no. 12, pp. 7628–7641, 2022. doi: 10.1109/TSMC.2022.3151695
|
[19] |
H. Lan, Y. Tong, and C. Seatzu, “Verification of infinite-step opacity using labeled Petri nets,” IFAC-PapersOnLine, vol. 53, no. 2, pp. 1729–1734, 2020. doi: 10.1016/j.ifacol.2020.12.2287
|
[20] |
Y. Tong, H. Lan, and C. Seatzu, “Verification of K-step and infinite-step opacity of bounded labeled Petri nets,” Automatica, vol. 140, p. 110221, 2022. doi: 10.1016/j.automatica.2022.110221
|
[21] |
G. Zhu, Z. Li, and N. Wu, “Online verification of K-step opacity by Petri nets in centralized and decentralized structures,” Automatica, vol. 145, p. 110528, 2022. doi: 10.1016/j.automatica.2022.110528
|
[22] |
W. Duo, M. Zhou, and A. Abusorrah, “A survey of cyber attacks on cyber physical systems: Recent advances and challenges,” IEEE/CAA J. Autom. Sinica, vol. 9, no. 5, pp. 784–800, 2022. doi: 10.1109/JAS.2022.105548
|
[23] |
X. Wang, J. Sun, G. Wang, F. Allgöwer, and J. Chen, “Data-driven control of distributed event-triggered network systems,” IEEE/CAA J. Autom. Sinica, vol. 10, no. 2, pp. 351–364, 2023. doi: 10.1109/JAS.2023.123225
|
[24] |
D. You, S. Wang, M. Zhou, and C. Seatzu, “Supervisory control of Petri nets in the presence of replacement attacks,” IEEE Trans. Autom. Control, vol. 67, no. 3, pp. 1466–1473, 2022. doi: 10.1109/TAC.2021.3063699
|
[25] |
D. You, S. Wang, and C. Seatzu, “A liveness-enforcing supervisor tolerant to sensor-reading modification attacks,” IEEE Trans. Systems,Man,and Cyber.: Systems, vol. 52, no. 4, pp. 2398–2411, 2022. doi: 10.1109/TSMC.2021.3051096
|
[26] |
F. Lin, “Control of networked discrete event systems: Dealing with communication delays and losses,” SIAM J. Control and Optimization, vol. 52, no. 2, pp. 1276–1298, 2014. doi: 10.1137/130914942
|
[27] |
S. Shu and F. Lin, “Supervisor synthesis for networked discrete event systems with communication delays,” IEEE Trans. Autom. Control, vol. 60, no. 8, pp. 2183–2188, 2014.
|
[28] |
Y. Ju, D. Ding, X. He, Q.-L. Han, and G. Wei, “Consensus control of multi-agent systems using fault-estimation-in-the-loop: Dynamic event-triggered case,” IEEE/CAA J. Autom. Sinica, vol. 9, no. 8, pp. 1440–1451, 2021.
|
[29] |
S. Shu and F. Lin, “Predictive networked control of discrete event systems,” IEEE Trans. Autom. Control, vol. 62, no. 9, pp. 4698–4705, 2016.
|
[30] |
Z. Liu, X. Yin, S. Shu, F. Lin, and S. Li, “Online supervisory control of networked discrete event systems with control delays,” IEEE Trans. Autom. Control, vol. 67, no. 5, pp. 2314–2329, 2022. doi: 10.1109/TAC.2021.3080495
|
[31] |
J. Yang, W. Deng, D. Qiu, and C. Jiang, “Opacity of networked discrete event systems,” Information Sciences, vol. 543, pp. 328–344, 2021. doi: 10.1016/j.ins.2020.07.017
|
[32] |
T. Murata, “Petri nets: Properties, analysis and applications,” Proc. IEEE, vol. 77, pp. 541–580, 1989. doi: 10.1109/5.24143
|
[33] |
A. S. Miner and G. Ciardo, “Efficient reachability set generation and storage using decision diagrams,” in Proc. Int. Conf. Application and Theory of Petri Nets, 1999, pp. 6–25.
|
[34] |
A. S. Miner, “Implicit GSPN reachability set generation using decision diagrams,” Performance Evaluation, vol. 56, no. 1–4, pp. 145–165, 2004. doi: 10.1016/j.peva.2003.07.005
|
[35] |
G. Ciardo, G. Lüttgen, and R. Siminiceanu, “Efficient symbolic state-space construction for asynchronous systems,” in Proc. Int. Conf. Application and Theory of Petri Nets, 2000, pp. 103–122.
|
[36] |
M. Wan and G. Ciardo, “Symbolic state-space generation of asynchronous systems using extensible decision diagrams,” in Proc. Int. Conf. Current Trends in Theory and Practice of Computer Science, 2009, pp. 582–594.
|
[37] |
Y. Dong, Z. Li, and N. Wu, “Supplementary contents for NDESs.” [Online]. Available: https://github.com/dongyifan199/Opacity-in-NDESs. Accessed: Oct. 7th, 2023.
|
[38] |
J. Babar and A. Miner, “Meddly: Multi-terminal and edge-valued decision diagram library,” in Proc. 7th Int. Conf. Quantitative Evaluation of Systems, 2010, pp. 195–196.
|
[39] |
S. Liu, Y. Tong, C. Seatzu, and A. Giua, “Petribar: A Matlab tool- box for Petri nets implementing basis reachability approaches,” IFAC-PapersOnLine, vol. 51, no. 7, pp. 316–322, 2018. doi: 10.1016/j.ifacol.2018.06.319
|