Showing 1–8 of 8 results for author: Banno, R

Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption

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

Abstract: When monitoring a cyber-physical system (CPS) from a remote server, kee** 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… ▽ More When monitoring a cyber-physical system (CPS) from a remote server, kee** 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. △ Less

Submitted 26 May, 2024; originally announced May 2024.

Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption

Authors: Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga, Kohei Suenaga

Abstract: 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 wit… ▽ More 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. △ Less

Submitted 3 June, 2022; originally announced June 2022.

Comments: This is the extended version of a paper to appear at CAV 2022

Verification of a Merkle Patricia Tree Library Using F*

Authors: Sota Sato, Ryotaro Banno, Jun Furuse, Kohei Suenaga, Atsushi Igarashi

Abstract: A Merkle tree is a data structure for representing a key-value store as a tree. Each node of a Merkle tree is equipped with a hash value computed from those of their descendants. A Merkle tree is often used for representing a state of a blockchain system since it can be used for efficiently auditing the state in a trustless manner. Due to the safety-critical nature of blockchains, ensuring the cor… ▽ More A Merkle tree is a data structure for representing a key-value store as a tree. Each node of a Merkle tree is equipped with a hash value computed from those of their descendants. A Merkle tree is often used for representing a state of a blockchain system since it can be used for efficiently auditing the state in a trustless manner. Due to the safety-critical nature of blockchains, ensuring the correctness of their implementation is paramount. We show our formally verified implementation of the core part of Plebeia using F*. Plebeia is a library to manipulate an extension of Merkle trees (called Plebeia trees). It is being implemented as a part of the storage system of the Tezos blockchain system. To this end, we gradually ported Plebeia to F*; the OCaml code extracted from the modules ported to F* is linked with the unverified part of Plebeia. By this gradual porting process, we can obtain a working code from our partially verified implementation of Plebeia; we confirmed that the binary passes all the unit tests of Plebeia. More specifically, we verified the following properties on the implementation of Plebeia: (1) Each tree-manipulating function preserves the invariants on the data structure of a Plebeia tree and satisfies the functional requirements as a nested key-value store; (2) Each function for serializing/deserializing a Plebeia tree to/from the low-level storage is implemented correctly; and (3) The hash function for a Plebeia tree is relatively collision-resistant with respect to the cryptographic safety of the blake2b hash function. During porting Plebeia to F*, we found a bug in an old version of Plebeia, which was overlooked by the tests bundled with the original implementation. To the best of our knowledge, this is the first work that verifies a production-level implementation of a Merkle-tree library by F*. △ Less

Submitted 9 June, 2021; originally announced June 2021.

ACM Class: D.2.4; E.1

Virtual Secure Platform: A Five-Stage Pipeline Processor over TFHE

Authors: Kotaro Matsuoka, Ryotaro Banno, Naoki Matsumoto, Takashi Sato, Song Bian

Abstract: We present Virtual Secure Platform (VSP), the first comprehensive platform that implements a multi-opcode general-purpose sequential processor over Fully Homomorphic Encryption (FHE) for Secure Multi-Party Computation (SMPC). VSP protects both the data and functions on which the data are evaluated from the adversary in a secure computation offloading situation like cloud computing. We proposed a c… ▽ More We present Virtual Secure Platform (VSP), the first comprehensive platform that implements a multi-opcode general-purpose sequential processor over Fully Homomorphic Encryption (FHE) for Secure Multi-Party Computation (SMPC). VSP protects both the data and functions on which the data are evaluated from the adversary in a secure computation offloading situation like cloud computing. We proposed a complete processor architecture with a five-stage pipeline, which improves the performance of the VSP by providing more parallelism in circuit evaluation. In addition, we also designed a custom Instruction Set Architecture (ISA) to reduce the gate count of our processor, along with an entire set of toolchains to ensure that arbitrary C programs can be compiled into our custom ISA. In order to speed up instruction evaluation over VSP, CMUX Memory based ROM and RAM constructions over FHE are also proposed. Our experiments show that both the pipelined architecture and the CMUX Memory technique are effective in improving the performance of the proposed processor. We provide an open-source implementation of VSP which achieves a per-instruction latency of less than 1 second. We demonstrate that compared to the best existing processor over FHE, our implementation runs nearly 1,600$\times$ faster. △ Less

Submitted 19 October, 2020; originally announced October 2020.

Comments: Accepted in USENIX Security '21. This is a long version

Trail: A Blockchain Architecture for Light Nodes

Authors: Ryunosuke Nagayama, Ryohei Banno, Kazuyuki Shudo

Abstract: In Bitcoin and Ethereum, nodes require large storage capacity to maintain all the blockchain data, such as transactions, UTXOs, and account states. As of May 2020, the storage size of the Bitcoin blockchain has expanded to 270 GB, and it will continue to increase. This storage requirement is a major hurdle to becoming a block proposer or validator. Although many studies have attempted to reduce th… ▽ More In Bitcoin and Ethereum, nodes require large storage capacity to maintain all the blockchain data, such as transactions, UTXOs, and account states. As of May 2020, the storage size of the Bitcoin blockchain has expanded to 270 GB, and it will continue to increase. This storage requirement is a major hurdle to becoming a block proposer or validator. Although many studies have attempted to reduce the storage size, in the proposed methods, a node cannot keep all blocks or cannot generate a block. We propose an architecture called Trail that allows nodes to hold all blocks in a small storage and to generate and validate blocks and transactions. Trail does not depend on a consensus algorithm or fork choice rule. In this architecture, a client who issues transactions has the data to prove its own balances and can generate a transaction containing the proof of balances. The nodes in Trail do not store transactions, UTXOs and account balances: they keep only blocks. The blocksize is approximately 8 KB, which is 100 times smaller than that of Bitcoin. Further, the block size is constant regardless of the number of accounts and the number of transactions. Compared to traditional blockchains, clients who issue transactions must store additional data. However, we show that proper data archiving can keep the account device storage size small. Trail allows more users to be block proposers and validators and improves the decentralization of the blockchain. △ Less

Submitted 15 July, 2020; originally announced July 2020.

Comments: Proc. 25th IEEE Symposium on Computers and Communications (IEEE ISCC 2020)

Identifying Impacts of Protocol and Internet Development on the Bitcoin Network

Authors: Ryunosuke Nagayama, Kazuyuki Shudo, Ryohei Banno

Abstract: Improving transaction throughput is an important challenge for Bitcoin. However, shortening the block generation interval or increasing the block size to improve throughput makes it sharing blocks within the network slower and increases the number of orphan blocks. Consequently, the security of the blockchain is sacrificed. To mitigate this, it is necessary to reduce the block propagation delay. B… ▽ More Improving transaction throughput is an important challenge for Bitcoin. However, shortening the block generation interval or increasing the block size to improve throughput makes it sharing blocks within the network slower and increases the number of orphan blocks. Consequently, the security of the blockchain is sacrificed. To mitigate this, it is necessary to reduce the block propagation delay. Because of the contribution of new Bitcoin protocols and the improvements of the Internet, the block propagation delay in the Bitcoin network has been shortened in recent years. In this study, we identify impacts of compact block relay---an up-to-date Bitcoin protocol---and Internet improvement on the block propagation delay and fork rate in the Bitcoin network from 2015 to 2019. Existing measurement studies could not identify them but our simulation enables it. The experimental results reveal that compact block relay contributes to shortening the block propagation delay more than Internet improvements. The block propagation delay is reduced by 64.5% for the 50th percentile and 63.7% for the 90th percentile due to Internet improvements, and by 90.1% for the 50th percentile and by 87.6% for the 90th percentile due to compact block relay. △ Less

Submitted 3 June, 2020; v1 submitted 11 December, 2019; originally announced December 2019.

Comments: Proc. 25th IEEE Symposium on Computers and Communications (IEEE ISCC 2020)

Implicit Regularization in Over-parameterized Neural Networks

Authors: Masayoshi Kubo, Ryotaro Banno, Hidetaka Manabe, Masataka Minoji

Abstract: Over-parameterized neural networks generalize well in practice without any explicit regularization. Although it has not been proven yet, empirical evidence suggests that implicit regularization plays a crucial role in deep learning and prevents the network from overfitting. In this work, we introduce the gradient gap deviation and the gradient deflection as statistical measures corresponding to th… ▽ More Over-parameterized neural networks generalize well in practice without any explicit regularization. Although it has not been proven yet, empirical evidence suggests that implicit regularization plays a crucial role in deep learning and prevents the network from overfitting. In this work, we introduce the gradient gap deviation and the gradient deflection as statistical measures corresponding to the network curvature and the Hessian matrix to analyze variations of network derivatives with respect to input parameters, and investigate how implicit regularization works in ReLU neural networks from both theoretical and empirical perspectives. Our result reveals that the network output between each pair of input samples is properly controlled by random initialization and stochastic gradient descent to keep interpolating between samples almost straight, which results in low complexity of over-parameterized neural networks. △ Less

Submitted 5 March, 2019; originally announced March 2019.

SimBlock: A Blockchain Network Simulator

Authors: Yusuke Aoki, Kai Otsuki, Takeshi Kaneko, Ryohei Banno, Kazuyuki Shudo

Abstract: Blockchain, which is a technology for distributedly managing ledger information over multiple nodes without a centralized system, has elicited increasing attention. Performing experiments on actual blockchains are difficult because a large number of nodes in wide areas are necessary. In this study, we developed a blockchain network simulator SimBlock for such experiments. Unlike the existing simul… ▽ More Blockchain, which is a technology for distributedly managing ledger information over multiple nodes without a centralized system, has elicited increasing attention. Performing experiments on actual blockchains are difficult because a large number of nodes in wide areas are necessary. In this study, we developed a blockchain network simulator SimBlock for such experiments. Unlike the existing simulators, SimBlock can easily change behavior of node, so that it enables to investigate the influence of nodes' behavior on blockchains. We compared some simulation results with the measured values in actual blockchains to demonstrate the validity of this simulator. Furthermore, to show practical usage, we conducted two experiments which clarify the influence of neighbor node selection algorithms and relay networks on the block propagation time. The simulator could depict the effects of the two techniques on block propagation time. The simulator will be publicly available in a few months. △ Less

Submitted 19 March, 2019; v1 submitted 28 January, 2019; originally announced January 2019.

Comments: Proc. 2nd Workshop on Cryptocurrencies and Blockchains for Distributed Systems (CryBlock 2019) (in conj. with INFOCOM 2019)