Privacy-Preserving Runtime Verification

TL;DR

This paper tackles privacy concerns in runtime verification by enabling third-party monitoring of system traces against formal sequential specifications without exposing sensitive data. It introduces two protocols: an Open Specification protocol where the spec is public and the monitor learns only a per-round flag, and a Hidden Specification protocol where the spec remains private and the monitor still learns only whether the spec is satisfied; both achieve a single message per observation after an initial setup by encoding the specification as a circuit computing a next-state function and a flag. The core methods combine garbled circuits for open-spec and private function evaluation in a reactive setting (with DDH-based labeling and OT for hidden-spec), and the work provides formal correctness and semi-honest security proofs, along with experimental evaluation on register-automata specifications showing feasibility for circuits on the order of $10^5$ gates. The results demonstrate that privacy-preserving third-party monitoring can be practical with lightweight per-round communication and scalable cryptographic techniques, potentially enabling trustworthy audits in domains like finance and healthcare while protecting proprietary data and specifications.

Abstract

Runtime verification offers scalable solutions to improve the safety and reliability of systems. However, systems that require verification or monitoring by a third party to ensure compliance with a specification might contain sensitive information, causing privacy concerns when usual runtime verification approaches are used. Privacy is compromised if protected information about the system, or sensitive data that is processed by the system, is revealed. In addition, revealing the specification being monitored may undermine the essence of third-party verification. In this work, we propose two novel protocols for the privacy-preserving runtime verification of systems against formal sequential specifications. In our first protocol, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. Our second protocol ensures that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocols adapt and improve existing techniques used in cryptography, and more specifically, multi-party computation. The sequential specification defines the observation step of the monitor, whose granularity depends on the situation (e.g., banks may be monitored on a daily basis). Our protocols exchange a single message per observation step, after an initialisation phase. This design minimises communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.

Figures (12)

• Figure 1: The architecture of a system and a safety monitor with a privacy-preserving protocol: $(\pi_\textsf{Sys},\pi_\textsf{Mon})$
• Figure 2: Ideal setting with a trusted third party for monitoring where the specification is not a secret and circuit $\mathcal{C}$ is known to all.
• Figure 3: Ideal setting with a trusted third party for monitoring where the specification is a secret.
• Figure 4: Base labels: feed-out wires.
• Figure 5: Base labels: feed-in wires

Theorems & Definitions (13)

• definition thmcounterdefinition: Correctness of monitoring protocols with semi-honest parties
• definition thmcounterdefinition: Secure monitoring with semi-honest parties
• theorem thmcountertheorem
• theorem thmcountertheorem
• lemma thmcounterlemma: NR04
• theorem thmcountertheorem
• lemma thmcounterlemma: LP09
• theorem thmcountertheorem
• lemma thmcounterlemma: NR04
• lemma thmcounterlemma