LIPIcs.CONCUR.2023.21.pdf
- Filesize: 0.75 MB
- 16 pages
Document
Hypernode Automata
Authors
Ezio Bartocci 
,
Thomas A. Henzinger ,
Dejan Nickovic ,
Ana Oliveira da Costa
-
Part of:
Volume:
34th International Conference on Concurrency Theory (CONCUR 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-09-07
File
Document Identifiers
Author Details
Cite As Get BibTex
Ezio Bartocci, Thomas A. Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. Hypernode Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.21
Abstract
We introduce hypernode automata as a new specification formalism for hyperproperties of concurrent systems. They are finite automata with nodes labeled with hypernode logic formulas and transitions labeled with actions. A hypernode logic formula specifies relations between sequences of variable values in different system executions. Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces by constraining the values and the order of value changes of each variable without correlating the timing of the changes. Different execution traces are synchronized solely through the transitions of hypernode automata. Hypernode automata naturally combine asynchronicity at the node level with synchronicity at the transition level. We show that the model-checking problem for hypernode automata is decidable over action-labeled Kripke structures, whose actions induce transitions of the specification automata. For this reason, hypernode automaton is a suitable formalism for specifying and verifying asynchronous hyperproperties, such as declassifying observational determinism in multi-threaded programs.
Subject Classification
ACM Subject Classification
- Security and privacy → Logic and verification
Keywords
- Hyperproperties
- Asynchronous
- Automata
- Logic
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. URL: https://doi.org/10.1145/585265.585270.
- Aslan Askarov and Andrei Sabelfeld. Gradual release: Unifying declassification, encryption and key release policies. In 2007 IEEE Symposium on Security and Privacy, pages 207-221, 2007. URL: https://doi.org/10.1109/SP.2007.22.
- Ezio Bartocci, Thomas Ferrère, Thomas A. Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. Flavors of sequential information flow. In Bernd Finkbeiner and Thomas Wies, editors, 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 13182 of LNCS, pages 1-19. Springer International Publishing, 2022. URL: https://doi.org/10.1007/978-3-030-94583-1_1.
- Ezio Bartocci, Thomas A. Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. Hypernode automata, 2023. URL: https://arxiv.org/abs/2305.02836.
- Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. A temporal logic for asynchronous hyperproperties. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification (CAV), pages 694-717. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-81685-8_33.
- Raven Beutner and Bernd Finkbeiner. A Temporal Logic for Strategic Hyperproperties. In 32nd International Conference on Concurrency Theory (CONCUR), volume 203 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.24.
- Borzoo Bonakdarpour and Sarai Sheinvald. Finite-word hyperlanguages. In Alberto Leporati, Carlos Martín-Vide, Dana Shapira, and Claudio Zandron, editors, Language and Automata Theory and Applications (LATA). Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-68195-1.
- Laura Bozzelli, Adriano Peron, and César Sánchez. Asynchronous extensions of HyperLTL. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470583.
- Laura Bozzelli, Adriano Peron, and César Sánchez. Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties. In Bartek Klin, Sławomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory (CONCUR), volume 243 of Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1-27:16, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.27.
- 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 POST 2014: the Third International Conference on Principles of Security and Trust, volume 8414 of Lecture Notes in Computer Science, pages 265-284. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8.
- Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
- Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang., 5(POPL), 2021. URL: https://doi.org/10.1145/3434319.
- M. Huisman, P. Worah, and K. Sunesen. A temporal logic characterisation of observational determinism. In 19th IEEE Computer Security Foundations Workshop (CSFW), pages 13 pp.-3, 2006. URL: https://doi.org/10.1109/CSFW.2006.6.
- Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann. Team Semantics for the Specification and Verification of Hyperproperties. In Igor Potapov, Paul Spirakis, and James Worrell, editors, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018), volume 117 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1-10:16. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.MFCS.2018.10.
-
Andrei Sabelfeld and David Sands. Declassification: Dimensions and principles. Journal of Computer Security, 17(5):517-548, 2009.
- Tachio Terauchi. A type system for observational determinism. In 2008 21st IEEE Computer Security Foundations Symposium, pages 287-300, 2008. URL: https://doi.org/10.1109/CSF.2008.9.
- S. Zdancewic and A.C. Myers. Observational determinism for concurrent program security. In 16th IEEE Computer Security Foundations Workshop, 2003. Proceedings., pages 29-43, 2003. URL: https://doi.org/10.1109/CSFW.2003.1212703.