Ethereum’s community is standing up to the challenge of securing smart contracts by taking steps to implement the lessons learned from the DAO.
Microsoft Research, Harvard University and Inra, a French national research institute that employs 2700 computer science researchers from the “world’s most prestigious universities”, have published a highly technical paper [PDF] on the formal verification of smart contracts.
The paper presents a framework to analyze and formally verify Ethereum smart contracts using F*, a “functional programming language aimed at program verification.” The initial results are fairly stark and suggest that further research is required:
“[W]e are able to translate and typecheck 46 out of the 396 contracts we collected on https://etherscan.io. Out of these, only a handful are valid… This is a clear sign that a large scale analysis of published contract is likely to uncover widespread vulnerabilities; we leave such analysis to future work.”
University College London (UCL), one of the best universities in the world, has announced two Postgraduate positions focusing on smart contract security under the supervision of Ilya Sergey, Assistant Professor in Programming Principles, Logic and Verification at UCL.
The successful candidates are offered a fully funded scholarship that covers fees and living support for the entire program. The first position is focused on:
“Studying semantic and logical foundations of blockchain-based programming model, with a specific goal in mind: developing sound, scalable and useful tools for computer-aided analysis and verification of smart contracts.”
The second position will focus on “a certified framework for optimizing, sound and secure compilation of smart contracts… [and] develop a provably correct compiler from a high-level contract language (e.g., Solidity) to the low-level bytecode of Ethereum Virtual Machine.”
In addition, a Hackethon will take place in two-three weeks sponsored by Thompson Reuters, in partnership with Barclays and others, where a prize is to be offered for Ethereum smart contract security.
In combination, a picture is developing of strong foundations being established to secure smart contracts by utilizing formal verification tools and other means with researchers around the world taking direct steps to increase smart contract security.
Furthermore, this appears to be a sign of approval from institutions and researchers of Ethereum’s direction and response to the DAO debacle which has allowed the community to put that mistake fully behind and now focus its energies on actually providing solutions.
This is in contrast to Bitcoin’s approach following MT Gox’s hack which was at a far grander scale – half a billion dollars. The response of bitcoin’s community at the time led to little, if any, analysis or solutions provided on how to secure exchanges and wallets with the focus instead on the devastating loss.
Contrary to what some have suggested, the punishment of MT Gox’s users and the burning of half a billion dollars has not led to any lesson learned as clearly shown by the recent hack of bitfinex to the tune of $70 million.
The contrasting response to these hacks by the two communities, therefore, seems to clearly indicate on an empirical basis that the choice of Ethereum’s overwhelming majority to hardfork was the best solution and the path that has already led to analysis and plans for tools and implementations to increase security as well as attracting more researchers, developers, and institutions as the pragmatic community successfully corrected a mistake and addressed its first test in just two months, with the matter now already fading, but an important lesson learned by coders and researchers who are now taking steps to address one of the great challenges of digital currencies and smart contracts: security.
Featured image from Shutterstock.