Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Oblivious Online Monitoring for Safety LTL Spec...

Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption

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.

Our paper was accepted in CAV'22 ( http://i-cav.org/2022/ ). These slides were used in the presentation.

Paper (arXiv): https://arxiv.org/abs/2206.03582
GitHub: https://github.com/virtualsecureplatform/homfa

Ushitora Anqou

August 15, 2022
Tweet

More Decks by Ushitora Anqou

Other Decks in Technology

Transcript

  1. (Banno, Kyoto U.) Oblivious Online Monitoring for Safety LTL Specification

    via Fully Homomorphic Encryption Ryotaro Banno*1, Kotaro Matsuoka*1, Naoki Matsumoto*1, Song Bian*2, Masaki Waga*1, and Kohei Suenaga*1 *1 Kyoto University *2 Beihang University August 8, 2022 34th International Conference on Computer Aided Verification (CAV’22) 1
  2. (Banno, Kyoto U.) Background & Motivation Real-time monitoring of sensitive

    data • e.g., Monitoring blood glucose levels and/or ECG by wearable devices Server Client Sensitive sensed data Monitoring result Online monitoring 2
  3. (Banno, Kyoto U.) Background & Motivation Real-time monitoring of sensitive

    data • e.g., Monitoring blood glucose levels and/or ECG by wearable devices Server Client Sensitive sensed data Monitoring result Online monitoring 3 The server may exploit the sensitive sensed data
  4. (Banno, Kyoto U.) Background & Motivation Real-time monitoring of sensitive

    data • e.g., Monitoring blood glucose levels and/or ECG by wearable devices Server Client Sensitive sensed data Monitoring result 4 Online monitoring
  5. (Banno, Kyoto U.) Background & Motivation Real-time monitoring of sensitive

    data • e.g., Monitoring blood glucose levels and/or ECG by wearable devices Server Client Sensitive sensed data Monitoring result 5 Online monitoring The client may steal proprietary monitoring specification
  6. (Banno, Kyoto U.) Requirements of Remote Monitoring Protocol 2-party protocol

    that maintains both parties’ privacy 6 Server Client Sensed data Monitoring result Online monitoring
  7. (Banno, Kyoto U.) Requirements of Remote Monitoring Protocol 2-party protocol

    that maintains both parties’ privacy The client’s privacy: • Private data • Private result 7 Server Client Sensed data Monitoring result Online monitoring
  8. (Banno, Kyoto U.) Requirements of Remote Monitoring Protocol 2-party protocol

    that maintains both parties’ privacy The client’s privacy: • Private data • Private result 8 Server Client Sensed data Monitoring result Online monitoring The server’s privacy: • Private spec.
  9. (Banno, Kyoto U.) Requirements of Remote Monitoring Protocol 2-party protocol

    that maintains both parties’ privacy The client’s privacy: • Private data • Private result 9 Server Client Sensed data Monitoring result Online monitoring The server’s privacy: • Private spec. w/o any decryption
  10. (Banno, Kyoto U.) Requirements of Remote Monitoring Protocol 2-party protocol

    that maintains both parties’ privacy The client’s privacy: • Private data • Private result 10 Server Client Sensed data Monitoring result Online monitoring The server’s privacy: • Private spec. How can we implement this protocol? w/o any decryption
  11. (Banno, Kyoto U.) Contribution: Oblivious Online Monitoring Use fully homomorphic

    encryption (FHE) The client’s privacy: • Private data • Private result 11 Server Client Sensed data Monitoring result Online monitoring w/o any decryption The server’s privacy: • Private spec. Encryption allowing computation without decryption
  12. (Banno, Kyoto U.) Contribution: Oblivious Online Monitoring Use fully homomorphic

    encryption (FHE) The client’s privacy: • Private data • Private result 12 Server Client Sensed data Monitoring result Online monitoring w/o any decryption The server’s privacy: • Private spec. (Safety) LTL Encryption allowing computation without decryption Run a monitor DFA w/o any decryption
  13. (Banno, Kyoto U.) Challenge: Online, Obliviously, and Fast No known

    techniques provide fast oblivious online monitoring • Oblivious offline algorithms are known (e.g., [Chillotti+, J. Crypto 2020]) ◦ None of them is online • Trivial online algorithm via universality of FHE is theoretically possible ◦ Too slow 13
  14. (Banno, Kyoto U.) Our Contribution • Two online algorithms to

    run a DFA obliviously using FHE ◦ Named Reverse and Block • A protocol for oblivious online LTL monitoring ◦ with proofs of correctness and security • Experimentally demonstrated scalability and practicality ◦ Monitoring of a blood glucose level in < 3ms/sample in the best case 14
  15. (Banno, Kyoto U.) Outline • Preparation ◦ Offline Monitoring v.s.

    Online Monitoring ◦ Fully Homomorphic Encryption ◦ Offline algorithm to run a DFA obliviously • Oblivious Online LTL Monitoring ◦ Algorithm Reverse ◦ Algorithm Block • Experiments ◦ Monitoring of blood glucose levels 15
  16. (Banno, Kyoto U.) Offline Monitoring v.s. Online Monitoring Offline monitoring:

    • Monitored data: given in advance • Output: only once, after all data processed Online monitoring: • Monitored data: given one by one • Output: multiple times in the process 16 batch of data result 1st part of data partial result 2nd part of data partial result Offline monitoring Online monitoring
  17. (Banno, Kyoto U.) Fully Homomorphic Encryption (FHE) 18 x x

    Encrypt Common Encryption (e.g., AES) FHE
  18. (Banno, Kyoto U.) Fully Homomorphic Encryption (FHE) 19 x x

    f(x) Normal computation (e.g., addition) Encrypt Common Encryption (e.g., AES) FHE f
  19. (Banno, Kyoto U.) Fully Homomorphic Encryption (FHE) 20 x x

    f(x) f(x) Normal computation (e.g., addition) Encrypt Common Encryption (e.g., AES) FHE f
  20. (Banno, Kyoto U.) Fully Homomorphic Encryption (FHE) 21 x x

    f(x) f(x) Normal computation (e.g., addition) Encrypt Common Encryption (e.g., AES) FHE f x x f(x) Normal computation (e.g., addition) Encrypt f
  21. (Banno, Kyoto U.) Fully Homomorphic Encryption (FHE) 22 x x

    f(x) f(x) Normal computation (e.g., addition) Encrypt Common Encryption (e.g., AES) FHE f x x f(x) f(x) Normal computation (e.g., addition) Encrypt Decrypt f Computation via FHE (w/o dec.) f
  22. (Banno, Kyoto U.) Fully Homomorphic Encryption (FHE) 23 x x

    f(x) f(x) Normal computation (e.g., addition) Encrypt Common Encryption (e.g., AES) FHE f x x f(x) f(x) Normal computation (e.g., addition) Encrypt Decrypt f Computation via FHE (w/o dec.) f • We can construct f from f automatically via universality of FHE, but such f is slow • We need dedicated and fast algorithms
  23. (Banno, Kyoto U.) Primitive FHE Operation for DFA Execution FHE

    supports many operations over ciphertexts • It achieves its universality by combining them One primitive operation: CMux • Many FHE operations are constructed on top of CMux We realize DFA execution mainly via CMux 24
  24. (Banno, Kyoto U.) CMux (Controlled MUltipleXer) Gate A homomorphic operation

    FHE provides • Input: Ciphertext d, c 1 , c 0 • Output: Ciphertext o Calculate the following without decryption: • Dec(o) = Dec(c 1 ) if Dec(d) = 1 • Dec(o) = Dec(c 0 ) if Dec(d) = 0 Chosen value is not revealed • c 1 ≠ o and c 0 ≠ o (in binary representation) 25
  25. (Banno, Kyoto U.) Offline Execution of DFA via FHE The

    idea : • Enumerate all transitions of the DFA M that may be taken with the input data to be monitored • Select the correct one by CMux gates 26 [Chillotti+, J. Crypto 2020]
  26. (Banno, Kyoto U.) Offline Execution of DFA via FHE The

    idea : • Enumerate all transitions of the DFA M that may be taken with the input data to be monitored • Select the correct one by CMux gates 27 [Chillotti+, J. Crypto 2020] Assume input s = σ 1 σ 2 σ 3 (n=3) DFA M
  27. (Banno, Kyoto U.) Offline Execution of DFA via FHE The

    idea : • Enumerate all transitions of the DFA M that may be taken with the input data to be monitored • Select the correct one by CMux gates 28 [Chillotti+, J. Crypto 2020] Assume input s = σ 1 σ 2 σ 3 (n=3) DFA M n is known in advance in the offline setting
  28. (Banno, Kyoto U.) 1. Enumerate all transitions at depth n=3

    Assume input s = σ 1 σ 2 σ 3 (n=3) 29 [Chillotti+, J. Crypto 2020] DFA M Offline Execution of DFA via FHE
  29. (Banno, Kyoto U.) Offline Execution of DFA via FHE 1.

    Enumerate all transitions at depth n=3 2. Select by CMux gates 30 [Chillotti+, J. Crypto 2020]
  30. (Banno, Kyoto U.) Offline Execution of DFA via FHE 1.

    Enumerate all transitions at depth n=3 2. Select by CMux gates 31 [Chillotti+, J. Crypto 2020] The monitored ciphertexts
  31. (Banno, Kyoto U.) Offline Execution of DFA via FHE 1.

    Enumerate all transitions at depth n=3 2. Select by CMux gates 32 [Chillotti+, J. Crypto 2020] The monitored ciphertexts Flags indicating • accepting state (1) • not-accepting state (0)
  32. (Banno, Kyoto U.) Offline Execution of DFA via FHE 1.

    Enumerate all transitions at depth n=3 2. Select by CMux gates 33 [Chillotti+, J. Crypto 2020] The monitored ciphertexts Flags indicating • accepting state (1) • not-accepting state (0) Result: δ(q 0 , σ 1 σ 2 σ 3 ) F (encrypted) ∈
  33. (Banno, Kyoto U.) Why is the Algorithm Offline? • It

    consumes all the data from back to front • We cannot start the algorithm before we obtain the last input 34 Outline figure of the algorithm offline
  34. (Banno, Kyoto U.) Outline • Preparation ◦ Offline Monitoring v.s.

    Online Monitoring ◦ Fully Homomorphic Encryption ◦ Offline algorithm to run a DFA obliviously • Oblivious Online LTL Monitoring ◦ Algorithm Reverse ◦ Algorithm Block • Experiments ◦ Monitoring of blood glucose levels 35
  35. (Banno, Kyoto U.) Proposed Online Algorithms • Algorithm Reverse: 1.

    Reverse the DFA to obtain MR 2. Apply the offline algorithm to MR • Algorithm Block: 1. Split the monitored ciphertexts into fixed-length blocks 2. Process each block sequentially with the modified offline alg. 36 [Contribution]
  36. (Banno, Kyoto U.) Proposed Online Algorithms • Algorithm Reverse: 1.

    Reverse the DFA to obtain MR 2. Apply the offline algorithm to MR • Algorithm Block: 1. Split the monitored ciphertexts into fixed-length blocks 2. Process each block sequentially with the modified offline alg. 37 [Contribution] • Essentially reverse M twice • Time complexity is O(2|M|) due to powerset construction
  37. (Banno, Kyoto U.) Proposed Online Algorithms • Algorithm Reverse: 1.

    Reverse the DFA to obtain MR 2. Apply the offline algorithm to MR • Algorithm Block: 1. Split the monitored ciphertexts into fixed-length blocks 2. Process each block sequentially with the modified offline alg. 38 [Contribution] • Essentially reverse M twice • Time complexity is O(2|M|) due to powerset construction This talk focuses on algorithm Block
  38. (Banno, Kyoto U.) Revisit the Offline Algorithm Observation: The offline

    algorithm can output the reached state (i.e., δ(q 0 , σ 1 σ 2 …σ n ) ) 39
  39. (Banno, Kyoto U.) Revisit the Offline Algorithm Observation: The offline

    algorithm can output the reached state (i.e., δ(q 0 , σ 1 σ 2 …σ n ) ) 40 Use states as inputs instead of flags
  40. (Banno, Kyoto U.) Revisit the Offline Algorithm Observation: The offline

    algorithm can output the reached state (i.e., δ(q 0 , σ 1 σ 2 …σ n ) ) 41 Use states as inputs instead of flags Result: δ(q 0 , σ 1 σ 2 σ 3 )
  41. (Banno, Kyoto U.) Algorithm Block 43 Monitored ciphertexts: 1. Split

    the monitored ciphertexts into blocks of size B (here B=3)
  42. (Banno, Kyoto U.) Algorithm Block 44 Monitored ciphertexts: 1. Split

    the monitored ciphertexts into blocks of size B (here B=3) 2. Apply the modified offline alg. • to obtain δ(q 0 , σ 1 σ 2 σ 3 )
  43. (Banno, Kyoto U.) Algorithm Block 45 Monitored ciphertexts: 1. Split

    the monitored ciphertexts into blocks of size B (here B=3) How can we handle the block #2? • We want δ(δ(q 0 , σ 1 σ 2 σ 3 ), σ 4 σ 5 σ 6 ) • But, we don’t know δ(q 0 , σ 1 σ 2 σ 3 ) because it’s encrypted 2. Apply the modified offline alg. • to obtain δ(q 0 , σ 1 σ 2 σ 3 )
  44. (Banno, Kyoto U.) Algorithm Block 46 Monitored ciphertexts: 2. Apply

    the modified offline alg. • to obtain δ(q 0 , σ 1 σ 2 σ 3 ) 1. Split the monitored ciphertexts into blocks of size B (here B=3) 3. Apply the modified offline alg. to every state q i • to obtain δ(q i , σ 4 σ 5 σ 6 )
  45. (Banno, Kyoto U.) Algorithm Block 47 Monitored ciphertexts: 2. Apply

    the modified offline alg. • to obtain δ(q 0 , σ 1 σ 2 σ 3 ) 1. Split the monitored ciphertexts into blocks of size B (here B=3) Candidates 3. Apply the modified offline alg. to every state q i • to obtain δ(q i , σ 4 σ 5 σ 6 )
  46. (Banno, Kyoto U.) Algorithm Block 48 Monitored ciphertexts: 2. Apply

    the modified offline alg. • to obtain δ(q 0 , σ 1 σ 2 σ 3 ) 1. Split the monitored ciphertexts into blocks of size B (here B=3) Candidates Selector 3. Apply the modified offline alg. to every state q i • to obtain δ(q i , σ 4 σ 5 σ 6 )
  47. (Banno, Kyoto U.) Algorithm Block 49 Monitored ciphertexts: 2. Apply

    the modified offline alg. • to obtain δ(q 0 , σ 1 σ 2 σ 3 ) 1. Split the monitored ciphertexts into blocks of size B (here B=3) Candidates Selector 3. Apply the modified offline alg. to every state q i • to obtain δ(q i , σ 4 σ 5 σ 6 ) 4. Select the correct current state • i.e, δ(δ(q 0 , σ 1 σ 2 σ 3 ), σ 4 σ 5 σ 6 ) = δ(q 0 , σ 1 σ 2 σ 3 σ 4 σ 5 σ 6 ) This “Big CMux” is essentially a tree of CMux gates Selector Candidates
  48. (Banno, Kyoto U.) Algorithm Block: Pros and Cons • Pros:

    # of CMux gates is linear to |M| as well as to n ◦ In contrast, it’s exponential to |M| in algorithm Reverse • Cons: “Big CMux” can be slow ◦ It contains a very slow operation (~ 1,000 times slower than CMux) ◦ Tolerate B bits of delay of monitoring results for better performance ▪ Large B Fewer “Big CMux” ⇒ 50
  49. (Banno, Kyoto U.) Outline • Preparation ◦ Offline Monitoring v.s.

    Online Monitoring ◦ Fully Homomorphic Encryption ◦ Offline algorithm to run a DFA obliviously • Oblivious Online LTL Monitoring ◦ Algorithm Reverse ◦ Algorithm Block • Experiments ◦ Monitoring of blood glucose levels 51
  50. (Banno, Kyoto U.) Monitoring of Blood Glucose Levels (BG) Monitor

    BG of simulated type 1 diabetes patients • Use 6 LTL formulae (ψ 1 , ψ 2 , ψ 4 , φ 1 , φ 4 , φ 5 ) ◦ Originally presented by [Cameron+, RV’15] and [Young+, IoTDI’18] ◦ Use discrete sampling to convert original STL formulae to LTL ones • Record BG every 1 minute • Encode each BG in 9 bits 52 Experimental environment: • CPU: Intel Xeon Silver 4216 (32C64T @ 3.2 GHz) • RAM: 128 GiB
  51. (Banno, Kyoto U.) Experimental Result 53 Formula |M| |MR| Mean

    Runtime (ms/value) Block Reverse ψ 1 10524 2712974 184.02 22220.62 ψ 2 11126 2885376 182.43 23626.97 ψ 4 7026 —*1 49.12 —*1 φ 1 21 20 172.72 2.21 φ 4 237 237 205.68 4.19 φ 5 390 390 206.78 5.44 *1: Construction of MR for ψ 4 was aborted due to memory limit
  52. (Banno, Kyoto U.) Experimental Result 54 Formula |M| |MR| Mean

    Runtime (ms/value) Block Reverse ψ 1 10524 2712974 184.02 22220.62 ψ 2 11126 2885376 182.43 23626.97 ψ 4 7026 —*1 49.12 —*1 φ 1 21 20 172.72 2.21 φ 4 237 237 205.68 4.19 φ 5 390 390 206.78 5.44 *1: Construction of MR for ψ 4 was aborted due to memory limit |MR| is large ⇨ Block is faster <
  53. (Banno, Kyoto U.) Experimental Result 55 Formula |M| |MR| Mean

    Runtime (ms/value) Block Reverse ψ 1 10524 2712974 184.02 22220.62 ψ 2 11126 2885376 182.43 23626.97 ψ 4 7026 —*1 49.12 —*1 φ 1 21 20 172.72 2.21 φ 4 237 237 205.68 4.19 φ 5 390 390 206.78 5.44 *1: Construction of MR for ψ 4 was aborted due to memory limit |MR| is large ⇨ Block is faster |MR| is small ⇨ Reverse is faster < >
  54. (Banno, Kyoto U.) Experimental Result 56 Formula |M| |MR| Mean

    Runtime (ms/value) Block Reverse ψ 1 10524 2712974 184.02 22220.62 ψ 2 11126 2885376 182.43 23626.97 ψ 4 7026 —*1 49.12 —*1 φ 1 21 20 172.72 2.21 φ 4 237 237 205.68 4.19 φ 5 390 390 206.78 5.44 *1: Construction of MR for ψ 4 was aborted due to memory limit Both algorithms took at most 24 sec./value ⇨ Faster than sampling interval (1 min.)
  55. (Banno, Kyoto U.) The client’s privacy: • Private data •

    Private result Server Client Sensed data Monitoring result Online monitoring The server’s privacy: • Private spec. w/o any decryption Conclusion 57
  56. (Banno, Kyoto U.) The client’s privacy: • Private data •

    Private result Server Client Sensed data Monitoring result Online monitoring The server’s privacy: • Private spec. w/o any decryption Conclusion 58 1. We proposed a protocol of oblivious online LTL monitoring
  57. (Banno, Kyoto U.) The client’s privacy: • Private data •

    Private result Server Client Sensed data Monitoring result Online monitoring The server’s privacy: • Private spec. w/o any decryption Conclusion 59 1. We proposed a protocol of oblivious online LTL monitoring 2. We proposed online algorithms Reverse and Block
  58. (Banno, Kyoto U.) The client’s privacy: • Private data •

    Private result Server Client Sensed data Monitoring result Online monitoring The server’s privacy: • Private spec. w/o any decryption Conclusion 60 1. We proposed a protocol of oblivious online LTL monitoring 2. We proposed online algorithms Reverse and Block 3. We experimentally showed scalability and practicality of our algorithms
  59. (Banno, Kyoto U.) The client’s privacy: • Private data •

    Private result Server Client Sensed data Monitoring result Online monitoring The server’s privacy: • Private spec. w/o any decryption Conclusion 61 1. We proposed a protocol of oblivious online LTL monitoring 2. We proposed online algorithms Reverse and Block 3. We experimentally showed scalability and practicality of our algorithms Thank you! In the paper, we discuss: • Details on Reverse and Block • Proposed 2-party protocol • Other experiments