RVHyper – A Runtime Verification Tool for Temporal Hyperproperties

Copyright © 2017-2019 Marvin Stenger, Christopher Hahn, Leander Tentrup, Saarland University

Introduction

Hyperproperties generalize properties of individual computation traces in that they relate such traces to each other. This is needed to express information flow security policies, such as observational determinism: A systems behavior should appear to be deterministic to an external observer, i.e., there should be no information leakage of certain secrets into the public domain.

HyperLTL, which extends Linear-time Temporal Logic (LTL) with explicit trace quantification, is a recently introduced temporal logic capable of formalizing many hyperproperties of interest. However, formalizing hyperproperties in HyperLTL can be error-prone, since we have to consider multiple traces at the same time.

RVHyper is a runtime verification tool for HyperLTL. Given a specification and a set of traces, RVHyper determines whether the specification is satisfied on those traces and, in case of violation, outputs a counterexample consisting of a subset of the input traces.

Poster

(See our publications at RV 2017 and TACAS 2018)

Furthermore, in a new monitoring approach, we focus on requirements that new incoming traces pose on future traces by rewriting a hyperproperty in the temporal logic HyperLTL to a Boolean constraint system. A hyperproperty is then violated by multiple runs of the system if the constraint system becomes unsatisfiable. Our implementation either utilizes BDDs or a SAT solver to store and evaluate constraints.

Poster

(See our publication at TACAS 2019)

RVHyper

The source code is available at GitHub: RVHyper.
The artifact for our constraint-based monitoring approach is available at: Artifact

Related Publications