RVHyper – A Runtime Verification Tool for Temporal Hyperproperties
Copyright © 2017 Marvin Stenger, Saarland University
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.
The source code is available at GitHub: RVHyper.
Monitoring Hyperproperties.Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup.
17th International Conference on Runtime Verification (RV 2017).
If you have questions or problems, please do not hesitate to contact Marvin Stenger.