Document Open Access Logo

Reasoning About Quality in Hyperproperties

Authors Samuel Graepler, Benjamin Monmege , Jean-Marc Talbot

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.45.pdf
  • Filesize: 0.81 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Security and privacy
Keywords
  • Hyperlogics
  • Automata-based model checking
  • Quantitative verification

Metrics

Abstract

Hyperproperties allow one to specify properties of systems that inherently involve not single executions of the system, but several of them at once: observational determinism and non-inference are two examples of such properties used to study the security of systems. Logics like HyperLTL have been studied in the past to model check hyperproperties of systems. However, most of the time, requiring strict security properties is actually ineffective as systems do not meet such requirements. To overcome this issue, we introduce qualitative reasoning in HyperLTL, inspired by a similar work on LTL by Almagor, Boker and Kupferman [Almagor et al., 2016] where a formula has a value in the interval [0, 1], obtained by considering either a propositional quality (how much the specification is satisfied), or a temporal quality (when the specification is satisfied). We show decidability of the approximated model checking problem, as well as the model checking of large fragments.

Cite As Get BibTex

Samuel Graepler, Benjamin Monmege, and Jean-Marc Talbot. Reasoning About Quality in Hyperproperties. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 45:1-45:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.45

Author Details

Samuel Graepler
  • Fakultät für Mathematik und Informatik, Universität Leipzig, Germany
Benjamin Monmege
  • Aix Marseille Univ, CNRS, LIS, Marseille, France
Jean-Marc Talbot
  • Aix Marseille Univ, CNRS, LIS, Marseille, France
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400 Talence, France

Funding

This work was partially done while the first author was an intern at Aix-Marseille Université. This work was partly supported by ANR-23-PECL-0009 TRUSTINCloudS.

Acknowledgements

We thank the reviewers of the different versions of this article for their valuable feedback.

References

  1. Erika Ábrahám and Borzoo Bonakdarpour. HyperPCTL: A temporal logic for probabilistic hyperproperties. In Quantitative Evaluation of Systems. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99154-2_2.
  2. Shaull Almagor, Udi Boker, and Orna Kupferman. Formally reasoning about quality. Journal of the ACM, 63(3):1-56, 2016. URL: https://doi.org/10.1145/2875421.
  3. Benedikt Bollig, Paul Gastin, Benjamin Monmege, and Marc Zeitoun. Pebble weighted automata and weighted logics. ACM Trans. Comput. Log., 15(2):15:1-15:35, 2014. URL: https://doi.org/10.1145/2579819.
  4. Marco Chiesa, Guy Kindler, and Michael Schapira. Traffic engineering with equal-cost-multipath: An algorithmic perspective. IEEE/ACM Transactions on Networking, 25(2):779-792, 2017. URL: https://doi.org/10.1109/TNET.2016.2614247.
  5. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer Cham, 2020. URL: https://doi.org/10.1007/978-3-319-10575-8.
  6. M. R. Clarkson, Bernd Finkbeiner, M. Koleini, K. K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In POST 2014, volume 8414 of LNCS, pages 265-284. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_15.
  7. M. R. Clarkson and F. Schneider. Hyperproperties. Journal of Computer Security, 18:1157-1210, 2010. URL: https://doi.org/10.1109/CSF.2008.7.
  8. Manfred Droste and Paul Gastin. Weighted automata and weighted logics. Theor. Comput. Sci., 380(1-2):69-86, 2007. URL: https://doi.org/10.1016/J.TCS.2007.02.055.
  9. Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. From Spot 2.0 to Spot 2.10: What’s new? In CAV 2022, volume 13372 of LNCS, pages 174-187. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13188-2_9.
  10. Marco Faella, Axel Legay, and Mariëlle Stoelinga. Model checking quantitative linear time logic. Electronic Notes in Theoretical Computer Science, 220:61-77, 2008. URL: https://doi.org/10.1016/j.entcs.2008.11.019.
  11. Angelo Ferrando, Giulia Luongo, Vadim Malvone, and Aniello Murano. Theory and practice of quantitative ATL. In PRIMA 2024: Principles and Practice of Multi-Agent Systems, volume 15395 of LNCS. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-77367-9_18.
  12. Bernd Finkbeiner and Christopher Hahn. Deciding hyperproperties. In CONCUR 2016, volume 59 of LIPIcs, pages 13:1-13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.13.
  13. Bernd Finkbeiner, Christopher Hahn, and Hazem Torfah. Model checking quantitative hyperproperties. In CAV 2018, volume 10981 of LNCS. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96145-3_8.
  14. Bernd Finkbeiner and Martin Zimmermann. The first-order logic of hyperproperties. In 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017, March 8-11, 2017, Hannover, Germany, volume 66 of LIPIcs, pages 30:1-30:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.30.
  15. R. Focardi and R. Gorrieri. Classification of security properties (part I: Information flow). In FOSAD 2000, volume 2171 of LNCS, pages 331-396. Springer, 2000. URL: https://doi.org/10.1007/3-540-45608-2_6.
  16. Rob Gerth, Doron Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In PSTV 1995, pages 3-15. Springer, 1995. URL: https://doi.org/10.1007/978-0-387-34892-6_1.
  17. Joseph A. Goguen and José Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, pages 11-20. IEEE, 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  18. Samuel Graepler, Benjamin Monmege, and Jean-Marc Talbot. Reasoning about quality in hyperproperties. Technical Report 2512.00500, arXiv, 2025. URL: https://doi.org/10.48550/arXiv.2512.00500.
  19. Gerard J. Holzmann. The model checker SPIN. IEEE Trans. Software Eng., 23(5):279-295, 1997. URL: https://doi.org/10.1109/32.588521.
  20. John McLean. A general theory of composition for trace sets closed under selective interleaving functions. In Symposium on Research in Security and Privacy, pages 79-93. IEEE Computer Society, 1994. URL: https://doi.org/10.1109/RISP.1994.296590.
  21. C. E. Shannon. The synthesis of two terminal switching circuits. The Bell System Technical Journal, 28(1):59-98, 1949. URL: https://doi.org/10.1002/j.1538-7305.1949.tb03624.x.
  22. A. P. Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logic. Journal of the ACM, 32:733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  23. G. Smith. On the foundations of quantitative information flow. In FoSSaCS 2009, volume 5504 of LNCS. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00596-1_21.
  24. Tachio Terauchi and Alex Aiken. Secure information flow as a safety problem. In Chris Hankin and Igor Siveroni, editors, Static Analysis, pages 352-367, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11547662_24.
  25. Hirotoshi Yasuoka and Tachio Terauchi. Quantitative information flow as safety and liveness hyperproperties. Theoretical Computer Science, 538:167-182, 2014. URL: https://doi.org/10.1016/J.TCS.2013.07.031.
  26. A. Zakinthinos and E.S. Lee. A general theory of security properties. In Proceedings. 1997 IEEE Symposium on Security and Privacy (Cat. No.97CB36097), pages 94-102, 1997. URL: https://doi.org/10.1109/SECPRI.1997.601322.
  27. Steve Zdancewic and Andrew C. Myers. Observational determinism for concurrent program security. In CSFW 2003. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/CSFW.2003.1212703.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact