Centralized vs Decentralized Monitors for Hyperproperties

TL;DR

This paper compares centralized and decentralized runtime monitors for hyperproperties expressed in Hyper-recHML, providing synthesis procedures and correctness proofs, including bisimulation results, to enhance distributed system verification.

Contribution

It introduces a formal framework for both centralized and decentralized monitors for hyperproperties, with synthesis procedures and correctness proofs, including bisimulation equivalence.

Findings

Centralized and decentralized monitors are shown to be weakly bisimilar.

A synthesis procedure for correct monitors is provided for both settings.

Decentralized monitors communicate to produce a unique verdict.

Abstract

This paper focuses on the runtime verification of hyperproperties expressed in Hyper-recHML, an expressive yet simple logic for describing properties of sets of traces. To this end, we consider a simple language of monitors that observe sets of system executions and report verdicts w.r.t. a given Hyper-recHML formula. We first employ a unique omniscient monitor that centrally observes all system traces. Since centralised monitors are not ideal for distributed settings, we also provide a language for decentralized monitors, where each trace has a dedicated monitor; these monitors yield a unique verdict by communicating their observations to one another. For both the centralized and the decentralized settings, we provide a synthesis procedure that, given a formula, yields a monitor that is correct (i.e., sound and violation complete). A key step in proving the correctness of the synthesis for decentralized monitors is a result showing that, for each formula, the synthesized centralized monitor and its corresponding decentralized one are weakly bisimilar for a suitable notion of weak bisimulation.