Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption

TL;DR

This paper presents a privacy-preserving protocol for online safety property monitoring in IoT using fully homomorphic encryption, enabling secure, real-time analysis without revealing sensitive data or proprietary specifications.

Contribution

It introduces a novel fully homomorphic encryption-based method for oblivious online monitoring of safety LTL specifications, with two efficient algorithms and proven security.

Findings

Protocols are correct and secure.

Algorithms are scalable both theoretically and empirically.

Practical application demonstrated in blood glucose monitoring.

Abstract

In many Internet of Things (IoT) applications, data sensed by an IoT device are continuously sent to the server and monitored against a specification. Since the data often contain sensitive information, and the monitored specification is usually proprietary, both must be kept private from the other end. We propose a protocol to conduct oblivious online monitoring -- online monitoring conducted without revealing the private information of each party to the other -- against a safety LTL specification. In our protocol, we first convert a safety LTL formula into a DFA and conduct online monitoring with the DFA. Based on fully homomorphic encryption (FHE), we propose two online algorithms (Reverse and Block) to run a DFA obliviously. We prove the correctness and security of our entire protocol. We also show the scalability of our algorithms theoretically and empirically. Our case study shows that our algorithms are fast enough to monitor blood glucose levels online, demonstrating our protocol's practical relevance.