论文标题
正式验证事件B中的坚固合同
Formal Verification of Solidity contracts in Event-B
论文作者
论文摘要
智能合约是区块链的工件，可提供物理交易的不可变和可验证的规格。坚固性是一种特定领域的编程语言，目的是定义智能合约。它旨在减少通过以太坊等分布式分类帐上执行合同所带来的交易成本。但是，坚固的合同需要遵守需要正式验证和认证的安全和保障要求。本文提出了一种通过将坚固合同转换为事件B模型的方法，支持认证。为此，我们定义了一个约束的坚固性子集和转移函数，该功能将坚固的合同转化为事件B模型。然后，我们利用事件B方法功能来完善不同级别的抽象级别模型，以验证固体合同的特性。我们可以借助Rodin平台来验证事件-B模型的生成证明义务。
Smart contracts are the artifact of the blockchain that provide immutable and verifiable specifications of physical transactions. Solidity is a domain-specific programming language with the purpose of defining smart contracts. It aims at reducing the transaction costs occasioned by the execution of contracts on the distributed ledgers such as the Ethereum. However, Solidity contracts need to adhere safety and security requirements that require formal verification and certification. This paper proposes a method to meet such requirements by translating Solidity contracts to Event-B models, supporting certification. To that purpose, we define a restrained Solidity subset and a transfer function which translates Solidity contracts to Event-B models. Then we take advantage of Event-B method capabilities to refine models at different levels of abstraction to verify Solidity contracts' properties. And we can verify the generated proof obligations of the Event-B model with the help of the Rodin platform.
