Distributed Runtime Verification of Metric Temporal Properties for Cross-Chain Protocols
Distributed Runtime Verification of Metric Temporal Properties for Cross-Chain Protocols
复制标题
DOI：
10.1109/icdcs54860.2022.00012
复制
发表时间：
2022-04
期刊：
影响因子：
--
通讯作者：
R. Ganguly;Yingjie Xue;Aaron Jonckheere;Parker Ljung;Benjamin Schornstein;Borzoo Bonakdarpour;M. Herlihy
中科院分区：
文献类型：
--
作者：
R. Ganguly;Yingjie Xue;Aaron Jonckheere;Parker Ljung;Benjamin Schornstein;Borzoo Bonakdarpour;M. Herlihy
涉及多个区块链的交易通过跨链协议实现。这些协议基于智能合约，即在区块链上运行的程序，由计算机网络执行。智能合约的运行时正确性是一个令人信服的实际利益问题，因为智能合约可以在不信任的各方之间自动转移加密货币，电子证券和其他有价值资产的所有权。这种验证具有挑战性，因为智能合约的执行是时间敏感的，并且不同区块链上的时钟可能无法完全同步。本文描述了一种用于区块链执行的运行时监控方法。首先，我们提出了一个广义的运行时验证技术，验证部分同步分布式计算的度量时序逻辑（MTL），利用有界偏斜时钟同步。其次，我们介绍了一个基于进展的公式重写计划监测MTL规格采用SMT解决技术和报告的实验结果。
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.