Monitoring in the Dark: Privacy-Preserving Runtime Verification of Cyber-Physical Systems

TL;DR

The paper tackles privacy-preserving runtime verification for cyber-physical systems by ensuring that either the monitored trace or the formal specification remains secret while computing the robustness value $ ho(x,\phi,0)$ for STL-formulated properties. It introduces a garbled-circuits-based protocol and a DP-TALIRO-derived RTL circuit to perform robustness calculations on timed state sequences, with security grounded in the Real-Ideal paradigm and semi-honest adversaries. An end-to-end implementation is presented in Verilog and integrated with TinyGarble, and the authors empirically evaluate runtime, memory, and circuit size across multiple trace lengths and formula depths, highlighting exponential software runtimes, linear RAM growth, and meaningful hardware acceleration potential. The work demonstrates that privacy-preserving CPS monitoring and testing are feasible within certain scale bounds (e.g., design testing, offline monitoring) and discusses practical implications for Testing-as-a-Service markets and IP/privacy protections, while acknowledging substantial synthesis and scalability challenges for larger traces and deeper formulas. Overall, the approach offers a concrete path toward secure, privacy-aware runtime verification in CPS, with clear trade-offs between software practicality and hardware-enabled performance.

Abstract

In distributed Cyber-Physical Systems and Internet-of-Things applications, the nodes of the system send measurements to a monitor that checks whether these measurements satisfy given formal specifications. For instance in Urban Air Mobility, a local traffic authority will be monitoring drone traffic to evaluate its flow and detect emerging problematic patterns. Certain applications require both the specification and the measurements to be private -- i.e. known only to their owners. Examples include traffic monitoring, testing of integrated circuit designs, and medical monitoring by wearable or implanted devices. In this paper we propose a protocol that enables privacy-preserving robustness monitoring. By following our protocol, both system (e.g. drone) and monitor (e.g. traffic authority) only learn the robustness of the measured trace w.r.t. the specification. But the system learns nothing about the formula, and the monitor learns nothing about the signal monitored. We do this using garbled circuits, for specifications in Signal Temporal Logic interpreted over timed state sequences. We analyze the runtime and memory overhead of privacy preservation, the size of the circuits, and their practicality for three different usage scenarios: design testing, offline monitoring, and online monitoring of Cyber-Physical Systems.

Figures (9)

• Figure 1: CPS monitoring-and-testing loop. This paper introduces a way to do the monitoring in a privacy-preserving manner.
• Figure 2: Privacy-preserving monitoring using secure multi-party computation (MPC). Designer inputs the monitored trace, Verifier enters the formula. Both learn only the robustness $\rho(x,\phi,0)$.
• Figure 3: Finite state machine of the controller. Temporal blocks are labeled with conditions on their intervals (e.g. $U\_ZERO\_UNB$ corresponds to $\mathcal{U}_{[0,\infty)}$ and $F\_I\_EQ\_N$ for Eventually when the current table index equals signal size $N$).
• Figure 4: Movement of data between the Datapath, Controller, and Bounds modules. The Datapath handles input and output for the entire algorithm, taking in formula data and the signal and returning the robustness. Variables being passed to and from the Controller inform the Datapath on which calculations to perform next, and variables from the Bounds module provide information on which parts of the signal to consider in its calculations, given a subformula and starting point of the signal. Clock and reset variables are not included in this figure.
• Figure 5: Monitoring runtime vs trace length. For each length, we tried multiple formulas of depths 3 and 4. The curves show the best fit.