Secure Smart Contracts with Isabelle/Solidity

点击翻译按钮获取中文摘要

Smart contracts are digital contracts stored on a blockchain that are automatically executed when predetermined terms and conditions are met.They are often used to automate financial transactions and thus they hold great potential to transform and disrupt the financial industry.In particular it is estimated that blockchain and smart contracts can add up to $72.2B to the UK's GDP by 2030 and create up to 700,000 new jobs by 2030.Technically, smart contracts are programs and as such, they may contain bugs.However, since smart contracts are often used to automate financial transactions, exploiting these bugs may result in huge financial damages.In 2016, for example, a vulnerability in a smart contract was exploited, resulting in a loss of approximately $60M.More recently, hackers had exploited a vulnerability in a smart contract to steal $600M.In general, it is estimated that since 2019, more than $5B were lost due to vulnerabilities in smart contracts.This threatens society's trust in smart contracts and thus limits their potential for the development of FinTech, one of the most promising sectors for the UK economy.Unfortunately, however, even rigorous testing and auditing cannot guarantee that a smart contract does what it is supposed to do.In the best case scenario, vulnerabilities can be found with these techniques but they can never guarantee their absence.Thus, with this project, we will develop tools and techniques to support the verification of smart contracts to achieve the highest degree of reliability.Finally, we will engage in training next generation experts in the verification of smart contracts by hosting a summer school on formal methods for blockchains in Exeter.