论文标题
跨链协议的度量时间属性的分布式运行时验证
Distributed Runtime Verification of Metric Temporal Properties for Cross-Chain Protocols
论文作者
论文摘要
涉及多个区块链的交易由跨链协议实施。这些协议基于由计算机网络执行的区块链上运行的智能合约。因为智能合约可以自动转移不信任方之间的加密货币，电子证券和其他有价值的资产的所有权，因此验证智能合约的运行时正确性是令人信服的实际利益的问题。由于智能合约执行是时间敏感的，因此这种验证是具有挑战性的，并且不同区块链上的时钟可能无法完全同步。本文介绍了一种用于监视区块链执行的方法。首先，我们提出了一种通用的运行时验证技术，用于通过利用有界固定时钟的同步来验证公制时间逻辑（MTL）的部分同步分布式计算。其次，我们引入了一种基于进展的公式重写方案，用于监视采用SMT解决技术并报告实验结果的MTL规范。
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.
