@inproceedings{687fa11526654479989731f77ee4ab9b,
title = "Formal simulation and verification of solidity contracts in event-B",
abstract = "Smart contracts are the artifact of the blockchain that provides 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 Ethereum. However, Solidity contracts need to adhere to 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 that translates Solidity contracts to Event-B models. Besides, we have implemented a translator to improve the conversion efficiency. As a case study, we take advantage of EventB method capabilities to simulate models at different levels of abstraction and to express the properties of a typical smart contract: Honeypot contract. Lastly, we verify the generated proof obligations of the Event-B model with the help of the Rodin platform.",
keywords = "Blockchain, Event-B model, Formal verification for security, Smart contract, Solidity",
author = "Jian Zhu and Kai Hu and Mamoun Filali and Bodeveix, \{Jean Paul\} and Talpin, \{Jean Pierre\} and Haitao Cao",
note = "Publisher Copyright: {\textcopyright} 2021 IEEE.; 45th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2021 ; Conference date: 12-07-2021 Through 16-07-2021",
year = "2021",
month = jul,
doi = "10.1109/COMPSAC51774.2021.00183",
language = "英语",
series = "Proceedings - 2021 IEEE 45th Annual Computers, Software, and Applications Conference, COMPSAC 2021",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "1309--1314",
editor = "Chan, \{W. K.\} and Bill Claycomb and Hiroki Takakura and Ji-Jiang Yang and Yuuichi Teranishi and Dave Towey and Sergio Segura and Hossain Shahriar and Sorel Reisman and Ahamed, \{Sheikh Iqbal\}",
booktitle = "Proceedings - 2021 IEEE 45th Annual Computers, Software, and Applications Conference, COMPSAC 2021",
address = "美国",
}