Deductive verification of smart contracts with Dafny Cassez, Franck; Fuller, Joanne; Antón Quiles, Horacio Mijail
International journal on software tools for technology transfer,
04/2024, Letnik:
26, Številka:
2
Journal Article
Recenzirano
We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language
Dafny
. In our methodology the ...ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise, yet powerful solution for reasoning about contracts that have external calls. This includes arbitrary re-entrancy, which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from
Dafny
to Ethereum Virtual Machine bytecode, the results we obtain from the
Dafny
code can reasonably be assumed to translate to contracts written in languages like Solidity. As a result our approach can readily be used to develop and deploy safer contracts.
We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our methodology the ...ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from Dafny to EVM bytecode, the results we obtain on the Dafny code can reasonably be assumed to hold on Solidity code: the translation of the Dafny code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.
