Document Open Access Logo

A Temporal Logic for Strategic Hyperproperties

Authors Raven Beutner , Bernd Finkbeiner

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.24.pdf
  • Filesize: 0.89 MB
  • 19 pages

Document Identifiers

Author Details

Raven Beutner
  • CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
Bernd Finkbeiner
  • CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

Funding

This work was partially supported by the German Research Foundation (DFG) as part of the Collaborative Research Center "Foundations of Perspicuous Software Systems" (TRR 248, 389792660), by the European Research Council (ERC) Grant OSARES (No. 683300) and by the Saarbrücken Graduate School of Computer Science.

Cite AsGet BibTex

Raven Beutner and Bernd Finkbeiner. A Temporal Logic for Strategic Hyperproperties. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.24

Abstract

Hyperproperties are commonly used in computer security to define information-flow policies and other requirements that reason about the relationship between multiple computations. In this paper, we study a novel class of hyperproperties where the individual computation paths are chosen by the strategic choices of a coalition of agents in a multi-agent system. We introduce HyperATL^*, an extension of computation tree logic with path variables and strategy quantifiers. HyperATL^* can express strategic hyperproperties, such as that the scheduler in a concurrent system has a strategy to avoid information leakage. HyperATL^* is particularly useful to specify asynchronous hyperproperties, i.e., hyperproperties where the speed of the execution on the different computation paths depends on the choices of the scheduler. Unlike other recent logics for the specification of asynchronous hyperproperties, our logic is the first to admit decidable model checking for the full logic. We present a model checking algorithm for HyperATL^* based on alternating word automata, and show that our algorithm is asymptotically optimal by providing a matching lower bound. We have implemented a prototype model checker for a fragment of HyperATL^*, able to check various security properties on small programs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Verification by model checking
Keywords
  • hyperproperties
  • temporal logic
  • alternating-time temporal logic
  • model checking
  • multi-agent systems
  • information flow
  • asynchronous hyperproperties

Metrics

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

Related Versions

References

  1. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. URL: https://doi.org/10.1145/585265.585270.
  2. Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran. MOCHA: modularity in model checking. In Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, volume 1427 of Lecture Notes in Computer Science, pages 521-525. Springer, 1998. URL: https://doi.org/10.1007/BFb0028774.
  3. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  4. Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. A temporal logic for asynchronous hyperproperties. In Computer Aided Verification - 33nd International Conference, CAV 2021, Los Angeles, CA, USA, July 18-24, 2021, Lecture Notes in Computer Science. Springer, 2021. Google Scholar
  5. Raphaël Berthon, Bastien Maubert, and Aniello Murano. Decidability results for atl* with imperfect information and perfect recall. In Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, São Paulo, Brazil, May 8-12, 2017, pages 1250-1258. ACM, 2017. URL: http://dl.acm.org/citation.cfm?id=3091299.
  6. Raven Beutner and Bernd Finkbeiner. A temporal logic for strategic hyperproperties. CoRR, abs/2107.02509, 2021. URL: http://arxiv.org/abs/2107.02509.
  7. Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat. Unifying hyper and epistemic temporal logics. In Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9034 of Lecture Notes in Computer Science, pages 167-182. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46678-0_11.
  8. Laura Bozzelli, Adriano Peron, and César Sánchez. Asynchronous extensions of hyperltl. In 36nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. ACM, 2021. Google Scholar
  9. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8414 of Lecture Notes in Computer Science, pages 265-284. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_15.
  10. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  11. Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. The hierarchy of hyperlogics. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785713.
  12. Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. Verifying hyperliveness. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, volume 11561 of Lecture Notes in Computer Science, pages 121-139. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25540-4_7.
  13. Doron Drusinsky and David Harel. On the power of bounded concurrency I: finite automata. J. ACM, 41(3):517-539, 1994. URL: https://doi.org/10.1145/176584.176587.
  14. E. Allen Emerson and Joseph Y. Halpern. "Sometimes" and "not never" revisited: on branching versus linear time temporal logic. J. ACM, 33(1):151-178, 1986. URL: https://doi.org/10.1145/4904.4999.
  15. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge. MIT Press, 1995. URL: https://doi.org/10.7551/mitpress/5803.001.0001.
  16. Bernd Finkbeiner. Temporal hyperproperties. Bull. EATCS, 123, 2017. URL: http://eatcs.org/beatcs/index.php/beatcs/article/view/514.
  17. Bernd Finkbeiner. Model checking algorithms for hyperproperties (invited paper). In Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings, volume 12597 of Lecture Notes in Computer Science, pages 3-16. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-67067-2_1.
  18. Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, and Leander Tentrup. Realizing omega-regular hyperproperties. In Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, volume 12225 of Lecture Notes in Computer Science, pages 40-63. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_4.
  19. Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. Synthesizing reactive systems from hyperproperties. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pages 289-306. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96145-3_16.
  20. Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for model checking hyperltl and hyperctl^*. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 30-48. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_3.
  21. Bernd Finkbeiner and Martin Zimmermann. The first-order logic of hyperproperties. In 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017, March 8-11, 2017, Hannover, Germany, volume 66 of LIPIcs, pages 30:1-30:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.30.
  22. Oliver Friedmann and Martin Lange. Solving parity games in practice. In Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, volume 5799 of Lecture Notes in Computer Science, pages 182-196. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04761-9_15.
  23. Joseph A. Goguen and José Meseguer. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982, pages 11-20. IEEE Computer Society, 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  24. Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Propositional dynamic logic for hyperproperties. In 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 50:1-50:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.50.
  25. Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang., 5(POPL):1-29, 2021. URL: https://doi.org/10.1145/3434319.
  26. Marieke Huisman, Pratik Worah, and Kim Sunesen. A temporal logic characterisation of observational determinism. In 19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006), 5-7 July 2006, Venice, Italy, page 3. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/CSFW.2006.6.
  27. Jan Kretínský, Tobias Meggendorfer, Salomon Sickert, and Christopher Ziegler. Rabinizer 4: From LTL to your favourite deterministic automaton. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pages 567-577. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96145-3_30.
  28. Orna Kupferman and Moshe Y. Vardi. Weak alternating automata and tree automata emptiness. In Proceedings of the Thirtieth Annual ACM Symposium on the Theory of Computing, Dallas, Texas, USA, May 23-26, 1998, pages 224-233. ACM, 1998. URL: https://doi.org/10.1145/276698.276748.
  29. Orna Kupferman and Moshe Y. Vardi. Weak alternating automata are not that weak. ACM Trans. Comput. Log., 2(3):408-429, 2001. URL: https://doi.org/10.1145/377978.377993.
  30. Heiko Mantel and Henning Sudbrock. Flexible scheduler-independent security. In Computer Security - ESORICS 2010, 15th European Symposium on Research in Computer Security, Athens, Greece, September 20-22, 2010. Proceedings, volume 6345 of Lecture Notes in Computer Science, pages 116-133. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15497-3_8.
  31. Daryl McCullough. Noninterference and the composability of security properties. In Proceedings of the 1988 IEEE Symposium on Security and Privacy, Oakland, California, USA, April 18-21, 1988, pages 177-186. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/SECPRI.1988.8110.
  32. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  33. Satoru Miyano and Takeshi Hayashi. Alternating finite automata on omega-words. Theor. Comput. Sci., 32:321-330, 1984. URL: https://doi.org/10.1016/0304-3975(84)90049-5.
  34. David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), Edinburgh, Scotland, UK, July 5-8, 1988, pages 422-427. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/LICS.1988.5139.
  35. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  36. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 179-190. ACM Press, 1989. URL: https://doi.org/10.1145/75277.75293.
  37. Amir Pnueli and Roni Rosner. On the synthesis of an asynchronous reactive module. In Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Proceedings, volume 372 of Lecture Notes in Computer Science, pages 652-671. Springer, 1989. URL: https://doi.org/10.1007/BFb0035790.
  38. Markus N. Rabe. A temporal logic approach to information-flow control. PhD thesis, Saarland University, 2016. URL: http://scidok.sulb.uni-saarland.de/volltexte/2016/6387/.
  39. Andrei Sabelfeld. Confidentiality for multithreaded programs via bisimulation. In Perspectives of Systems Informatics, 5th International Andrei Ershov Memorial Conference, PSI 2003, Akademgorodok, Novosibirsk, Russia, July 9-12, 2003, Revised Papers, volume 2890 of Lecture Notes in Computer Science, pages 260-274. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-39866-0_27.
  40. Andrei Sabelfeld and David Sands. Probabilistic noninterference for multi-threaded programs. In Proceedings of the 13th IEEE Computer Security Foundations Workshop, CSFW '00, Cambridge, England, UK, July 3-5, 2000, pages 200-214. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/CSFW.2000.856937.
  41. Walter J. Savitch. Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci., 4(2):177-192, 1970. URL: https://doi.org/10.1016/S0022-0000(70)80006-X.
  42. Wiebe van der Hoek and Michael J. Wooldridge. Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Stud Logica, 75(1):125-157, 2003. URL: https://doi.org/10.1023/A:1026185103185.
  43. Moshe Y. Vardi. Alternating automata and program verification. In Computer Science Today: Recent Trends and Developments, volume 1000 of Lecture Notes in Computer Science, pages 471-485. Springer, 1995. URL: https://doi.org/10.1007/BFb0015261.
  44. Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Inf. Comput., 115(1):1-37, 1994. URL: https://doi.org/10.1006/inco.1994.1092.
  45. J. Todd Wittbold and Dale M. Johnson. Information flow in nondeterministic systems. In Proceedings of the 1990 IEEE Symposium on Security and Privacy, Oakland, California, USA, May 7-9, 1990, pages 144-161. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/RISP.1990.63846.
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