跨链协议的度量时序性质分布式运行时验证
分布式、并行与集群计算
2022-05-09 v1 形式语言与自动机理论
摘要
涉及多个区块链的交易由跨链协议实现。这些协议基于智能合约（在区块链上运行、由计算机网络执行的程序）。由于智能合约可以在互不信任的各方之间自动转移加密货币、电子证券及其他有价值资产的所有权，验证智能合约的运行时正确性是一个具有迫切实际意义的问题。此类验证具有挑战性，因为智能合约执行对时间敏感，且不同区块链上的时钟可能并非完美同步。本文描述了一种用于区块链执行运行时监控的方法。首先，我们利用有界偏移时钟同步，提出了一种针对度量时序逻辑（MTL）的部分同步分布式计算的广义运行时验证技术。其次，我们引入了一种基于递进的公式重写方案，用于监控采用 SMT 求解技术的 MTL 规约，并报告了实验结果。
引用
@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}
}
备注
2022 IEEE 42nd International Conference on Distributed Computing Systems (ICDCS)