Abstract
Turing complete smart contract formalisms (e.g. Solidity)
are conceptually appealing, but leave the door open to the problems of
verifying completely arbitrary code, a task which can be of arbitrarily
high complexity or can be undecidable. We argue that a more structured
approach, in which smart contract families are designed ab initio with
efficient veriability in mind, provide a much more practical way for-
ward. We emphasise that the boundary between on-chain and off-chain
information, which must always be determined in an application specic
manner, is crucial in determining the practicability of smart contract
verification. We discuss the role of refinement technologies in breaking
down the complexity of smart contract verification, and illustrate the
argument using the Event-B formal modelling framework and Solidity
as implementation vehicle.
are conceptually appealing, but leave the door open to the problems of
verifying completely arbitrary code, a task which can be of arbitrarily
high complexity or can be undecidable. We argue that a more structured
approach, in which smart contract families are designed ab initio with
efficient veriability in mind, provide a much more practical way for-
ward. We emphasise that the boundary between on-chain and off-chain
information, which must always be determined in an application specic
manner, is crucial in determining the practicability of smart contract
verification. We discuss the role of refinement technologies in breaking
down the complexity of smart contract verification, and illustrate the
argument using the Event-B formal modelling framework and Solidity
as implementation vehicle.
| Original language | English |
|---|---|
| Title of host publication | 3rd Workshop on Trusted Smart Contracts |
| Publication status | Accepted/In press - 30 Jan 2019 |
| Event | 3rd Workshop on Trusted Smart Contracts - Frigate Bay, Saint Kitts and Nevis Duration: 22 Feb 2019 → … |
Conference
| Conference | 3rd Workshop on Trusted Smart Contracts |
|---|---|
| Country/Territory | Saint Kitts and Nevis |
| City | Frigate Bay |
| Period | 22/02/19 → … |
Keywords
- Blockchain
- Smart contract
- Solidity
- Verication
- Event-B
- Renement
- Rodin