Privacy-Preserving Runtime Verification

TL;DR

This paper introduces two cryptographic protocols enabling privacy-preserving runtime verification, allowing third-party monitoring of systems against formal specifications without revealing sensitive system data or the specifications themselves.

Contribution

The work presents novel protocols that adapt cryptographic multi-party computation techniques for privacy-preserving runtime verification, minimizing communication overhead and ensuring data confidentiality.

Findings

Protocols verify system compliance without revealing sensitive data.

Implementation for register automata demonstrates practical feasibility.

Single-message exchange per observation step reduces communication overhead.

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.