research-article

Open access

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties

Authors:

Thibault Dardinier,

Peter MüllerAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 8, Issue PLDI

Article No.: 207, Pages 1485 - 1509

https://doi.org/10.1145/3656437

Published: 20 June 2024 Publication History

Abstract

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 also properties of multiple executions of a program (so-called hyperproperties, such as determinism or non-interference). These program logics prove the absence of (bad combinations of) executions. On the other hand, program logics similar to Hoare logic have been proposed to disprove program properties (e.g., Incorrectness Logic), by proving the existence of (bad combinations of) executions. All of these logics have in common that they specify program properties using assertions over a fixed number of states, for instance, a single pre- and post-state for functional properties or pairs of pre- and post-states for non-interference. In this paper, we present Hyper Hoare Logic, a generalization of Hoare logic that lifts assertions to properties of arbitrary sets of states. The resulting logic is simple yet expressive: its judgments can express arbitrary program hyperproperties, a particular class of hyperproperties over the set of terminating executions of a program (including properties of individual program executions). By allowing assertions to reason about sets of states, Hyper Hoare Logic can reason about both the absence and the existence of (combinations of) executions, and, thereby, supports both proving and disproving program (hyper-)properties within the same logic, including (hyper-)properties that no existing Hoare logic can express. We prove that Hyper Hoare Logic is sound and complete, and demonstrate that it captures important proof principles naturally. All our technical results have been proved in Isabelle/HOL.

References

[1]

Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub. 2017. A relational logic for higher-order programs. Proceedings of the ACM on Programming Languages, 1, ICFP (2017), 1–29.

Digital Library

[2]

Torben Amtoft, Sruthi Bandhakavi, and Anindya Banerjee. 2006. A Logic for Information Flow in Object-Oriented Programs. SIGPLAN Not., 41, 1 (2006), jan, 91–102. issn:0362-1340 https://doi.org/10.1145/1111320.1111046

Digital Library

[3]

Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo. 2023. An Algebra of Alignment for Relational Verification. Proc. ACM Program. Lang., 7, POPL (2023), Article 20, jan, 31 pages. https://doi.org/10.1145/3571213

Digital Library

[4]

Mounir Assaf, David A Naumann, Julien Signoles, Eric Totel, and Frédéric Tronel. 2017. Hypercollecting semantics and its application to static analysis of information flow. ACM SIGPLAN Notices, 52, 1 (2017), 874–887.

Digital Library

[5]

Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011. Relational verification using product programs. In International Symposium on Formal Methods. 200–214.

[6]

Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2013. Beyond 2-safety: Asymmetric product programs for relational program verification. In International Symposium on Logical Foundations of Computer Science. 29–43.

[7]

Gilles Barthe, Pedro R D’argenio, and Tamara Rezk. 2011. Secure information flow by self-composition. Mathematical Structures in Computer Science, 21, 6 (2011), 1207–1252.

Digital Library

[8]

Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, and Matteo Maffei. 2019. Verifying relational properties using trace logic. In 2019 Formal Methods in Computer Aided Design (FMCAD). 170–178.

[9]

Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. An assertion-based program logic for probabilistic programs. In European Symposium on Programming. 117–144.

[10]

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, and Pierre-Yves Strub. 2014. Proving differential privacy in Hoare logic. In 2014 IEEE 27th Computer Security Foundations Symposium. 411–424.

Digital Library

[11]

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2009. Formal certification of code-based cryptographic proofs. In Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 90–101.

Digital Library

[12]

Gilles Barthe, Justin Hsu, and Kevin Liao. 2019. A Probabilistic Separation Logic. Proc. ACM Program. Lang., 4, POPL (2019), Article 55, dec, 30 pages. https://doi.org/10.1145/3371123

Digital Library

[13]

Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’04). Association for Computing Machinery, New York, NY, USA. 14–25. isbn:158113729X https://doi.org/10.1145/964001.964003

Digital Library

[14]

Raven Beutner and Bernd Finkbeiner. 2022. Software Verification of Hyperproperties Beyond k-Safety. In Computer Aided Verification, Sharon Shoham and Yakir Vizel (Eds.). Cham. 341–362. isbn:978-3-031-13185-1

[15]

Raven Beutner and Bernd Finkbeiner. 2023. AutoHyper: Explicit-State Model Checking for HyperLTL. In Tools and Algorithms for the Construction and Analysis of Systems, Sriram Sankaranarayanan and Natasha Sharygina (Eds.). Springer Nature Switzerland, Cham. 145–163. isbn:978-3-031-30823-9

[16]

Sam Blackshear, Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey. 2018. RacerD: Compositional Static Race Detection. Proc. ACM Program. Lang., 2, OOPSLA (2018), Article 144, oct, 28 pages. https://doi.org/10.1145/3276514

Digital Library

[17]

Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. 2021. A Logic for Locally Complete Abstract Interpretations. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1–13. https://doi.org/10.1109/LICS52264.2021.9470608

Digital Library

[18]

Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. 2023. A Correctness and Incorrectness Program Logic. J. ACM, 70, 2 (2023), Article 15, mar, 45 pages. issn:0004-5411 https://doi.org/10.1145/3582267

Digital Library

[19]

Michael R Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K Micinski, Markus N Rabe, and César Sánchez. 2014. Temporal logics for hyperproperties. In International Conference on Principles of Security and Trust. 265–284.

[20]

Michael R. Clarkson and Fred B. Schneider. 2008. Hyperproperties. In 21st IEEE Computer Security Foundations Symposium. 51–65. https://doi.org/10.1109/CSF.2008.7

Digital Library

[21]

Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. 2019. Verifying hyperliveness. In International Conference on Computer Aided Verification. 121–139.

[22]

Ricardo Corin and Jerry Den Hartog. 2006. A probabilistic Hoare-style logic for game-based cryptographic proofs. In International Colloquium on Automata, Languages, and Programming. 252–263.

[23]

David Costanzo and Zhong Shao. 2014. A Separation Logic for Enforcing Declarative Information Flow Control Policies. In Principles of Security and Trust, Martín Abadi and Steve Kremer (Eds.). 179–198. isbn:978-3-642-54792-8

[24]

Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 238–252.

Digital Library

[25]

Thibault Dardinier. 2023. Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties. Archive of Formal Proofs, April, issn:2150-914x https://isa-afp.org/entries/HyperHoareLogic.html

[26]

Thibault Dardinier and Peter Müller. 2023. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version). arxiv:cs.LO/2301.10037.

[27]

Thibault Dardinier and Peter Müller. 2024. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (artifact). https://doi.org/10.5281/zenodo.10808236

[28]

Edsko de Vries and Vasileios Koutavas. 2011. Reverse Hoare Logic. In Software Engineering and Formal Methods, Gilles Barthe, Alberto Pardo, and Gerardo Schneider (Eds.). 155–171. isbn:978-3-642-24690-6

[29]

JI Den Hartog and Erik P de Vink. 2002. Verifying probabilistic programs using a Hoare like logic. International journal of foundations of computer science, 13, 03 (2002), 315–340.

[30]

Robert Dickerson, Qianchuan Ye, Michael K. Zhang, and Benjamin Delaware. 2022. RHLE: Modular Deductive Verification of Relational ∀ ∃ Properties. In Programming Languages and Systems: 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings. 67–87. isbn:978-3-031-21036-5 https://doi.org/10.1007/978-3-031-21037-2_4

Digital Library

[31]

Dino Distefano, Manuel Fähndrich, Francesco Logozzo, and Peter W. O’Hearn. 2019. Scaling Static Analyses at Facebook. Commun. ACM, 62, 8 (2019), jul, 62–70. issn:0001-0782 https://doi.org/10.1145/3338112

Digital Library

[32]

Emanuele D’Osualdo, Azadeh Farzan, and Derek Dreyer. 2022. Proving Hypersafety Compositionally. Proc. ACM Program. Lang., 6, OOPSLA2 (2022), Article 135, oct, 26 pages. https://doi.org/10.1145/3563298

Digital Library

[33]

Marco Eilers, Thibault Dardinier, and Peter Müller. 2023. CommCSL: Proving Information Flow Security for Concurrent Programs Using Abstract Commutativity. Proc. ACM Program. Lang., 7, PLDI (2023), Article 175, jun, 26 pages. https://doi.org/10.1145/3591289

Digital Library

[34]

Marco Eilers, Peter Müller, and Samuel Hitz. 2019. Modular product programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 42, 1 (2019), 1–37.

Digital Library

[35]

Gidon Ernst and Toby Murray. 2019. SecCSL: Security Concurrent Separation Logic. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Cham. 208–230. isbn:978-3-030-25543-5

[36]

Robert W. Floyd. 1967. Assigning Meanings to Programs. Proceedings of Symposium in Applied Mathematics, 19–32.

[37]

Nissim Francez. 1983. Product properties and their direct verification. Acta informatica, 20, 4 (1983), 329–344.

[38]

Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey. 2019. A True Positives Theorem for a Static Race Detector. Proc. ACM Program. Lang., 3, POPL (2019), Article 57, jan, 29 pages. https://doi.org/10.1145/3290370

Digital Library

[39]

David Harel. 1979. First-order dynamic logic. Springer.

[40]

C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM, 12, 10 (1969), oct, 576–580. issn:0001-0782 https://doi.org/10.1145/363235.363259

Digital Library

[41]

Tzu-Han Hsu, César Sánchez, and Borzoo Bonakdarpour. 2021. Bounded Model Checking for Hyperproperties. In Tools and Algorithms for the Construction and Analysis of Systems, Jan Friso Groote and Kim Guldstrand Larsen (Eds.). Springer International Publishing, Cham. 94–112. isbn:978-3-030-72016-2

[42]

Thomas Kleymann. 1999. Hoare Logic and Auxiliary Variables. Form. Asp. Comput., 11, 5 (1999), dec, 541–566. issn:0934-5043 https://doi.org/10.1007/s001650050057

Digital Library

[43]

Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Finding Real Bugs in Big Programs with Incorrectness Logic. Proc. ACM Program. Lang., 6, OOPSLA1 (2022), Article 81, apr, 27 pages. https://doi.org/10.1145/3527325

Digital Library

[44]

K. Rustan M. Leino. 2008. This is Boogie 2. June, https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/

[45]

Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas, and Antoine Van Muylder. 2019. The next 700 Relational Program Logics. Proc. ACM Program. Lang., 4, POPL (2019), Article 4, dec, 33 pages. https://doi.org/10.1145/3371072

Digital Library

[46]

Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner. 2023. Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). 263, 19:1–19:27. isbn:978-3-95977-281-5 issn:1868-8969 https://doi.org/10.4230/LIPIcs.ECOOP.2023.19

[47]

Daryl McCullough. 1987. Specifications for multi-level security and a hook-up. In 1987 IEEE Symposium on Security and Privacy. 161–161.

[48]

John McLean. 1996. A general theory of composition for a class of" possibilistic" properties. IEEE Transactions on Software Engineering, 22, 1 (1996), 53–67.

Digital Library

[49]

Bernhard Möller, Peter O’Hearn, and Tony Hoare. 2021. On Algebra of Program Correctness and Incorrectness. In Relational and Algebraic Methods in Computer Science, Uli Fahrenberg, Mai Gehrke, Luigi Santocanale, and Michael Winter (Eds.). Cham. 325–343. isbn:978-3-030-88701-8

[50]

Toby Murray. 2020. An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation and More. https://doi.org/10.48550/ARXIV.2003.04791

[51]

David A. Naumann. 2020. Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History. In Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles, Tiziana Margaria and Bernhard Steffen (Eds.). Cham. 93–116. isbn:978-3-030-61470-6

[52]

David A. Naumann and Minh Ngo. 2019. Whither Specifications as Programs. In Unifying Theories of Programming, Pedro Ribeiro and Augusto Sampaio (Eds.). Springer International Publishing, Cham. 39–61. isbn:978-3-030-31038-7

[53]

Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, Berlin, Heidelberg. isbn:3540433767

Digital Library

[54]

Peter W. O’Hearn. 2019. Incorrectness Logic. Proc. ACM Program. Lang., 4, POPL (2019), Article 10, dec, 32 pages. https://doi.org/10.1145/3371078

Digital Library

[55]

Michele Pasqua. 2019. Hyper Static Analysis of Programs – An Abstract Interpretation-Based Framework for Hyperproperties Verification. University of Verona. https://doi.org/10.5281/zenodo.6584085

[56]

Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O’Hearn, and Jules Villard. 2020. Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. In Computer Aided Verification. Cham. 225–252. isbn:978-3-030-53291-8

[57]

Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Concurrent Incorrectness Separation Logic. Proc. ACM Program. Lang., 6, POPL (2022), Article 34, jan, 29 pages. https://doi.org/10.1145/3498695

Digital Library

[58]

Lyle Harold Ramshaw. 1979. Formalizing the Analysis of Algorithms. Stanford University.

[59]

Robert Rand and Steve Zdancewic. 2015. VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. Electronic Notes in Theoretical Computer Science, 319 (2015), 351–367. issn:1571-0661 https://doi.org/10.1016/j.entcs.2015.12.021 The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI).

Digital Library

[60]

C. E. Shannon. 1948. A mathematical theory of communication. The Bell System Technical Journal, 27, 3 (1948), 379–423. https://doi.org/10.1002/j.1538-7305.1948.tb01338.x

[61]

Geoffrey Smith. 2009. On the Foundations of Quantitative Information Flow. In Foundations of Software Science and Computational Structures, Luca de Alfaro (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 288–302. isbn:978-3-642-00596-1

[62]

Marcelo Sousa and Isil Dillig. 2016. Cartesian Hoare Logic for Verifying K-Safety Properties. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). Association for Computing Machinery, New York, NY, USA. 57–69. isbn:9781450342612 https://doi.org/10.1145/2908080.2908092

Digital Library

[63]

Tachio Terauchi and Alex Aiken. 2005. Secure information flow as a safety problem. In International Static Analysis Symposium. 352–367.

Digital Library

[64]

Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. 2021. Constraint-Based Relational Verification. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer International Publishing, Cham. 742–766. isbn:978-3-030-81685-8

[65]

Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 1996. A sound type system for secure flow analysis. Journal of computer security, 4, 2-3 (1996), 167–187.

Digital Library

[66]

Hongseok Yang. 2007. Relational separation logic. Theoretical Computer Science, 375, 1 (2007), 308–334. issn:0304-3975 https://doi.org/10.1016/j.tcs.2006.12.036

Digital Library

[67]

Hirotoshi Yasuoka and Tachio Terauchi. 2010. On Bounding Problems of Quantitative Information Flow. In Computer Security – ESORICS 2010, Dimitris Gritzalis, Bart Preneel, and Marianthi Theoharidou (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 357–372. isbn:978-3-642-15497-3

[68]

Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. Proc. ACM Program. Lang., 7, OOPSLA1 (2023), Article 93, apr, 29 pages. https://doi.org/10.1145/3586045

Digital Library

Cited By

Dardinier TLi AMüller P(2024)Hypra: A Deductive Program Verifier for Hyper Hoare LogicProceedings of the ACM on Programming Languages10.1145/36897568:OOPSLA2(1279-1308)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689756
Zhang LZilberstein NKaminski BSilva A(2024)Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate TransformersProceedings of the ACM on Programming Languages10.1145/36897408:OOPSLA2(817-845)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689740
Zilberstein NSridharan M(2024)Unified Analysis Techniques for Programs with OutcomesCompanion Proceedings of the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity10.1145/3689491.3691814(4-6)Online publication date: 20-Oct-2024
https://dl.acm.org/doi/10.1145/3689491.3691814
Show More Cited By

Index Terms

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
1. Theory of computation
  1. Logic
    1. Hoare logic
    2. Logic and verification

Recommendations

Hypra: A Deductive Program Verifier for Hyper Hoare Logic

Hyperproperties relate multiple executions of a program and are useful to express common correctness properties (such as determinism) and security properties (such as non-interference). While there are a number of powerful program logics for the ...
A Correctness and Incorrectness Program Logic
Abstract interpretation is a well-known and extensively used method to extract over-approximate program invariants by a sound program analysis algorithm. Soundness means that no program errors are lost and it is, in principle, guaranteed by construction. ...
On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties
Logic, Language, Information, and Computation
Abstract
In this article we study linear temporal logics with team semantics ( $TeamLTL$ ) that are novel logics for defining hyperproperties. We define Kamp-type translations of these logics into fragments of first-order team logic and second-order logic. We ...

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 8, Issue PLDI

June 2024

2198 pages

EISSN:2475-1421

DOI:10.1145/3554317

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2024 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: 20 June 2024

Published in PACMPL Volume 8, Issue PLDI

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Swiss National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
363
Total Downloads

Downloads (Last 12 months)363
Downloads (Last 6 weeks)121

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dardinier TLi AMüller P(2024)Hypra: A Deductive Program Verifier for Hyper Hoare LogicProceedings of the ACM on Programming Languages10.1145/36897568:OOPSLA2(1279-1308)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689756
Zhang LZilberstein NKaminski BSilva A(2024)Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate TransformersProceedings of the ACM on Programming Languages10.1145/36897408:OOPSLA2(817-845)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689740
Zilberstein NSridharan M(2024)Unified Analysis Techniques for Programs with OutcomesCompanion Proceedings of the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity10.1145/3689491.3691814(4-6)Online publication date: 20-Oct-2024
https://dl.acm.org/doi/10.1145/3689491.3691814
Gladshtein VZhao QAhrens WAmarasinghe SSergey I(2024)Mechanised Hypersafety Proofs about Structured DataProceedings of the ACM on Programming Languages10.1145/36564038:PLDI(647-670)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656403
Kondratyev D(2023)Logic for reasoning about bugs in loops over data sequences (IFIL)Modeling and Analysis of Information Systems10.18255/1818-1015-2023-3-214-23330:3(214-233)Online publication date: 17-Sep-2023
https://doi.org/10.18255/1818-1015-2023-3-214-233

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