论文标题
正式规格和与事件的坚固合同验证
Formal Specification and Verification of Solidity Contracts with Events
论文作者
论文摘要
坚固语言的事件提供了一种分散应用程序的链链服务与这些服务的用户之间的交流方式。事件通常用作从用户的角度使用的合同执行的抽象。因此，用户必须能够理解发射事件的含义和信任。本文提出了一种用于正式规格和验证坚固合同的源级别方法，主要关注事件。我们的方法允许根据其跟踪的链链数据规定事件，并鉴定出定义区块链状态与事件提供的抽象视图之间的对应关系。该方法是在Solc-Verify中实现的，Solc-Verify是一个模块化验证者，以实现固体性，我们通过各种示例演示了其适用性。
Events in the Solidity language provide a means of communication between the on-chain services of decentralized applications and the users of those services. Events are commonly used as an abstraction of contract execution that is relevant from the users' perspective. Users must, therefore, be able to understand the meaning and trust the validity of the emitted events. This paper presents a source-level approach for the formal specification and verification of Solidity contracts with the primary focus on events. Our approach allows specification of events in terms of the on-chain data that they track, and predicates that define the correspondence between the blockchain state and the abstract view provided by the events. The approach is implemented in solc-verify, a modular verifier for Solidity, and we demonstrate its applicability with various examples.
