Centralized vs Decentralized Monitors for Hyperproperties
Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Daniele Gorla, Jana Wagemaker
TL;DR
The paper tackles runtime verification of hyperproperties by introducing both centralized and decentralized monitors for Hyper-$\mathsf{rec}$HML. It develops a syntax-driven synthesis framework that yields sound and violation-complete monitors in the centralized setting for formulas without least fixed points and extends this to a decentralized choreography of communicating monitors for a expressive but constrained fragment, PHyper-$\mathsf{rec}$HML. A key technical contribution is establishing a weak bisimulation between centralized and decentralized monitors to transfer correctness, despite the added complexity of inter-monitor communication. The results advance scalable verification of hyperproperties in distributed systems, offering principled methods to synthesize robust monitoring architectures and paving the way for practical tooling and extended logic fragments.
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.