Distributed Runtime Verification of Metric Temporal Properties for Cross-Chain Protocols
| Autor: | Ganguly, Ritam, Xue, Yingjie, Jonckheere, Aaron, Ljung, Parker, Schornstein, Benjamin, Bonakdarpour, Borzoo, Herlihy, Maurice |
|---|---|
| Rok vydání: | 2022 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: 2022 IEEE 42nd International Conference on Distributed Computing Systems (ICDCS) |
| Databáze: | arXiv |
| Externí odkaz: |
|