Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption

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 dat...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2024-10
Main Authors: Waga, Masaki, Matsuoka, Kotaro, Suwa, Takashi, Matsumoto, Naoki, Banno, Ryotaro, Bian, Song, Suenaga, Kohei
Format: Article
Language:English
Subjects:
Arithmetic
Cyber-physical systems
Discrete time systems
Encryption
Remote monitoring
Temporal logic
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422
DOI:10.48550/arxiv.2405.16767