Efficient Monitoring of Hyperproperties using Prefix Trees

TL;DR

This paper introduces RVHyper, a runtime verification tool that efficiently monitors hyperproperties specified in HyperLTL by using prefix trees to optimize trace storage and detection of violations.

Contribution

The paper presents a novel trace storage technique using prefix trees for monitoring hyperproperties, improving efficiency in runtime verification.

Findings

Effective detection of hyperproperty violations in benchmarks

Trace minimization reduces memory usage during monitoring

Application to hardware design analysis demonstrates versatility

Abstract

Hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other and are thus not monitorable by tools that consider computations in isolation. We present the monitoring approach implemented in the latest version of RVHyper, a runtime verification tool for hyperproperties. The input to the tool are specifications given in the temporal logic HyperLTL, which extends linear-time temporal logic (LTL) with trace quantifiers and trace variables. RVHyper processes execution traces sequentially until a violation of the specification is detected. In this case, a counter example, in the form of a set of traces, is returned. RVHyper employs a range of optimizations: a preprocessing analysis of the specification and a procedure that minimizes the traces that need to be stored during the monitoring process. In this article, we introduce a novel trace storage technique that arranges the traces in a tree-like structure to exploit partially equal traces. We evaluate RVhyper on existing benchmarks on secure information-flow control, error correcting codes and symmetry in hardware designs. As an example application outside of security, we show how RVHyper can be used to detect spurious dependencies in hardware designs.