More Web Proxy on the site http://driver.im/

research-article

Open access

Automata and fixpoints for asynchronous hyperproperties

Authors:

Jens Oliver Gutsfeld,

Markus Müller-Olm,

Christoph OhremAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 38, Pages 1 - 29

https://doi.org/10.1145/3434319

Published: 04 January 2021 Publication History

Abstract

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 paper, we systematically study asynchronous analyses for hyperproperties by introducing both a novel automata model (Alternating Asynchronous Parity Automata) and the temporal fixpoint calculus H_µ, the first fixpoint calculus that can systematically express hyperproperties in an asynchronous manner and at the same time subsumes the existing logic HyperLTL. We show that the expressive power of both models coincides over fixed path assignments. The high expressive power of both models is evidenced by the fact that decision problems of interest are highly undecidable, i.e. not even arithmetical. As a remedy, we propose approximative analyses for both models that also induce natural decidable fragments.

References

[1]

Henrik Reif Andersen. 1994. A polyadic modal-calculus. Technical Report ID-TR: 1994-195. Dept. of Computer Science, Technical University of Denmark, Copenhagen.

[2]

Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. 2009. Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. In Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009 (Lecture Notes in Computer Science, Vol. 5505 ), Stefan Kowalewski and Anna Philippou (Eds.). Springer, 107-123. https://doi.org/10.1007/978-3-642-00768-2_11

Digital Library

[3]

Kshitij Bansal and Stéphane Demri. 2013. Model-Checking Bounded Multi-Pushdown Systems. In Computer Science-Theory and Applications-8th International Computer Science Symposium in Russia, CSR 2013, Ekaterinburg, Russia, June 25-29, 2013. Proceedings. 405-417. https://doi.org/10.1007/978-3-642-38536-0_35

[4]

Howard Barringer, Ruurd Kuiper, and Amir Pnueli. 1986. A Really Abstract Concurrent Model and its Temporal Logic. In Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, USA, January 1986. ACM Press, 173-183. https://doi.org/10.1145/512644.512660

Digital Library

[5]

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. https://doi.org/10.1007/978-3-540-74407-8_32

[6]

Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat. 2015. Unifying hyper and epistemic temporal logics. In International Conference on Foundations of Software Science and Computation Structures. Springer, 167-182. https://doi.org/10.1007/978-3-662-46678-0_11

[7]

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. https://doi.org/10.1007/978-3-642-54792-8_15

[8]

Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. J. Comput. Secur. 18, 6 (Sept. 2010 ), 1157-1210. https://doi.org/10.3233/JCS-2009-0393

[9]

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

[10]

Patrick Cousot and Radhia Cousot. 1979. Constructive versions of Tarski's fixed point theorems. Pacific J. Math. 82, 1 ( 1979 ), 43-57. https://projecteuclid.org:443/euclid.pjm/1102785059

[11]

Christian Dax and Felix Klaedtke. 2008. Alternation elimination by complementation. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, 214-229. https://doi.org/10.1007/978-3-540-89439-1_16

Digital Library

[12]

Stéphane Demri, Valentin Goranko, and Martin Lange. 2016. Temporal Logics in Computer Science: Finite-State Systems. Cambridge University Press. https://doi.org/10.1017/CBO9781139236119

[13]

Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, and Rupak Majumdar. 2015. Model Checking Parameterized Asynchronous Shared-Memory Systems. In Computer Aided Verification-27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 9206 ), Daniel Kroening and Corina S. Pasareanu (Eds.). Springer, 67-84. https://doi.org/10.1007/978-3-319-21690-4_5

[14]

E. Allen Emerson and Charanjit S. Jutla. 1991. Tree Automata, Mu-Calculus and Determinacy (Extended Abstract). In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991. 368-377. https: //doi.org/10.1109/SFCS. 1991.185392

Digital Library

[15]

Javier Esparza, Pierre Ganty, and Rupak Majumdar. 2016. Parameterized Verification of Asynchronous Shared-Memory Systems. J. ACM 63, 1 ( 2016 ), 10 : 1-10 : 48. https://doi.org/10.1145/2842603

Digital Library

[16]

Bernd Finkbeiner. 2017. Temporal Hyperproperties. Bulletin of the EATCS 123 ( 2017 ).

[17]

Bernd Finkbeiner and Christopher Hahn. 2016. Deciding Hyperproperties. In CONCUR 2016. 13 : 1-13 : 14. https://doi.org/10. 4230/LIPIcs.CONCUR. 2016.13

[18]

Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. 2020. Synthesis from hyperproperties. Acta Informatica 57, 1-2 ( 2020 ), 137-163. https://doi.org/10.1007/s00236-019-00358-2

[19]

Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. 2019. Monitoring hyperproperties. Formal Methods Syst. Des. 54, 3 ( 2019 ), 336-363. https://doi.org/10.1007/s10703-019-00334-z

[20]

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

[21]

Olivier Finkel. 2006. On the Accepting Power of 2-Tape Büchi Automata. In STACS 2006, 23rd Annual Symposium on Theoretical Aspects of Computer Science, Marseille, France, February 23-25, 2006, Proceedings. 301-312. https://doi.org/10. 1007/11672142_24

Digital Library

[22]

Olivier Finkel. 2016. Infinite games specified by 2-tape automata. Ann. Pure Appl. Logic 167, 12 ( 2016 ), 1184-1212. https://doi.org/10.1016/j.apal. 2016. 05.005

[23]

Olivier Finkel and Dominique Lecomte. 2009. Decision problems for Turing machines. Inf. Process. Lett. 109, 23-24 ( 2009 ), 1223-1226. https://doi.org/10.1016/j.ipl. 2009. 09.002

Digital Library

[24]

Carlo A. Furia. 2014. Asynchronous Multi-Tape Automata Intersection: Undecidabiliy and Approximation. CoRR abs/1206.4860 ( 2014 ). arXiv: 1206.4860v5 http://arxiv.org/abs/1206.4860v5

[25]

Pierre Ganty and Rupak Majumdar. 2012. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst. 34, 1 ( 2012 ), 6 : 1-6 : 48. https://doi.org/10.1145/2160910.2160915

Digital Library

[26]

Pierre Ganty, Rupak Majumdar, and Andrey Rybalchenko. 2009. Verifying liveness for asynchronous programs. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 102-113. https://doi.org/10.1145/1480881.1480895

Digital Library

[27]

Dainis Geidmanis. 1987. On the Capabilities of Alternating and Nondeterministic Multitape Automata. In Fundamentals of Computation Theory, International Conference FCT' 87, Kazan, USSR, June 22-26, 1987, Proceedings. 150-154. https: //doi.org/10.1007/3-540-18740-5_35

[28]

Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. 2020a. Propositional Dynamic Logic for Hyperproperties. In 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference) (LIPIcs, Vol. 171 ), Igor Konnov and Laura Kovács (Eds.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 50 : 1-50 : 22. https://doi.org/10.4230/LIPIcs.CONCUR. 2020.50

[29]

Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. 2020b. Automata and Fixpoints for Asynchronous Hyperproperties. arXiv: 2010. 11605 [cs.LO]

[30]

Oscar H. Ibarra and Nicholas Q. Trân. 2013. How to synchronize the Heads of a Multitape Automaton. Int. J. Found. Comput. Sci. 24, 6 ( 2013 ), 799-814. https://doi.org/10.1142/S0129054113400194

[31]

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 (LIPIcs, Vol. 117 ), Igor Potapov, Paul G. Spirakis, and James Worrell (Eds.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 10 : 1-10 : 16. https://doi.org/10.4230/LIPIcs.MFCS. 2018.10

[32]

Martin Lange. 2005. Weak Automata for the Linear Time-Calculus. In Verification, Model Checking, and Abstract Interpretation, Radhia Cousot (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 267-281. https://doi.org/10.1007/978-3-540-30579-8_18

Digital Library

[33]

Martin Lange. 2015. The Arity Hierarchy in the Polyadic-Calculus. In FICS (EPTCS, Vol. 191 ). 105-116. https://doi.org/10. 4204/EPTCS.191.10

[34]

Isabella Mastroeni and Michele Pasqua. 2017. Hyperhierarchy of Semantics-A Formal Framework for Hyperproperties Verification. In Static Analysis-24th International Symposium, SAS 2017, New York, NY, USA, August 30-September 1, 2017, Proceedings (Lecture Notes in Computer Science, Vol. 10422 ), Francesco Ranzato (Ed.). Springer, 232-252. https: //doi.org/10.1007/978-3-319-66706-5_12

[35]

Isabella Mastroeni and Michele Pasqua. 2018. Verifying Bounded Subset-Closed Hyperproperties. In Static Analysis-25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 11002 ), Andreas Podelski (Ed.). Springer, 263-283. https://doi.org/10.1007/978-3-319-99725-4_17

[36]

Dimiter Milushev and Dave Clarke. 2013. Incremental Hyperproperty Model Checking via Games. In Proceedings of the 18th Nordic Conference on Secure IT Systems-Volume 8208 ( Ilulissat, Greenland) ( NordSec 2013 ). Springer-Verlag New York, Inc., New York, NY, USA, 247-262. https://doi.org/10.1007/978-3-642-41488-6_17

Digital Library

[37]

Anca Muscholl. 1996. On the Complementation of Asynchronous Cellular Büchi Automata. Theor. Comput. Sci. 169, 2 ( 1996 ), 123-145. https://doi.org/10.1016/S0304-3975 ( 96 ) 00117-X

Digital Library

[38]

Martin Otto. 1999. Bisimulation-invariant PTIME and higher-dimensional-calculus. Theor. Comput. Sci. 224, 1-2 ( 1999 ), 237-265. https://doi.org/10.1016/S0304-3975 ( 98 ) 00314-4

Digital Library

[39]

D. Peled and W. Penczek. 1996. Using Asynchronous Büchi Automata for Eficient Automatic Verification of Concurrent Systems. In Protocol Specification, Testing and Verification XV: Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, June 1995. Springer US, Boston, MA, 315-330. https://doi.org/10.1007/978-0-387-34892-6_20

[40]

Shaz Qadeer. 2008. The Case for Context-Bounded Verification of Concurrent Programs. In Model Checking Software, 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings (Lecture Notes in Computer Science, Vol. 5156 ), Klaus Havelund, Rupak Majumdar, and Jens Palsberg (Eds.). Springer, 3-6. https://doi.org/10.1007/978-3-540-85114-1_2

Digital Library

[41]

Shaz Qadeer and Jakob Rehof. 2005. Context-Bounded Model Checking of Concurrent Software. In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005 (Lecture Notes in Computer Science, Vol. 3440 ), Nicolas Halbwachs and Lenore D. Zuck (Eds.). Springer, 93-107. https://doi.org/10.1007/978-3-540-31980-1_7

Digital Library

[42]

Markus N. Rabe. 2016. A temporal logic approach to Information-flow control. Ph.D. Dissertation. Saarland University.

[43]

Michael O. Rabin and Dana S. Scott. 1959. Finite Automata and Their Decision Problems. IBM Journal of Research and Development 3, 2 ( 1959 ), 114-125. https://doi.org/10.1147/rd.32.0114

Digital Library

[44]

Aravinda Prasad Sistla. 1983. Theoretical Issues in the Design and Verification of Distributed Systems. Ph.D. Dissertation. Carnegie-Mellon University, USA.

[45]

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 (EPTCS, Vol. 73 ), Fang Yu and Chao Wang (Eds.). 20-34. https://doi.org/10.4204/EPTCS.73.5

[46]

Larry Joseph Stockmeyer. 1974. The complexity of decision problems in automata theory and logic. Ph.D. Dissertation. MIT.

[47]

Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 2 ( 1955 ), 285-309. https://projecteuclid.org:443/euclid.pjm/1103044538

[48]

Moshe Y. Vardi. 1988. A Temporal Fixpoint Calculus. In POPL. ACM Press, 250-259. https://doi.org/10.1145/73560.735822

[49]

Wieslaw Zielonka. 1987. Notes on Finite Asynchronous Automata. ITA 21, 2 ( 1987 ), 99-135.

Cited By

Gutsfeld JMüller-Olm MOhrem C(2024)Deciding Asynchronous Hyperproperties for Recursive ProgramsProceedings of the ACM on Programming Languages10.1145/36328448:POPL(33-60)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632844
Chalupa MHenzinger Tda Costa A(2024)Monitoring Extended Hypernode LogicIntegrated Formal Methods10.1007/978-3-031-76554-4_9(151-171)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-76554-4_9
Beutner RHsu TBonakdarpour BFinkbeiner B(2024)Syntax-Guided Automated Program Repair for HyperpropertiesComputer Aided Verification10.1007/978-3-031-65633-0_1(3-26)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_1
Show More Cited By

Index Terms

Automata and fixpoints for asynchronous hyperproperties
1. Theory of computation
  1. Formal languages and automata theory
    1. Automata over infinite objects
  2. Logic
    1. Modal and temporal logics
    2. Verification by model checking

Recommendations

Deciding Asynchronous Hyperproperties for Recursive Programs

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 ...
Temporal Team Semantics Revisited
LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science

In 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 ...
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties

Hoare logics are proof systems that allow one to formally establish properties of computer programs. Traditional Hoare logics prove properties of individual program executions (such as functional correctness). Hoare logic has been generalized to prove ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Deutsche Forschungsgemeinschaft

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
720
Total Downloads

Downloads (Last 12 months)185
Downloads (Last 6 weeks)22

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gutsfeld JMüller-Olm MOhrem C(2024)Deciding Asynchronous Hyperproperties for Recursive ProgramsProceedings of the ACM on Programming Languages10.1145/36328448:POPL(33-60)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632844
Chalupa MHenzinger Tda Costa A(2024)Monitoring Extended Hypernode LogicIntegrated Formal Methods10.1007/978-3-031-76554-4_9(151-171)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-76554-4_9
Beutner RHsu TBonakdarpour BFinkbeiner B(2024)Syntax-Guided Automated Program Repair for HyperpropertiesComputer Aided Verification10.1007/978-3-031-65633-0_1(3-26)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_1
Kontinen JSandström MVirtema J(2024)A Remark on the Expressivity of Asynchronous TeamLTL and HyperLTLFoundations of Information and Knowledge Systems10.1007/978-3-031-56940-1_15(275-286)Online publication date: 8-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-56940-1_15
Finkbeiner B(2023)Logics and Algorithms for HyperpropertiesACM SIGLOG News10.1145/3610392.361039410:2(4-23)Online publication date: 19-Jul-2023
https://dl.acm.org/doi/10.1145/3610392.3610394
Coenen NFinkbeiner BHofmann JTillman J(2023)Smart Contract Synthesis Modulo Hyperproperties2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00006(276-291)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00006
Chalupa MHenzinger T(2023)Monitoring Hyperproperties with Prefix TransducersRuntime Verification10.1007/978-3-031-44267-4_9(168-190)Online publication date: 1-Oct-2023
https://doi.org/10.1007/978-3-031-44267-4_9
Beutner RFinkbeiner BFrenkel HMetzger N(2023)Second-Order HyperpropertiesComputer Aided Verification10.1007/978-3-031-37703-7_15(309-332)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37703-7_15
Hsu TSánchez CSheinvald SBonakdarpour B(2023)Efficient Loop Conditions for Bounded Model Checking HyperpropertiesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30823-9_4(66-84)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30823-9_4
Hsu TBonakdarpour BFinkbeiner BSánchez C(2023)Bounded Model Checking for Asynchronous HyperpropertiesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30823-9_2(29-46)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30823-9_2
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents