Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption

被引：3

作者：

Banno, Ryotaro ^{[1
]}

Matsuoka, Kotaro ^{[1
]}

Matsumoto, Naoki ^{[1
]}

Bian, Song ^{[2
]}

Waga, Masaki ^{[1
]}

Suenaga, Kohei ^{[1
]}

机构：

[1] Kyoto Univ, Kyoto, Japan

[2] Beihang Univ, Beijing, Peoples R China

来源：

COMPUTER AIDED VERIFICATION (CAV 2022), PT I | 2022年 / 13371卷

关键词：

INTERNET; THINGS;

D O I：

10.1007/978-3-031-13185-1_22

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：447 / 468

页数：22

共 38 条

[1]

Abbas H., 2019, EMSOFT 2019, P11

[2] A NOTE ON THE NUMBER OF QUERIES NEEDED TO IDENTIFY REGULAR LANGUAGES [J].

ANGLUIN, D .

INFORMATION AND CONTROL, 1981, 51 (01) :76-87

[3] The Internet of Things: A survey [J].

Atzori, Luigi ;

Iera, Antonio ;

Morabito, Giacomo .

COMPUTER NETWORKS, 2010, 54 (15) :2787-2805

[4]

Banno R., OBLIVIOUS ONLINE MON

[5]

Bartocci Ezio, 2018, Lectures on Runtime. Verification Introductory and Advanced Topics. LNCS 10457, P135, DOI 10.1007/978-3-319-75632-5_5

[6] Runtime Verification for LTL and TLTL [J].

Bauer, Andreas ;

Leucker, Martin ;

Schallhart, Christian .

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2011, 20 (04)

[7]

Bellare M., 2005, UCSD CSE 207 Course Notes, P283

[8]

Blanton M, 2010, LECT NOTES COMPUT SC, V6166, P49, DOI 10.1007/978-3-642-13739-6_4

[9]

Brakerski Z., 2020, IACR CRYPTOLOGY EPRI, P1024

[10]

Brakerski Z., 2012, P ITCS, P309, DOI [10.1145/2090236.2090262, DOI 10.1145/2090236.2090262]

← 1 2 3 4 →