Trace properties, which are sets of execution traces, are often used to analyze systems, but their expressiveness is limited. Clarkson and Schneider defined hyperproperties as a generalization of trace properties to sets of sets of traces. Typical applications of hyperproperties are found in information flow security. We introduce an analogous definition of concurrent hyperproperties, by generalizing traces to concurrent traces, which we define as partially ordered multisets. We take Petri nets as the basic semantic model. Concurrent traces are formalized via causal nets. To check concurrent hyperproperties, we define may and must testing of sets of concurrent traces in the style of DeNicola and Hennessy, using the parallel composition of Petri nets. In our approach, we thus distinguish nondeterministic and concurrent behavior. We discuss examples where concurrent hyperproperties are needed.
History
Editor
Bowen JP ; Li Q ; Xu Q
Primary Research Area
Reliable Security Guarantees
Volume
14080
Book Title
Theories of Programming and Formal Methods
Page Range
211-231
Series
Lecture Notes in Computer Science
Publisher
Springer Nature
Open Access Type
Hybrid
BibTeX
@inbook{Finkbeiner:Olderog:2023,
title = "Concurrent Hyperproperties",
author = "Finkbeiner, Bernd" AND "Olderog, Ernst-Rüdiger",
editor = "Bowen, Jonathan P" AND "Li, Qin" AND "Xu, Qiwen",
year = 2023,
month = 9,
booktitle = "Theories of Programming and Formal Methods",
series = "Lecture Notes in Computer Science",
pages = "211--231",
publisher = "Springer Nature",
doi = "10.1007/978-3-031-40436-8_8"
}