Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption

TL;DR

This paper presents a protocol for privacy-preserving online monitoring of cyber-physical systems using fully homomorphic encryption, enabling secure computation of STL-based safety assessments on encrypted data.

Contribution

It extends previous work by combining two FHE schemes to perform arithmetic and logical operations for STL monitoring on encrypted signals.

Findings

Successful case studies on blood glucose monitoring

Effective vehicle behavior analysis against safety rules

Demonstrated practical feasibility of the protocol

Abstract

When monitoring a cyber-physical system (CPS) from a remote server, keeping the monitored data secret is crucial, particularly when they contain sensitive information, e.g., biological or location data. Recently, Banno et al. (CAV'22) proposed a protocol for online LTL monitoring that keeps data concealed from the server using Fully Homomorphic Encryption (FHE). We build on this protocol to allow arithmetic operations over encrypted values, e.g., to compute a safety measurement combining distance, velocity, and so forth. Overall, our protocol enables oblivious online monitoring of discrete-time real-valued signals against signal temporal logic (STL) formulas. Our protocol combines two FHE schemes, CKKS and TFHE, leveraging their respective strengths. We employ CKKS to evaluate arithmetic predicates in STL formulas while utilizing TFHE to process them using a DFA derived from the STL formula. We conducted case studies on monitoring blood glucose levels and vehicles' behavior against the Responsibility-Sensitive Safety (RSS) rules. Our results suggest the practical relevance of our protocol.