Document Open Access Logo

State-Based Opacity of Real-Time Automata

Author Kuize Zhang

PDF
Thumbnail PDF

File

OASIcs.AUTOMATA.2021.12.pdf
  • Filesize: 0.64 MB
  • 15 pages

Document Identifiers

Author Details

Kuize Zhang
  • Control Systems Group, Technische Universität Berlin, Germany

Funding

This work was partially supported by the Alexander von Humboldt Foundation.

Cite AsGet BibTex

Kuize Zhang. State-Based Opacity of Real-Time Automata. In 27th IFIP WG 1.5 International Workshop on Cellular Automata and Discrete Complex Systems (AUTOMATA 2021). Open Access Series in Informatics (OASIcs), Volume 90, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/OASIcs.AUTOMATA.2021.12

Abstract

State-based opacity is a special type of opacity as a confidentiality property, which describes whether an external intruder cannot make for sure whether secret states of a system have been visited by observing generated outputs, given that the intruder knows complete knowledge of the system’s structure but can only see generated outputs. When the time of visiting secret states is specified as the initial time, the current time, any past time, and at most K steps prior to the current time, the notions of state-based opacity can be formulated as initial-state opacity, current-state opacity, infinite-step opacity, and K-step opacity, respectively. In this paper, we formulate the four versions of opacity for real-time automata which are a widely-used model of real-time systems, and give 2-EXPTIME verification algorithms for the four notions by defining appropriate notions of observer and reverse observer for real-time automata that are computable in 2-EXPTIME.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
  • Security and privacy → Formal security models
Keywords
  • real-time automaton
  • state-based opacity
  • observer
  • verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. J. Balun and T. Masopust. Comparing the notions of opacity for discete-event systems, 2021. URL: https://arxiv.org/abs/2102.02889.
  2. B. Bérard, S. Haar, S. Schmitz, and S. Schwoon. The complexity of diagnosability and opacity verification for Petri nets. Fundamenta Informaticae, 161(4):317-349, 2018. Google Scholar
  3. J. W. Bryans, M. Koutny, L. Mazaré, and P. Y. A. Ryan. Opacity generalised to transition systems. International Journal of Information Security, 7(6):421-435, November 2008. URL: https://doi.org/10.1007/s10207-008-0058-x.
  4. F. Cassez. The dark side of timed opacity. In Jong Hyuk Park, Hsiao-Hwa Chen, Mohammed Atiquzzaman, Changhoon Lee, Tai-hoon Kim, and Sang-Soo Yeo, editors, Advances in Information Security and Assurance, pages 21-30, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  5. F. Cassez, J. Dubreil, and H. Marchand. Dynamic observers for the synthesis of opaque systems. In Automated Technology for Verification and Analysis, pages 352-367, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  6. S. Chédor, C. Morvan, S. Pinchinat, and H. Marchand. Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems. Discrete Event Dynamic Systems, 25(1-2):271-294, 2014. Google Scholar
  7. F. Lin. Opacity of discrete event systems and its applications. Automatica, 47(3):496-503, 2011. URL: https://doi.org/10.1016/j.automatica.2011.01.002.
  8. L. Mazaré. Using unification for opacity properties. In Proceedings of the Workshop on Issues in the Theory of Security (WITS'04), pages 165-176, 2004. Google Scholar
  9. M. Nykänen and E. Ukkonen. The exact path length problem. Journal of Algorithms, 42(1):41-53, 2002. URL: https://doi.org/10.1006/jagm.2001.1201.
  10. A. Saboori and C. N. Hadjicostis. Notions of security and opacity in discrete event systems. In 2007 46th IEEE Conference on Decision and Control, pages 5056-5061, December 2007. URL: https://doi.org/10.1109/CDC.2007.4434515.
  11. A. Saboori and C. N. Hadjicostis. Verification of K-step opacity and analysis of its complexity. In Proceedings of the 48h IEEE Conference on Decision and Control (CDC) held jointly with 2009 28th Chinese Control Conference, pages 205-210, 2009. URL: https://doi.org/10.1109/CDC.2009.5400083.
  12. A. Saboori and C. N. Hadjicostis. Verification of infinite-step opacity and complexity considerations. IEEE Transactions on Automatic Control, 57(5):1265-1269, May 2012. URL: https://doi.org/10.1109/TAC.2011.2173774.
  13. A. Saboori and C. N. Hadjicostis. Verification of initial-state opacity in security applications of discrete event systems. Information Sciences, 246:115-132, 2013. URL: https://doi.org/10.1016/j.ins.2013.05.033.
  14. A. Schrijver. Theory of Linear and Integer Programming. John Wiley & Sons, Inc., USA, 1986. Google Scholar
  15. M. Sipser. Introduction to the Theory of Computation. International Thomson Publishing, 1st edition, 1996. Google Scholar
  16. Y. Tong, Z. Li, C. Seatzu, and A. Giua. Decidability of opacity verification problems in labeled Petri net systems. Automatica, 80:48-53, 2017. URL: https://doi.org/10.1016/j.automatica.2017.01.013.
  17. L. Wang and N. Zhan. Decidability of the Initial-State Opacity of Real-Time Automata, pages 44-60. Springer International Publishing, Cham, 2018. URL: https://doi.org/10.1007/978-3-030-01461-2_3.
  18. L. Wang, N. Zhan, and J. An. The opacity of real-time automata. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 37(11):2845-2856, 2018. URL: https://doi.org/10.1109/TCAD.2018.2857363.
  19. Y. Wu and S. Lafortune. Comparative analysis of related notions of opacity in centralized and coordinated architectures. Discrete Event Dynamic Systems, 23(3):307-339, September 2013. URL: https://doi.org/10.1007/s10626-012-0145-z.
  20. X. Yin and S. Lafortune. A new approach for the verification of infinite-step and K-step opacity using two-way observers. Automatica, 80:162-171, 2017. URL: https://doi.org/10.1016/j.automatica.2017.02.037.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact