Monitoring Hyperproperties over Observed and Constructed Traces

TL;DR

This paper introduces a novel runtime monitoring approach for hyperproperties, allowing the construction of unobserved traces via generator functions, enabling the verification of complex asynchronous hyperproperties in concurrency and security.

Contribution

It extends hypernode logic with trace quantifiers over generator functions and provides a monitoring algorithm capable of handling infinite domains and asynchronous hyperproperties.

Findings

Implemented and evaluated the monitoring algorithm on various hyperproperties.

First method to enable monitoring of asynchronous hyperproperties with alternating trace quantifiers.

Demonstrated effectiveness in concurrency and security applications.

Abstract

We study the problem of monitoring at runtime whether a system fulfills a specification defined by a hyperproperty, such as linearizability or variants of non-interference. For this purpose, we introduce specifications with both passive and active quantification over traces. While passive trace quantifiers range over the traces that are observed, active trace quantifiers are instantiated with \emph{generator functions}, which are part of the specification. Generator functions enable the monitor to construct traces that may never be observed at runtime, such as the linearizations of a concurrent trace. As specification language, we extend hypernode logic with trace quantifiers over generator functions and interpret these hypernode formulas over possibly infinite domains. We present a corresponding monitoring algorithm, which we implemented and evaluated on a range of hyperproperties for concurrency and security applications. Our method enables, for the first time, the monitoring of asynchronous hyperproperties that contain alternating trace quantifiers.