Document Open Access Logo

Execution-Time Opacity Problems in One-Clock Parametric Timed Automata

Authors Étienne André , Johan Arcile , Engel Lefaucheux

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2024.3.pdf
  • Filesize: 1.01 MB
  • 22 pages

Document Identifiers

Author Details

Étienne André
  • Université Sorbonne Paris Nord, LIPN, CNRS UMR 7030, F-93430 Villetaneuse, France
  • Institut Universitaire de France (IUF), Paris, France
Johan Arcile
  • IBISC, Univ Evry, Université Paris-Saclay, 91025 Evry, France
Engel Lefaucheux
  • Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

Funding

This work is partially supported by the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015 / 2019 ANR NRF 0092) and by ANR BisoUS (ANR-22-CE48-0012).

Cite As Get BibTex

Étienne André, Johan Arcile, and Engel Lefaucheux. Execution-Time Opacity Problems in One-Clock Parametric Timed Automata. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 3:1-3:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSTTCS.2024.3

Abstract

Parametric timed automata (PTAs) extend the concept of timed automata, by allowing timing delays not only specified by concrete values but also by parameters, allowing the analysis of systems with uncertainty regarding timing behaviors. The full execution-time opacity is defined as the problem in which an attacker must never be able to deduce whether some private location was visited, by only observing the execution time. The problem of full ET-opacity emptiness (i.e., the emptiness over the parameter valuations for which full execution-time opacity is satisfied) is known to be undecidable for general PTAs. We therefore focus here on one-clock PTAs with integer-valued parameters over dense time. We show that the full ET-opacity emptiness is undecidable for a sufficiently large number of parameters, but is decidable for a single parameter, and exact synthesis can be effectively achieved. Our proofs rely on a novel construction as well as on variants of Presburger arithmetics. We finally prove an additional decidability result on an existential variant of execution-time opacity.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
  • Security and privacy → Logic and verification
Keywords
  • Timed opacity
  • Parametric timed automata
  • Presburger arithmetic

Metrics

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

Related Versions

References

  1. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, April 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  2. Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In S. Rao Kosaraju, David S. Johnson, and Alok Aggarwal, editors, STOC, pages 592-601, New York, NY, USA, 1993. ACM. URL: https://doi.org/10.1145/167088.167242.
  3. Ikhlass Ammar, Yamen El Touati, Moez Yeddes, and John Mullins. Bounded opacity for timed systems. Journal of Information Security and Applications, 61:1-13, September 2021. URL: https://doi.org/10.1016/j.jisa.2021.102926.
  4. Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan, and Ichiro Hasuo. The opacity of timed automata. In André Platzer, Kristin-Yvonne Rozier, Matteo Pradella, and Matteo Rossi, editors, FM, volume 14933 of Lecture Notes in Computer Science, pages 620-637. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-71162-6_32.
  5. Étienne André. What’s decidable about parametric timed automata? International Journal on Software Tools for Technology Transfer, 21(2):203-219, April 2019. URL: https://doi.org/10.1007/s10009-017-0467-0.
  6. Étienne André, Sarah Dépernet, and Engel Lefaucheux. The bright side of timed opacity. In Kazuhiro Ogata, Meng Sun, and Dominique Méry, editors, ICFEM, 2024. To appear. Google Scholar
  7. Étienne André, Engel Lefaucheux, Didier Lime, Dylan Marinho, and Jun Sun. Configuring timing parameters to ensure execution-time opacity in timed automata. In Maurice H. ter Beek and Clemens Dubslaff, editors, TiCSA, Electronic Proceedings in Theoretical Computer Science. Springer, 2023. Invited paper. Google Scholar
  8. Étienne André, Engel Lefaucheux, and Dylan Marinho. Expiring opacity problems in parametric timed automata. In Yamine Ait-Ameur and Ferhat Khendek, editors, ICECCS, pages 89-98, 2023. URL: https://doi.org/10.1109/ICECCS59891.2023.00020.
  9. Étienne André, Didier Lime, Dylan Marinho, and Jun Sun. Guaranteeing timed opacity using parametric timed model checking. ACM Transactions on Software Engineering and Methodology, 31(4):1-36, October 2022. URL: https://doi.org/10.1145/3502851.
  10. Étienne André, Didier Lime, and Nicolas Markey. Language preservation problems in parametric timed automata. Logical Methods in Computer Science, 16(1), January 2020. URL: https://doi.org/10.23638/LMCS-16(1:5)2020.
  11. Étienne André, Johan Arcile, and Engel Lefaucheux. Execution-time opacity problems in one-clock parametric timed automata (extended version). Technical Report abs/2410.01659, arXiv, October 2024. URL: https://arxiv.org/abs/2410.01659.
  12. Nikola Beneš, Peter Bezděk, Kim Gulstrand Larsen, and Jiří Srba. Language emptiness of continuous-time parametric timed automata. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, ICALP, Part II, volume 9135 of Lecture Notes in Computer Science, pages 69-81. Springer, July 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_6.
  13. Arnab Kumar Biswas, Dipak Ghosal, and Shishir Nagaraja. A survey of timing channels and countermeasures. ACM Computing Surveys, 50(1):6:1-6:39, 2017. URL: https://doi.org/10.1145/3023872.
  14. Véronique Bruyère, Emmanuel Dall'Olio, and Jean-Francois Raskin. Durations and parametric model-checking in timed automata. ACM Transactions on Computational Logic, 9(2):12:1-12:23, 2008. URL: https://doi.org/10.1145/1342991.1342996.
  15. Jeremy W. Bryans, Maciej Koutny, Laurent Mazaré, and Peter Y. A. Ryan. Opacity generalised to transition systems. International Journal of Information Security, 7(6):421-435, 2008. URL: https://doi.org/10.1007/s10207-008-0058-x.
  16. Daniel Bundala and Joël Ouaknine. On parametric timed automata and one-counter machines. Information and Computation, 253:272-303, 2017. URL: https://doi.org/10.1016/j.ic.2016.07.011.
  17. Franck 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, ISA, volume 5576 of Lecture Notes in Computer Science, pages 21-30. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02617-1_3.
  18. Catalin Dima. Real-time automata. Journal of Automata, Languages and Combinatorics, 6(1):3-23, 2001. URL: https://doi.org/10.25596/jalc-2001-003.
  19. Guillaume Gardey, John Mullins, and Olivier H. Roux. Non-interference control synthesis for security timed automata. Electronic Notes in Theoretical Computer Science, 180(1):35-53, 2007. URL: https://doi.org/10.1016/j.entcs.2005.05.046.
  20. Hermann Gruber and Markus Holzer. From finite automata to regular expressions and back - A summary on descriptional complexity. International Journal of Foundations of Computer Science, 26(8):1009-1040, 2015. URL: https://doi.org/10.1142/S0129054115400110.
  21. Stefan Göller and Mathieu Hilaire. Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete. In Markus Bläser and Benjamin Monmege, editors, STACS, volume 187 of LIPIcs, pages 36:1-36:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.STACS.2021.36.
  22. Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. Timed transition systems. In J. W. de Bakker, Cornelis Huizing, Willem P. de Roever, and Grzegorz Rozenberg, editors, REX, volume 600 of Lecture Notes in Computer Science, pages 226-251. Springer, 1992. URL: https://doi.org/10.1007/BFb0031995.
  23. Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming, 52-53:183-220, 2002. URL: https://doi.org/10.1016/S1567-8326(02)00037-1.
  24. Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer parameter synthesis for real-time systems. IEEE Transactions on Software Engineering, 41(5):445-461, 2015. URL: https://doi.org/10.1109/TSE.2014.2357445.
  25. Julian Klein, Paul Kogel, and Sabine Glesner. Verifying opacity of discrete-timed automata. In Nico Plat, Stefania Gnesi, Carlo A. Furia, and Antónia Lopes, editors, FormaliSE, pages 55-65. ACM, 2024. URL: https://doi.org/10.1145/3644033.3644376.
  26. Antonia Lechner, Joël Ouaknine, and James Worrell. On the complexity of linear arithmetic with divisibility. In LICS, pages 667-676. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.67.
  27. Engel Lefaucheux. When are two parametric semi-linear sets equal? Technical Report hal-04172593, HAL, 2024. URL: https://inria.hal.science/hal-04172593.
  28. Laurent Mazaré. Using unification for opacity properties. In Peter Ryan, editor, WITS, pages 165-176, April 2004. Google Scholar
  29. Joseph S. Miller. Decidability and complexity results for timed automata and semi-linear hybrid automata. In Nancy A. Lynch and Bruce H. Krogh, editors, HSCC, volume 1790 of Lecture Notes in Computer Science, pages 296-309. Springer, 2000. URL: https://doi.org/10.1007/3-540-46430-1_26.
  30. Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, Inc., New York, NY, USA, 1986. Google Scholar
  31. Lingtai Wang and Naijun Zhan. Decidability of the initial-state opacity of real-time automata. In Cliff B. Jones, Ji Wang, and Naijun Zhan, editors, Symposium on Real-Time and Hybrid Systems - Essays Dedicated to Professor Chaochen Zhou on the Occasion of His 80th Birthday, volume 11180 of Lecture Notes in Computer Science, pages 44-60. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-01461-2_3.
  32. Lingtai Wang, Naijun Zhan, and Jie 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.
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 About DROPS Imprint Privacy Contact