Lightweight Verification of Hyperproperties
Authors: 
Oyendrila Dobe, Stefan Schupp, Ezio Bartocci, Borzoo Bonakdarpour, Axel Legay, 
Miroslav Pajic, Yu WangAuthors Info & Claims
Pages 3 - 25
Abstract
Hyperproperties have been widely used to express system properties like noninterference, observational determinism, conformance, robustness, etc. However, the model checking problem for hyperproperties is challenging due to its inherent complexity of verifying properties across sets of traces and suffers from scalability issues. Previously, statistical approaches have proven effective in tackling the scalability of model checking for temporal logic. In this work, we have attempted to combine these two concepts to propose a tractable solution to model checking of hyperproperties expressed as HyperLTL on models involving nondeterminism. We have implemented our approach in PLASMA and experimented with a range of case studies to showcase its effectiveness.
References
[1]
PRISM: dining cryptographers’ problem. https://www.prismmodelchecker.org/casestudies/dining_crypt.php
[2]
Ábrahám, E., Bonakdarpour, B.: HyperPCTL: a temporal logic for probabilistic hyperproperties. In: Proceedings of the 15th International Conference on Quantitative Evaluation of Systems (QEST), pp. 20–35 (2018)
[3]
Ábrahám E, Bartocci E, Bonakdarpour B, and Dobe O Hung DV and Sokolsky O Probabilistic hyperproperties with nondeterminism Automated Technology for Verification and Analysis 2020 Cham Springer 518-534
[4]
Agha G and Palmskog K A survey of statistical model checking ACM Trans. Model. Comput. Simul. 2018 28 1 1-39
[5]
Agrawal, S., Bonakdarpour, B.: Runtime verification of k-safety hyperproperties in HyperLTL. In: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp. 239–252. IEEE, Lisbon (2016).
[6]
Arora S, Hansen RR, Larsen KG, Legay A, and Poulsen DB Legunsen O and Rosu G Statistical model checking for probabilistic hyperproperties of real-valued signals Model Checking Software, SPIN 2022 2022 Cham Springer 61-78
[7]
Baier C and Katoen JP Principles of Model Checking 2008 Cambridge MIT Press
[8]
Baumeister J, Coenen N, Bonakdarpour B, Finkbeiner B, and Sánchez C Silva A and Leino KRM A temporal logic for asynchronous hyperproperties Computer Aided Verification 2021 Cham Springer 694-717
[9]
Beauxis R and Palamidessi C Probabilistic and nondeterministic aspects of anonymity Theoret. Comput. Sci. 2009 410 41 4006-4025
[10]
Bonakdarpour B, Sanchez C, and Schneider G Margaria T and Steffen B Monitoring hyperproperties by combining static analysis and runtime verification Leveraging Applications of Formal Methods, Verification and Validation. Verification 2018 Cham Springer 8-27
[11]
Bonakdarpour, B., Finkbeiner, B.: The complexity of monitoring hyperproperties. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 162–174 (2018).
[12]
Boyer B, Corre K, Legay A, and Sedwards S Joshi K, Siegle M, Stoelinga M, and D’Argenio PR PLASMA-lab: a flexible, distributable statistical model checking library Quantitative Evaluation of Systems 2013 Heidelberg Springer 160-164
[13]
Bulychev, P., et al.: UPPAAL-SMC: statistical model checking for priced timed automata. arXiv preprint arXiv:1207.1272 (2012)
[14]
Cavalcante E, Quilbeuf J, Traonouez L-M, Oquendo F, Batista T, and Legay A Tekinerdogan B, Zdun U, and Babar A Statistical model checking of dynamic software architectures Software Architecture 2016 Cham Springer 185-200
[15]
Chaum D The dining cryptographers problem: unconditional sender and recipient untraceability J. Cryptol. 1988 1 1 65-75
[16]
Clarke EM and Zuliani P Bultan T and Hsiung P-A Statistical model checking for cyber-physical systems Automated Technology for Verification and Analysis 2011 Heidelberg Springer 1-12
[17]
Clarkson MR, Finkbeiner B, Koleini M, Micinski KK, Rabe MN, and Sánchez C Abadi M and Kremer S Temporal logics for hyperproperties Principles of Security and Trust 2014 Heidelberg Springer 265-284
[18]
Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: 2008 21st IEEE Computer Security Foundations Symposium, pp. 51–65. IEEE, Pittsburgh, PA, USA (2008).
[19]
Coenen N, Finkbeiner B, Sánchez C, and Tentrup L Dillig I and Tasiran S Verifying hyperliveness Computer Aided Verification 2019 Cham Springer 121-139
[20]
D’Argenio P, Legay A, Sedwards S, and Traonouez LM Smart sampling for lightweight verification of Markov decision processes Int. J. Softw. Tools Technol. Transfer 2015 17 4 469-484
[21]
Das, S., Prabhakar, P.: Bayesian statistical model checking for multi-agent systems using HyperPCTL* (2022)
[22]
Dimitrova R, Finkbeiner B, and Torfah H Hung DV and Sokolsky O Probabilistic hyperproperties of Markov decision processes Automated Technology for Verification and Analysis 2020 Cham Springer 484-500
[23]
Dobe O, Ábrahám E, Bartocci E, and Bonakdarpour B Huisman M, Păsăreanu C, and Zhan N HyperProb: a model checker for probabilistic hyperproperties Formal Methods 2021 Cham Springer 657-666
[24]
Dobe O, Ábrahám E, Bartocci E, and Bonakdarpour B Model checking hyperproperties for Markov decision processes Inf. Comput. 2022 289 104978
[25]
Dobe O, Wilke L, Ábrahám E, Bartocci E, and Bonakdarpour B Deshmukh JV, Havelund K, and Perez I Probabilistic hyperproperties with rewards NASA Formal Methods 2022 Cham Springer 656-673
[26]
Dwork C Bugliesi M, Preneel B, Sassone V, and Wegener I Differential privacy Automata, Languages and Programming 2006 Heidelberg Springer 1-12
[27]
Finkbeiner B, Hahn C, and Hans T Lahiri SK and Wang C MGHyper: checking satisfiability of HyperLTL formulas beyond the fragment Automated Technology for Verification and Analysis 2018 Cham Springer 521-527
[28]
Finkbeiner B, Hahn C, and Stenger M Majumdar R and Kunčak V EAHyper: satisfiability, implication, and equivalence checking of hyperproperties Computer Aided Verification 2017 Cham Springer 564-570
[29]
Finkbeiner B, Hahn C, Stenger M, and Tentrup L Lahiri S and Reger G Monitoring hyperproperties Runtime Verification 2017 Cham Springer 190-207
[30]
Finkbeiner B, Hahn C, Stenger M, and Tentrup L Beyer D and Huisman M : A runtime verification tool for temporal hyperproperties Tools and Algorithms for the Construction and Analysis of Systems 2018 Cham Springer 194-200
[31]
Finkbeiner B, Hahn C, and Torfah H Chockler H and Weissenbacher G Model checking quantitative hyperproperties Computer Aided Verification 2018 Cham Springer 144-163
[32]
Finkbeiner, B., Müller, C., Seidl, H., Zalinescu, E.: Verifying security policies in multi-agent workflows with loops. In: Proceedings of the CCS 2017 (2017)
[33]
Finkbeiner B, Rabe MN, and Sánchez C Kroening D and Păsăreanu CS Algorithms for model checking HyperLTL and HyperCTL Computer Aided Verification 2015 Cham Springer 30-48
[34]
Gadyatskaya O, Hansen RR, Larsen KG, Legay A, Olesen MC, and Poulsen DB Fränzle M and Markey N Modelling attack-defense trees using timed automata Formal Modeling and Analysis of Timed Systems 2016 Cham Springer 35-50
[35]
Gilbert, D.R., Donaldson, R.: A monte Carlo model checker for probabilistic LTL with numerical constraints (2008)
[36]
Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11–20 (1982)
[37]
Hahn C, Stenger M, and Tentrup L Vojnar T and Zhang L Constraint-based monitoring of hyperproperties Tools and Algorithms for the Construction and Analysis of Systems 2019 Cham Springer 115-131
[38]
Henriques, D., Martins, J.G., Zuliani, P., Platzer, A., Clarke, E.M.: Statistical model checking for Markov decision processes. In: 2012 Ninth International Conference on Quantitative Evaluation of Systems, pp. 84–93 (2012).
[39]
Hsu, T., Bonakdarpour, B., Finkbeiner, B., Sánchez, C.: Bounded model checking for asynchronous hyperproperties. CoRR abs/2301.07208 (2023).
[40]
Hsu, T., Bonakdarpour, B., Sánchez, C.: HyperQube: a QBF-based bounded model checker for hyperproperties. CoRR abs/2109.12989 (2021). https://arxiv.org/abs/2109.12989
[41]
Hsu T-H, Sánchez C, and Bonakdarpour B Bounded model checking for hyperproperties Tools and Algorithms for the Construction and Analysis of Systems 2021 Cham Springer 94-112
[42]
Gray JW III and Syverson PF A logical approach to multilevel security of probabilistic systems Distrib. Comput. 1998 11 2 73-90
[43]
Katoen JP, Zapreev IS, Hahn EM, Hermanns H, and Jansen DN The ins and outs of the probabilistic model checker MRMC Perform. Eval. 2011 68 2 90-104
[44]
Kwiatkowska M, Norman G, and Parker D Gopalakrishnan G and Qadeer S PRISM 4.0: verification of probabilistic real-time systems Computer Aided Verification 2011 Heidelberg Springer 585-591
[45]
Larsen KG and Legay A Margaria T and Steffen B 30 years of statistical model checking Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles 2020 Cham Springer 325-330
[46]
Legay A, Delahaye B, Bensalem S, et al. Barringer H et al. Statistical model checking: an overview Runtime Verification 2010 Heidelberg Springer 122-135
[47]
Legay A, Lukina A, Traonouez LM, Yang J, Smolka SA, and Grosu R Steffen B and Woeginger G Statistical model checking Computing and Software Science 2019 Cham Springer 478-504
[48]
Legay, A., Sedwards, S.: On statistical model checking with PLASMA. In: The 8th International Symposium on Theoretical Aspects of Software Engineering (2014)
[49]
O’Neill, K.R., Clarkson, M.R., Chong, S.: Information-flow security for interactive programs. In: CSFW, pp. 190–201. IEEE Computer Society (2006)
[50]
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46–57. IEEE (1977)
[51]
Stucki S, Sánchez C, Schneider G, and Bonakdarpour B ter Beek MH, McIver A, and Oliveira JN Gray-box monitoring of hyperproperties Formal Methods – The Next 30 Years 2019 Cham Springer 406-424
[52]
Wald A Sequential tests of statistical hypotheses Ann. Math. Stat. 1945 16 2 117-186
[53]
Wang, Y., Nalluri, S., Bonakdarpour, B., Pajic, M.: Statistical model checking for hyperproperties. In: IEEE Computer Security Foundations Symposium, pp. 1–16. Dubrovnik, Croatia (2021)
[54]
Wang, Y., Nalluri, S., Pajic, M.: Hyperproperties for robotics: planning via HyperLTL. In: 2020 IEEE International Conference on Robotics and Automation (ICRA), pp. 8462–8468 (2020).
[55]
Wang Y, Zarei M, Bonakdarpour B, and Pajic M Statistical verification of hyperproperties for cyber-physical systems ACM Trans. Embed. Comput. Syst. 2019 18 5 92
[56]
Younes HLS Etessami K and Rajamani SK Ymer: a statistical model checker Computer Aided Verification 2005 Heidelberg Springer 429-433
[57]
Zdancewic, S., Myers, A.C.: 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, p. 29. IEEE Computer Society (2003).
[58]
Zuliani P Statistical model checking for biological applications Int. J. Softw. Tools Technol. Transfer 2015 17 527-536
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 ...
Software Verification of Hyperproperties Beyond k-Safety
Computer Aided VerificationAbstractTemporal hyperproperties are system properties that relate multiple execution traces. For (finite-state) hardware, temporal hyperproperties are supported by model checking algorithms, and tools for general temporal logics like HyperLTL exist. For (...
On the limits of refinement-testing for model-checking CSP
AbstractRefinement-checking, as embodied in tools like FDR, PAT and ProB, is a popular approach for model-checking refinement-closed predicates of CSP processes. We consider the limits of this approach to model-checking these kinds of predicates. By ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2023.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 24 October 2023
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 18 Dec 2024