Document Open Access Logo

On Verifying Timed Hyperproperties

Authors Hsi-Ming Ho , Ruoyu Zhou, Timothy M. Jones

PDF
Thumbnail PDF

File

LIPIcs.TIME.2019.20.pdf
  • Filesize: 0.66 MB
  • 18 pages

Document Identifiers

Author Details

Hsi-Ming Ho
  • University of Cambridge, UK
Ruoyu Zhou
  • University of Cambridge, UK
Timothy M. Jones
  • University of Cambridge, UK

Funding

This work was supported by the Engineering and Physical Sciences Research Council (EPSRC), through grant references EP/K026399/1 and EP/P020011/1.

Cite AsGet BibTex

Hsi-Ming Ho, Ruoyu Zhou, and Timothy M. Jones. On Verifying Timed Hyperproperties. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TIME.2019.20

Abstract

We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMTL, a timed extension of HyperLTL. Depending on whether interleaving of events in different traces is allowed, two possible semantics can be defined for timed hyperproperties: synchronous and asynchronous. While the satisfiability problem can be decided similarly as for HyperLTL regardless of the choice of semantics, we show that the model-checking problem for HyperMTL, unless the specification is alternation-free, is undecidable even when very restricted timing constraints are allowed. On the positive side, we show that model checking HyperMTL with quantifier alternations is possible under certain conditions in the synchronous semantics, or when there is a fixed bound on the length of the time domain.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Timed Automata
  • Temporal Logics
  • Cybersecurity

Metrics

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

Related Versions

References

  1. Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, Karin Quaas, and James Worrell. Universality Analysis for One-Clock Timed Automata. Fundam. Inform, 89(4):419-450, 2008. Google Scholar
  2. Erika Ábrahám and Borzoo Bonakdarpour. HyperPCTL: A temporal logic for probabilistic hyperproperties. In QEST, volume 11024 of Lecture Notes in Computer Science, pages 20-35. Springer, 2018. Google Scholar
  3. Shreya Agrawal and Borzoo Bonakdarpour. Runtime Verification of k-Safety Hyperproperties in HyperLTL. In CSF, pages 239-252. IEEE Computer Society, 2016. Google Scholar
  4. Rajeev Alur and David L. Dill. A Theory of Timed Automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  5. Rajeev Alur, Tomás Feder, and Thomas A. Henzinger. The Benefits of Relaxing Punctuality. Journal of the ACM, 43(1):116-146, 1996. Google Scholar
  6. Rajeev Alur and Thomas A. Henzinger. Back to the future: towards a theory of timed regular languages. In FOCS, pages 177-186. IEEE Computer Society, 1992. Google Scholar
  7. Rajeev Alur and Thomas A. Henzinger. Logics and Models of Real Time: A Survey. In REX, volume 600 of LNCS, pages 74-106. Springer-Verlag, 1992. Google Scholar
  8. Rajeev Alur and Thomas A. Henzinger. Real-Time Logics: Complexity and Expressiveness. Information and Computation, 104(1):35-77, 1993. Google Scholar
  9. Rajeev Alur and Thomas A. Henzinger. A Really Temporal Logic. Journal of the ACM, 41(1):164-169, 1994. Google Scholar
  10. Gilles Barthe, Pedro R. D'Argenio, and Tamara Rezk. Secure information flow by self-composition. Mathematical Structures in Computer Science, 21(6):1207-1252, 2011. Google Scholar
  11. Béatrice Bérard, Antoine Petit, Volker Diekert, and Paul Gastin. Characterization of the Expressive Power of Silent Transitions in Timed Automata. Fundam. Inform, 36(2-3):145-182, 1998. Google Scholar
  12. Borzoo Bonakdarpour and Bernd Finkbeiner. The Complexity of Monitoring Hyperproperties. In CSF, pages 162-174. IEEE Computer Society, 2018. Google Scholar
  13. D. Brand and P. Zafiropulo. On communicating finite state machines. Journal of the ACM, 30:323-342, 1983. Google Scholar
  14. Thomas Brihaye, Morgane Estiévenart, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege, and Nathalie Sznajder. Real-Time Synthesis is Hard! In FORMATS, volume 9884 of LNCS, pages 105-120. Springer, 2016. Google Scholar
  15. Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. NuSMV2: An opensource tool for symbolic model checking. In CAV, volume 2404 of LNCS, pages 359-364. Springer, 2002. Google Scholar
  16. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal Logics for Hyperproperties. In POST, volume 8414 of LNCS, pages 265-284. Springer, 2014. Google Scholar
  17. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. Google Scholar
  18. Laurent Doyen, Gilles Geeraerts, Jean-François Raskin, and Julien Reichert. Realizability of Real-Time Logics. In FORMATS, volume 5813 of LNCS, pages 133-148. Springer, 2009. Google Scholar
  19. Deepak D'Souza and P. Madhusudan. Timed control synthesis for external specifications. In STACS, volume 2285 of LNCS, pages 571-582. Springer, 2002. Google Scholar
  20. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 - A Framework for LTL and ω-Automata Manipulation. In ATVA, volume 9938 of LNCS, pages 122-129. Springer, 2016. Google Scholar
  21. Thomas Ferrère. The Compound Interest in Relaxing Punctuality. In FM, volume 10951 of LNCS, pages 147-164. Springer, 2018. Google Scholar
  22. Bernd Finkbeiner and Christopher Hahn. Deciding Hyperproperties. In CONCUR, volume 59 of LIPIcs, pages 13:1-13:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  23. Bernd Finkbeiner, Christopher Hahn, and Tobias Hans. MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the ∃^∗∀^∗ Fragment. In ATVA, volume 11138 of Lecture Notes in Computer Science, pages 521-527. Springer, 2018. Google Scholar
  24. Bernd Finkbeiner, Christopher Hahn, and Marvin Stenger. EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties. In CAV, volume 10427 of Lecture Notes in Computer Science, pages 564-570. Springer, 2017. Google Scholar
  25. Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. Monitoring Hyperproperties. In RV, volume 10548 of LNCS, pages 190-207. Springer, 2017. Google Scholar
  26. Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. RVHyper: A runtime verification tool for temporal hyperproperties. In TACAS, volume 10806 of Lecture Notes in Computer Science, pages 194-200. Springer, 2018. Google Scholar
  27. Bernd Finkbeiner, Christopher Hahn, and Hazem Torfah. Model Checking Quantitative Hyperproperties. In CAV, volume 10981 of Lecture Notes in Computer Science, pages 144-163. Springer, 2018. Google Scholar
  28. Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for Model Checking HyperLTL and HyperCTL^∗. In CAV, volume 9206 of LNCS, pages 30-48. Springer, 2015. Google Scholar
  29. Guillaume Gardey, John Mullins, and Olivier H. Roux. Non-Interference Control Synthesis for Security Timed Automata. Electr. Notes Theor. Comput. Sci, 180(1):35-53, 2007. Google Scholar
  30. Christopher Gerking, David Schubert, and Eric Bodden. Model Checking the Information Flow Security of Real-Time Systems. In ESSoS, volume 10953 of LNCS, pages 27-43. Springer, 2018. Google Scholar
  31. J. A. Goguen and J. Meseguer. Security Policies and Security Models. In S&P, pages 11-20. IEEE Computer Society, 1982. Google Scholar
  32. Jens Heinen. Model Checking Timed Hyperproperties. Master’s thesis, Saarland University, 2018. Google Scholar
  33. Thomas A. Henzinger, Jean-François Raskin, and Pierre-Yves Schobbens. The Regular Real-Time Languages. In ICALP, volume 1443 of LNCS, pages 580-591. Springer, 1998. Google Scholar
  34. Hsi-Ming Ho. On the Expressiveness of Metric Temporal Logic over Bounded Timed Words. In RP, volume 8762 of Lecture Notes in Computer Science, pages 138-150. Springer, 2014. Google Scholar
  35. Gerard J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5):279-295, 1997. Google Scholar
  36. John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979. Google Scholar
  37. Marieke Huisman, Pratik Worah, and Kim Sunesen. A Temporal Logic Characterisation of Observational Determinism. In CSFW, page 3. IEEE Computer Society, 2006. Google Scholar
  38. Paul Kocher, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. Spectre Attacks: Exploiting Speculative Execution. CoRR, abs/1801.01203, 2018. URL: http://arxiv.org/abs/1801.01203.
  39. Ron Koymans. Specifying Real-time Properties with Metric Temporal Logic. Real-Time Systems, 2(4):255-299, 1990. Google Scholar
  40. Jan Kretínský, Tobias Meggendorfer, and Salomon Sickert. Owl: A Library for ω-Words, Automata, and LTL. In ATVA, volume 11138 of Lecture Notes in Computer Science, pages 543-550. Springer, 2018. Google Scholar
  41. Antonín Kučera and Jan Strejček. The stuttering principle revisited. Acta Informatica, 41(7-8):415-434, 2005. Google Scholar
  42. L. Lamport. What good is Temporal Logic? In R.E.A. Mason, editor, IFIP Congress, pages 657-667, Amsterdam, 1983. North-Holland. Google Scholar
  43. Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134-152, 1997. Google Scholar
  44. Yang Li, Kazuo Sakiyama, Shigeto Gomisawa, Toshinori Fukunaga, Junko Takahashi, and Kazuo Ohta. Fault Sensitivity Analysis. In Stefan Mangard and François-Xavier Standaert, editors, CHES, volume 6225 of Lecture Notes in Computer Science, pages 320-334. Springer, 2010. Google Scholar
  45. Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. Meltdown: Reading Kernel Memory from User Space. In USENIX Security Symposium, pages 973-990. USENIX Association, 2018. Google Scholar
  46. John McLean. A general theory of composition for trace sets closed under selective interleaving functions. In S&P, pages 79-93. IEEE Computer Society, 1994. Google Scholar
  47. Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh, and Taylor T. Johnson. Hyperproperties of real-valued signals. In MEMOCODE, pages 104-113. ACM, 2017. Google Scholar
  48. Joël Ouaknine, Alexander Rabinovich, and James Worrell. Time-bounded verification. In Proceedings of CONCUR 2009, volume 5710 of LNCS, pages 496-510. Springer, 2009. Google Scholar
  49. Joël Ouaknine and James Worrell. On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap. In LICS, pages 54-63. IEEE Computer Society, 2004. Google Scholar
  50. Joël Ouaknine and James Worrell. On the Decidability and Complexity of Metric Temporal Logic over Finite Words. Logical Methods in Computer Science, 3(1), 2007. Google Scholar
  51. Joël Ouaknine and James Worrell. Some Recent Results in Metric Temporal Logic. In FORMATS, volume 5215 of LNCS, pages 1-13. Springer, 2008. Google Scholar
  52. Amir Pnueli. The temporal logic of programs. In FOCS, pages 46-57. IEEE, 1977. Google Scholar
  53. Jean-François Raskin. Logics, automata and classical theories for deciding real time. PhD thesis, FUNDP (Belgium), 1999. Google Scholar
  54. A. W. Roscoe. CSP and determinism in security modelling. In S&P, pages 114-127. IEEE Computer Society, 1995. Google Scholar
  55. Laurent Simon, David Chisnall, and Ross J. Anderson. What You Get is What You C: Controlling Side Effects in Mainstream C Compilers. In EuroS&P, pages 1-15. IEEE, 2018. Google Scholar
  56. A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The Complementation Problem for Büchi Automata with Applications to Temporal Logic (Extended Abstract). In ICALP, volume 194 of LNCS, pages 465-474. Springer, 1985. Google Scholar
  57. Ming-Hsien Tsai, Yih-Kuen Tsay, and Yu-Shiang Hwang. GOAL for Games, Omega-Automata, and Logics. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 883-889. Springer, 2013. Google Scholar
  58. Panagiotis Vasilikos, Flemming Nielson, and Hanne Riis Nielson. Secure Information Release in Timed Automata. In POST, volume 10804 of LNCS, pages 28-52. Springer, 2018. Google Scholar
  59. Steve Zdancewic and Andrew C. Myers. Observational Determinism for Concurrent Program Security. In CSFW, page 29. IEEE Computer Society, 2003. Google Scholar
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