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

Article

Bounded Model Checking for Hyperproperties

Authors:

César Sánchez,

Borzoo BonakdarpourAuthors Info & Claims

Tools and Algorithms for the Construction and Analysis of Systems: 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part I

Pages 94 - 112

https://doi.org/10.1007/978-3-030-72016-2_6

Published: 27 March 2021 Publication History

Abstract

This paper introduces a bounded model checking (BMC) algorithm for hyperproperties expressed in HyperLTL, which — to the best of our knowledge — is the first such algorithm. Just as the classic BMC technique for LTL primarily aims at finding bugs, our approach also targets identifying counterexamples. BMC for LTL is reduced to SAT solving, because LTL describes a property via inspecting individual traces. Our BMC approach naturally reduces to QBF solving, as HyperLTL allows explicit and simultaneous quantification over multiple traces. We report on successful and efficient model checking, implemented in our tool called HyperQube, of a rich set of experiments on a variety of case studies, including security, concurrent data structures, path planning for robots, and mutation testing.

References

[1]

Shreya Agrawal and Borzoo Bonakdarpour. Runtime verification of

k

-safety hyperproperties in HyperLTL. In Proc. of the 29th IEEE Computer Security Foundations Symposium (CSF’16), pages 239–252. IEEE, 2016.

[2]

Borzoo Bonakdarpour and Bernd Finkbeiner. The complexity of monitoring hyperproperties. In Proc. of the IEEE 31st Computer Security Foundations Symposium (CSF’18), pages 162–174. IEEE, 2018.

[3]

Borzoo Bonakdarpour and Bernd Finkbeiner. Program repair for hyperproperties. In Proc. of the 17th Symposium on Automated Technology for Verification and Analysis (ATVA’19), volume 11781 of LNCS, pages 423–441. Springer, 2019.

[4]

Borzoo Bonakdarpour and Bernd Finkbeiner. Controller synthesis for hyperproperties. In Proc. of the 33rd IEEE Computer Security Foundations Symposium (CSF’20), pages 366–379. IEEE, 2020.

[5]

Borzoo Bonakdarpour, Pavithra Prabhakar, and César Sánchez. Model checking timed hyperproperties in discrete-time systems. In Proc. of the 12th NASA Formal Methods Symposium (NFM’20), volume 12229 of LNCS, pages 311–328. Springer, 2020.

[6]

Borzoo Bonakdarpour, César Sánchez, and Gerardo Schneider. Monitoring hyperproperties by combining static analysis and runtime verification. In Proc. of the 8th Int’l Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’18), Part II, volume 11245 of LNCS, pages 8–27. Springer, 2018.

[7]

Noel Brett, Umair Siddique, and Borzoo Bonakdarpour. Rewriting-based runtime verification for alternation-free HyperLTL. In Proc. of the 23rd Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17), Part II, volume 10206 of LNCS, pages 77–93. Springer, 2017.

[8]

Edmund M. Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7–34, 2001.

[9]

Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In Proc. of the 3rd Int’l Conf. on Principles of Security and Trust (POST’14), volume 8414 of LNCS, pages 265–284. Springer, 2014.

[10]

Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157–1210, 2010.

[11]

Norine Coenen, Bernd Finkbeiner, Cristopher Hahn, and Jana Hofmann. The hierarchy of hyperlogics. In Proc. of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’19), pages 1–13. IEEE, 2019.

[12]

Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. Verifying hyperliveness. In Proc. of the 31st Int’l Conf. on Computer Aided Verification (CAV’19), Part I, volume 11561 of LNCS, pages 121–139. Springer, 2019.

[13]

Leonardo de Moura and Nikolaj Bjorner. Z3 – a tutorial. Technical report, Microsoft, 2012.

[14]

Simon Doherty, David Detlefs, Lindsay Groves, Christine H. Flood, Victor Luchangco, Paul Alan Martin, Mark Moir, Nir Shavit, and Guy L. Steele Jr. DCAS is not a silver bullet for nonblocking algorithm design. In Proc. of the 16th Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA’04), pages 216–224. ACM, 2004.

[15]

Andreas Fellner, Mitra Tabaei Befrouei, and Georg Weissenbacher. Mutation testing with hyperproperties. In Proc. of the 17th Int’l Conf. on Software Engineering and Formal Methods (SEFM’19), volume 11724 of LNCS, pages 203–221. Springer, 2019.

[16]

Bernd Finkbeiner and Cristopher Hahn. Deciding hyperproperties. In Proc. of the 27th Int’l Conf. on Concurrency Theory (CONCUR’16), volume 59 of LIPIcs, pages 13:1–13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.

[17]

Bernd Finkbeiner, Cristopher Hahn, and Tobias Hans. MGHyper: Checking satisfiability of HyperLTL formulas beyond the

\exists^{*} \forall^{*}

fragment. In Proc. of the 16th Int’l Symposium on Automated Technology for Verification and Analysis (ATVA’18), volume 11138 of LNCS, pages 521–527. Springer, 2018.

[18]

Bernd Finkbeiner, Cristopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. Synthesis from hyperproperties. Acta Informatica, 57(1-2):137–163, 2020.

[19]

Bernd Finkbeiner, Cristopher Hahn, and Marvin Stenger. Eahyper: Satisfiability, implication, and equivalence checking of hyperproperties. In Proc. of the 29th Int’l Conf. on Computer Aided Verification (CAV’17), Part II, volume 10427 of LNCS, pages 564–570. Springer, 2017.

[20]

Bernd Finkbeiner, Cristopher Hahn, Marvin Stenger, and Leander Tentrup. RVHyper: A runtime verification tool for temporal hyperproperties. In Proc. of the 24th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18), Part II, volume 10806 of LNCS, pages 194–200. Springer, 2018.

[21]

Bernd Finkbeiner, Cristopher Hahn, Marvin Stenger, and Leander Tentrup. Monitoring hyperproperties. Formal Methods in System Design, 54(3):336–363, 2019.

[22]

Bernd Finkbeiner, Cristopher Hahn, and Hazem Torfah. Model checking quantitative hyperproperties. In Proc. of the 30th Int’l Conf. on Computer Aided Verification (CAV’18), Part I, volume 10981 of LNCS, pages 144–163. Springer, 2018.

[23]

Bernd Finkbeiner, Christian Müller, Helmut Seidl, and Eugene Zalinescu. Verifying security policies in multi-agent workflows with loops. In Proc. of the 15th ACM Conf. on Computer and Communications Security (CCS’17), pages 633–645. ACM, 2017.

[24]

Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for model checking HyperLTL and HyperCTL*. In Proc. of the 27th Int’l Conf. on Computer Aided Verification (CAV’15), Part I, volume 9206 of LNCS, pages 30–48. Springer, 2015.

[25]

Joseph A. Goguen and José Meseguer. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy, pages 11–20. IEEE Computer Society, 1982.

[26]

Cristopher Hahn, Marvin Stenger, and Leander Tentrup. Constraint-based monitoring of hyperproperties. In Proc. of the 25th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’19), volume 11428 of LNCS, pages 115–131. Springer, 2019.

[27]

Klaus Havelund and Doron Peled. Runtime verification: From propositional to first-order temporal logic. In Proc. of the 18th Int’l Conf. on Runtime Verification (RV’18), volume 11237 of LNCS, pages 90–112. Springer, 2018.

[28]

Jesko Hecking-Harbusch and Leander Tentrup. Solving QBF by abstraction. In Proc. of the 9th Int’l Symposium on Games, Automata, Logics and Formal Verification (GandALF’18), volume 277 of EPTCS, pages 88–102, 2018.

[29]

Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 12(3):463–492, 1990.

[30]

Tzu-Han Hsu, César Sánchez, and Borzoo Bonakdarpour. Bounded model checking for hyperproperties. CoRR, abs/2009.08907, 2020.

[31]

Wojciech Jamroga, Sjouke Mauw, and Matthijs Melissen. Fairness in non-repudiation protocols. In Proc. of the 7th Int’l Workshop on Security and Trust Management (STM’11), volume 7170 of LNCS, pages 122–139. Springer, 2011.

[32]

Geoffrey Smith and Dennis M. Volpano. Secure information flow in a multi-threaded imperative language. In Proc. of the 25th ACM Symposium on Principles of Programming Languages (POPL’98), pages 355–364. ACM, 1998.

[33]

Sandro Stucki, César Sánchez, Gerardo Schneider, and Borzoo Bonakdarpour. Graybox monitoring of hyperproperties. In Proc. of the 23rd Int’l Symposium on Formal Methods (FM’19), volume 11800 of LNCS, pages 406–424. Springer, 2019.

[34]

Yu Wang, Siddharta Nalluri, and Miroslav Pajic. Hyperproperties for robotics: Planning via HyperLTL. In 2020 IEEE Int’l Conf. on Robotics and Automation (ICRA’20), pages 8011–8017. IEEE, 2020.

[35]

Yu Wang, Mojtaba Zarei, Borzoo Bonakdarpour, and Miroslav Pajic. Statistical verification of hyperproperties for cyber-physical systems. ACM Transactions on Embedded Computing systems, 18(5s):92:1–92:23, 2019.

Cited By

Correnson ANießen TFinkbeiner BWeissenbacher G(2024)Finding ∀∃ Hyperbugs using Symbolic ExecutionProceedings of the ACM on Programming Languages10.1145/36897618:OOPSLA2(1420-1445)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689761
Beutner RFinkbeiner BGöbl A(2024)Visualizing Game-Based Certificates for Hyperproperty VerificationFormal Methods10.1007/978-3-031-71177-0_5(67-75)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71177-0_5
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

Bounded Model Checking for Hyperproperties
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Index terms have been assigned to the content through auto-classification.

Recommendations

Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology

Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
Evaluation of SAT-based Bounded Model Checking of ACTL Properties
TASE '07: Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering

Bounded model checking (BMC) based on SAT has been introduced as a complementary method to BDDbased symbolic model checking of LTL and ACTL properties in recent years. For general LTL and ACTL properties, BMC has traditionally aimed mainly at error ...
Three-valued logic in bounded model checking
MEMOCODE '05: Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design

In principle, bounded model checking (BMC) leads to semi-decision procedures that can be used to verify liveness properties and to falsify safety properties. If the procedures fail, there is usually no information about the validity of the considered ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Tools and Algorithms for the Construction and Analysis of Systems: 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part I

Mar 2021

482 pages

ISBN:978-3-030-72015-5

DOI:10.1007/978-3-030-72016-2

Editors:
Jan Friso Groote
Eindhoven University of Technology, Eindhoven, The Netherlands
,
Kim Guldstrand Larsen
Aalborg University, Aalborg East, Denmark

© The Author(s) 2021.

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 March 2021

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Correnson ANießen TFinkbeiner BWeissenbacher G(2024)Finding ∀∃ Hyperbugs using Symbolic ExecutionProceedings of the ACM on Programming Languages10.1145/36897618:OOPSLA2(1420-1445)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689761
Beutner RFinkbeiner BGöbl A(2024)Visualizing Game-Based Certificates for Hyperproperty VerificationFormal Methods10.1007/978-3-031-71177-0_5(67-75)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71177-0_5
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
Beutner R(2024)Automated Software Verification of HyperlivenessTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_10(196-216)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57249-4_10
Bonnah ENguyen LHoque KZhu Qvon Hanxleden RStephen EBrandt J(2023)Model Checking Time Window Temporal Logic for HyperpropertiesProceedings of the 21st ACM-IEEE International Conference on Formal Methods and Models for System Design10.1145/3610579.3611077(100-110)Online publication date: 21-Sep-2023
https://dl.acm.org/doi/10.1145/3610579.3611077
Beutner RFinkbeiner BFrenkel HSiber J(2023)Checking and Sketching Causes on Temporal SequencesAutomated Technology for Verification and Analysis10.1007/978-3-031-45332-8_18(314-327)Online publication date: 24-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45332-8_18
Dobe OSchupp SBartocci EBonakdarpour BLegay APajic MWang Y(2023)Lightweight Verification of HyperpropertiesAutomated Technology for Verification and Analysis10.1007/978-3-031-45332-8_1(3-25)Online publication date: 24-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45332-8_1
Coenen NDachselt RFinkbeiner BFrenkel HHahn CHorak TMetzger NSiber J(2022)Explaining Hyperproperty ViolationsComputer Aided Verification10.1007/978-3-031-13185-1_20(407-429)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_20
Zaman ECiardo GÁbrahám EBonakdarpour B(2022)HyperPCTL Model Checking by Probabilistic DecompositionIntegrated Formal Methods10.1007/978-3-031-07727-2_12(209-226)Online publication date: 7-Jun-2022
https://dl.acm.org/doi/10.1007/978-3-031-07727-2_12
Baumeister JCoenen NBonakdarpour BFinkbeiner BSánchez C(2021)A Temporal Logic for Asynchronous HyperpropertiesComputer Aided Verification10.1007/978-3-030-81685-8_33(694-717)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81685-8_33

View Options

View options

Media

Figures

Other

Tables

View Table of Contents