Concurrent Hyperproperties

TL;DR

This paper introduces concurrent hyperproperties, extending hyperproperties to concurrent traces modeled by Petri nets, enabling analysis of systems with nondeterministic and concurrent behaviors, especially in security contexts.

Contribution

It generalizes hyperproperties to concurrent traces using Petri nets and formalizes testing methods for concurrent hyperproperties.

Findings

Defines concurrent hyperproperties using Petri nets.

Formalizes may and must testing for concurrent traces.

Distinguishes nondeterministic and concurrent behaviors.

Abstract

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.