Distributed Runtime Verification of Metric Temporal Properties for Cross-Chain Protocols
Author
Abstract

Protocol Verification - Transactions involving multiple blockchains are implemented by cross-chain protocols. These protocols are based on smart contracts, programs that run on blockchains, executed by a network of computers. Verifying the runtime correctness of smart contracts is a problem of compelling practical interest since, smart contracts can automatically transfer ownership of cryptocurrencies, electronic securities, and other valuable assets among untrusting parties. Such verification is challenging since smart contract execution is time sensitive, and the clocks on different blockchains may not be perfectly synchronized. This paper describes a method for runtime monitoring of blockchain executions. First, we propose a generalized runtime verification technique for verifying partially synchronous distributed computations for the metric temporal logic (MTL) by exploiting bounded-skew clock synchronization. Second, we introduce a progression-based formula rewriting scheme for monitoring MTL specifications which employs SMT solving techniques and report experimental results.

Year of Publication
2022
Date Published
jul
Publisher
IEEE
Conference Location
Bologna, Italy
ISBN Number
978-1-66547-177-0
URL
https://ieeexplore.ieee.org/document/9912283/
DOI
10.1109/ICDCS54860.2022.00012
Google Scholar | BibTeX | DOI