论文标题
具有扩展并发分离逻辑的正式化和验证分散系统
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.
