Distributed Runtime Verification of Metric Temporal Properties for Cross-Chain Protocols
Abstract
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. Because smart contracts can automatically transfer ownership of cryptocurrencies, electronic securities, and other valuable assets among untrusting parties, verifying the runtime correctness of smart contracts is a problem of compelling practical interest. 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 employ SMT solving techniques and report experimental results.
Keywords
Cite
@article{arxiv.2204.09796,
title = {Distributed Runtime Verification of Metric Temporal Properties for Cross-Chain Protocols},
author = {Ritam Ganguly and Yingjie Xue and Aaron Jonckheere and Parker Ljung and Benjamin Schornstein and Borzoo Bonakdarpour and Maurice Herlihy},
journal= {arXiv preprint arXiv:2204.09796},
year = {2022}
}
Comments
2022 IEEE 42nd International Conference on Distributed Computing Systems (ICDCS)