Deciding Asynchronous Hyperproperties for Recursive Programs
Article No.: 2, Pages 33 - 60
Abstract
We introduce a novel logic for asynchronous hyperproperties with a new mechanism to identify relevant positions on traces. While the new logic is more expressive than a related logic presented recently by Bozzelli et al., we obtain the same complexity of the model checking problem for finite state models. Beyond this, we study the model checking problem of our logic for pushdown models. We argue that the combination of asynchronicity and a non-regular model class studied in this paper constitutes the first suitable approach for hyperproperty model checking against recursive programs.
References
[1]
Rajeev Alur, Kousha Etessami, and P. Madhusudan. 2004. A Temporal Logic of Nested Calls and Returns. In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, Kurt Jensen and Andreas Podelski (Eds.) (Lecture Notes in Computer Science, Vol. 2988). Springer, 467–481. https://doi.org/10.1007/978-3-540-24730-2_35
[2]
Rajeev Alur and P. Madhusudan. 2004. Visibly Pushdown Languages. In Proceedings of the 36th Annual ACM Symposium on Theory of Computing, Chicago, IL, USA, June 13-16, 2004, László Babai (Ed.). ACM, 202–211. https://doi.org/10.1145/1007352.1007390
[3]
Ali Bajwa, Minjian Zhang, Rohit Chadha, and Mahesh Viswanathan. 2023. Stack-Aware Hyperproperties. In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I, Sriram Sankaranarayanan and Natasha Sharygina (Eds.) (Lecture Notes in Computer Science, Vol. 13993). Springer, 308–325. https://doi.org/10.1007/978-3-031-30823-9_16
[4]
Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. 2021. A Temporal Logic for Asynchronous Hyperproperties. In Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, Alexandra Silva and K. Rustan M. Leino (Eds.) (Lecture Notes in Computer Science, Vol. 12759). Springer, 694–717. https://doi.org/10.1007/978-3-030-81685-8_33
[5]
Raven Beutner and Bernd Finkbeiner. 2022. Software Verification of Hyperproperties Beyond k-Safety. In Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, Sharon Shoham and Yakir Vizel (Eds.) (Lecture Notes in Computer Science, Vol. 13371). Springer, 341–362. https://doi.org/10.1007/978-3-031-13185-1_17
[6]
Borzoo Bonakdarpour, Pavithra Prabhakar, and César Sánchez. 2020. Model Checking Timed Hyperproperties in Discrete-Time Systems. In NASA Formal Methods - 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings, Ritchie Lee, Susmit Jha, and Anastasia Mavridou (Eds.) (Lecture Notes in Computer Science, Vol. 12229). Springer, 311–328. https://doi.org/10.1007/978-3-030-55754-6_18
[7]
Borzoo Bonakdarpour, César Sánchez, and Gerardo Schneider. 2018. Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification. In Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part II, Tiziana Margaria and Bernhard Steffen (Eds.) (Lecture Notes in Computer Science, Vol. 11245). Springer, 8–27. https://doi.org/10.1007/978-3-030-03421-4_2
[8]
Ahmed Bouajjani, Javier Esparza, and Oded Maler. 1997. Reachability Analysis of Pushdown Automata: Application to Model-Checking. In CONCUR ’97: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings, Antoni W. Mazurkiewicz and Józef Winkowski (Eds.) (Lecture Notes in Computer Science, Vol. 1243). Springer, 135–150. https://doi.org/10.1007/3-540-63141-0_10
[9]
Laura Bozzelli. 2007. Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages. In CONCUR 2007 – Concurrency Theory, Luís Caires and Vasco T. Vasconcelos (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 476–491. isbn:978-3-540-74407-8 https://doi.org/10.1007/978-3-540-74407-8_32
[10]
Laura Bozzelli, Adriano Peron, and César Sánchez. 2021. Asynchronous Extensions of HyperLTL. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. IEEE, 1–13. https://doi.org/10.1109/LICS52264.2021.9470583
[11]
Laura Bozzelli, Adriano Peron, and César Sánchez. 2022. Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties. In 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, Bartek Klin, Slawomir Lasota, and Anca Muscholl (Eds.) (LIPIcs, Vol. 243). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 27:1–27:16. https://doi.org/10.4230/LIPIcs.CONCUR.2022.27
[12]
Stephen D. Brookes. 1996. Full Abstraction for a Shared-Variable Parallel Language. Inf. Comput., 127, 2 (1996), 145–163. https://doi.org/10.1006/inco.1996.0056
[13]
Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. 2014. Temporal Logics for Hyperproperties. In Principles of Security and Trust, Martín Abadi and Steve Kremer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 265–284. isbn:978-3-642-54792-8 https://doi.org/10.1007/978-3-642-54792-8_15
[14]
Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. J. Comput. Secur., 18, 6 (2010), Sept., 1157–1210. issn:0926-227X https://doi.org/10.3233/JCS-2009-0393
[15]
Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. 2019. The Hierarchy of Hyperlogics. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. 1–13. https://doi.org/10.1109/LICS.2019.8785713
[16]
Christian Dax and Felix Klaedtke. 2008. Alternation elimination by complementation. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. 214–229. https://doi.org/10.1007/978-3-540-89439-1_16
[17]
Stéphane Demri, Valentin Goranko, and Martin Lange. 2016. Temporal Logics in Computer Science: Finite-State Systems. Cambridge University Press. isbn:9781107028364 https://doi.org/10.1017/CBO9781139236119
[18]
Bernd Finkbeiner. 2017. Temporal Hyperproperties. Bulletin of the EATCS, 123 (2017).
[19]
Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. 2015. Algorithms for Model Checking HyperLTL and HyperCTL^*. In CAV 2015. 30–48. https://doi.org/10.1007/978-3-319-21690-4_3
[20]
Jens Oliver Gutsfeld, Arne Meier, Christoph Ohrem, and Jonni Virtema. 2022. Temporal Team Semantics Revisited. In LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, Christel Baier and Dana Fisman (Eds.). ACM, 44:1–44:13. https://doi.org/10.1145/3531130.3533360
[21]
Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. 2020. Propositional Dynamic Logic for Hyperproperties. In 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), Igor Konnov and Laura Kovács (Eds.) (LIPIcs, Vol. 171). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 50:1–50:22. https://doi.org/10.4230/LIPIcs.CONCUR.2020.50
[22]
Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. 2021. Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang., 5, POPL (2021), 1–29. https://doi.org/10.1145/3434319
[23]
Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. 2023. Deciding Asynchronous Hyperproperties for Recursive Programs. arxiv:2201.12859. arxiv:2201.12859
[24]
Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann. 2018. Team Semantics for the Specification and Verification of Hyperproperties. In 43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018, August 27-31, 2018, Liverpool, UK, Igor Potapov, Paul G. Spirakis, and James Worrell (Eds.) (LIPIcs, Vol. 117). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 10:1–10:16. https://doi.org/10.4230/LIPIcs.MFCS.2018.10
[25]
Adrien Pommellet and Tayssir Touili. 2018. Model-Checking HyperLTL for Pushdown Systems. In Model Checking Software - 25th International Symposium, SPIN 2018, Malaga, Spain, June 20-22, 2018, Proceedings, María-del-Mar Gallardo and Pedro Merino (Eds.) (Lecture Notes in Computer Science, Vol. 10869). Springer, 133–152. https://doi.org/10.1007/978-3-319-94111-0_8
[26]
Markus N. Rabe. 2016. A temporal logic approach to Information-flow control. Ph. D. Dissertation. Saarland University.
[27]
Alex Spelten, Wolfgang Thomas, and Sarah Winter. 2011. Trees over Infinite Structures and Path Logics with Synchronization. In Proceedings 13th International Workshop on Verification of Infinite-State Systems, INFINITY 2011, Taipei, Taiwan, 10th October 2011, Fang Yu and Chao Wang (Eds.) (EPTCS, Vol. 73). 20–34. https://doi.org/10.4204/EPTCS.73.5
[28]
Moshe Y. Vardi. 1988. A Temporal Fixpoint Calculus. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988, Jeanne Ferrante and Peter Mager (Eds.). ACM Press, 250–259. https://doi.org/10.1145/73560.73582
[29]
Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang. 2021. Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021, December 15-17, 2021, Virtual Conference, Mikolaj Bojanczyk and Chandra Chekuri (Eds.) (LIPIcs, Vol. 213). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 52:1–52:17. https://doi.org/10.4230/LIPIcs.FSTTCS.2021.52
[30]
Pierre Wolper. 1981. Temporal Logic Can Be More Expressive. In 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28-30 October 1981. IEEE Computer Society, 340–348. https://doi.org/10.1109/SFCS.1981.44
[31]
Steve Zdancewic and Andrew C. Myers. 2003. Observational Determinism for Concurrent Program Security. In 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), 30 June - 2 July 2003, Pacific Grove, CA, USA. IEEE Computer Society, 29. https://doi.org/10.1109/CSFW.2003.1212703
Index Terms
- Deciding Asynchronous Hyperproperties for Recursive Programs
Recommendations
Stack-Aware Hyperproperties
Tools and Algorithms for the Construction and Analysis of SystemsAbstractA hyperproperty relates executions of a program and is used to formalize security objectives such as confidentiality, non-interference, privacy, and anonymity. Formally, a hyperproperty is a collection of allowable sets of executions. A program ...
Temporal Team Semantics Revisited
LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer ScienceIn this paper, we study a novel approach to asynchronous hyperproperties by reconsidering the foundations of temporal team semantics. We consider three logics: , and , which are obtained by adding quantification over so-called time evaluation functions ...
Automata and fixpoints for asynchronous hyperproperties
Hyperproperties have received increasing attention in the last decade due to their importance e.g. for security analyses. Past approaches have focussed on synchronous analyses, i.e. techniques in which different paths are compared lockstepwise. In this ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2024
2820 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 05 January 2024
Published in PACMPL Volume 8, Issue POPL
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- DFG
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 265Total Downloads
- Downloads (Last 12 months)265
- Downloads (Last 6 weeks)36
Reflects downloads up to 09 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in