RVHyper – A Runtime Verification Tool for Temporal Hyperproperties

Copyright © 2017 Marvin Stenger, 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

RVHyper

The source code is available at GitHub: RVHyper.

Related Publications

RVHyper: A Runtime Verification Tool for Temporal Hyperproperties.

Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup.
24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018).
Tool.
Poster.

Monitoring Hyperproperties.

Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup.
17th International Conference on Runtime Verification (RV 2017).

Contact

If you have questions or problems, please do not hesitate to contact Marvin Stenger.