Deductive Verification of Smart Contracts with Dafny
International Journal on Software Tools for Technology Transfer(2024)
摘要
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.
更多查看译文
关键词
Formal verification,Ethereum,Smart contracts,Dafny
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要