RVHyper – A Runtime Verification Tool for Temporal Hyperproperties
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.
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.
(See our publication at TACAS 2019)
Constraint-based Monitoring of HyperpropertiesWith Marvin Stenger and Leander Tentrup.
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019).
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.