扩展并发分离逻辑的分散系统形式化与可重构
Formalizing and Verifying Decentralized Systems with Extended Concurrent Separation Logic
摘要：
随着区块链等分布式账本技术的快速发展，去中心化技术正变得至关重要和无处不在。已经开发了许多分散式系统，通过这些技术以极大的可靠性和可靠性来解决安全和隐私问题。同时，分散系统的形式化和验证是保证设计正确性和实现安全性的关键。本文提出了一种新的方法，形式化和验证分散系统与一种扩展的并发分离逻辑。我们的逻辑扩展了标准的并发分离逻辑的新功能，包括通信封装，环境感知和节点级推理，增强了模块化和表达能力。此外，我们开发了统一性和兼容性的逻辑，以方便实现。此外，我们通过应用我们的逻辑来形式化和验证去中心化系统中的关键技术，包括共识机制和智能合约，来证明我们方法的有效性和多功能性。
英文摘要：
Decentralized techniques are becoming crucial and ubiquitous with the rapid advancement of distributed ledger technologies such as the blockchain. Numerous decentralized systems have been developed to address security and privacy issues with great dependability and reliability via these techniques. Meanwhile, formalization and verification of the decentralized systems is the key to ensuring correctness of the design and security properties of the implementation. In this paper, we propose a novel method of formalizing and verifying decentralized systems with a kind of extended concurrent separation logic. Our logic extends the standard concurrent separation logic with new features including communication encapsulation, environment perception, and node-level reasoning, which enhances modularity and expressiveness. Besides, we develop our logic with unitarity and compatibility to facilitate implementation. Furthermore, we demonstrate the effectiveness and versatility of our method by applying our logic to formalize and verify critical techniques in decentralized systems including the consensus mechanism and the smart contract.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
