Efficient monitoring of hyperproperties using prefix trees
- PDF / 630,951 Bytes
- 12 Pages / 595.276 x 790.866 pts Page_size
- 66 Downloads / 192 Views
STTT Special Issue: TACAS 2018
Efficient monitoring of hyperproperties using prefix trees Bernd Finkbeiner1 · Christopher Hahn1 · Marvin Stenger1 · Leander Tentrup1
© The Author(s) 2020
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 counterexample, 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. Keywords Runtime verification · Monitoring · Hyperproperties
1 Introduction Hyperproperties [10] are widely studied in (but not limited to) the context of secure information flow control. They generalize trace properties in that they not only check the correctness of individual computation traces in isolation, but relate multiple computation traces to each other. ExamThis work was partially supported by the German Research Foundation (DFG) as part of the Collaborative Research Center “Methods and Tools for Understanding and Controlling Privacy” (CRC 1223) and the Collaborative Research Center “Foundations of Perspicuous Software Systems” (TRR 248, 389792660), and by the European Research Council (ERC) Grant OSARES (No. 683300).
B
Christopher Hahn [email protected] Bernd Finkbeiner [email protected] Marvin Stenger [email protected] Leander Tentrup [email protected]
1
Reactive Systems Group, Saarland University, Saarbrücken, Germany
ples include information flow policies, such as observational determinism [33,34,42], (quantitative) non-interference [33, 36,41] as well as symmetry [26] and spurious dependencies in hardware designs [23], error correcting codes [26], and anti-doping of automotive software [14]. In this article, we present the monitoring approach implemented in the latest version of RVHyper, an automata-based monitoring tool for hyperproperties [24]. In dynamic verification of hyperproperties, efficient and light-weight monitoring techniques are instrumented in systems, which are usually far beyond the
Data Loading...
