Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption

Masaki Waga, Kotaro Matsuoka, Takashi Suwa, Naoki Matsumoto, Ryotaro Banno, Song Bian, Kohei Suenaga

TL;DR

This protocol enables oblivious online monitoring of discrete-time real-valued signals against signal temporal logic (STL) formulas against signal temporal logic (STL) formulas by combining two FHE schemes, CKKS and TFHE, leveraging their respective strengths.

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.

Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption

TL;DR

This protocol enables oblivious online monitoring of discrete-time real-valued signals against signal temporal logic (STL) formulas against signal temporal logic (STL) formulas by combining two FHE schemes, CKKS and TFHE, leveraging their respective strengths.

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.
Paper Structure (39 sections, 2 theorems, 5 equations, 3 figures, 17 tables, 3 algorithms)

This paper contains 39 sections, 2 theorems, 5 equations, 3 figures, 17 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Monitoring of CPS with confidential information
  3. Oblivious online LTL monitoring
  4. Contribution: Oblivious online monitoring of STL formulas with arithmetic operations
  5. Scheme switching optimized with value range information
  6. Related work
  7. Organization of the paper
  8. Preliminaries
  9. Discrete-time signal temporal logic
  10. Fully Homomorphic Encryption
  11. Online algorithm for oblivious DFA execution
  12. Oblivious online discrete-time STL monitoring
  13. Overview of our oblivious online STL monitoring algorithm
  14. Scheme switching optimized with value range information
  15. Correctness and complexity of our algorithm
  16. ...and 24 more sections

Key Result

Lemma 1.5

Given an RLWE ciphertext $\overline{\mathbf{\mathbf{c}}}_{q_{\mathrm{CKKS}}}$, its scaling factor $\mathit{scale}$, $\mathit{maxDiff} \in {\mathbb{R}_{>0}}$, the switching size $k \in {\mathbb{N}_{>0}}$, and the modulus $q_{\mathrm{CKKS}}$ and $q_{\mathrm{TFHE}}$ of the quotient ring used in the inp

Figures (3)

  • Figure 1: Our leading example: a driver-assistance system with remote monitoring.
  • Figure 2: Our oblivious online STL monitoring protocol combining two FHE schemes:the CKKS and TFHE schemes. The DFA is constructed from the STL formula representing the monitored specification beforehand.
  • Figure 3: The auxiliary predicates and formulas in RSS. The constants are shown in \ref{['section:detail_rss_formula']}.

Theorems & Definitions (8)

  • Example 1.1: remote vehicle monitoring
  • Example 1.2
  • Example 1.3
  • Definition 1.4: signal temporal logic
  • Lemma 1.5: correctness of \ref{['algorithm:protocol:ckks_to_tfhe']}
  • Theorem 1.6: correctness
  • proof : sketch
  • Definition 7: signal temporal logic