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

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.