[Multiple projects]
Smart Contracts (SCs) are a cornerstone technology for decentralised finance and decentralised applications which are in the core of Ethereum. Of particular urgency is the problem of security for SCs as high financial incentives make them a prime target for attacks, and blockchain immutability make them impossible to fix once deployed. Numerous exploits of SC vulnerabilities over the lifetime of Ethereum—the first and currently most popular blockchain for deploying SCs—had devastating financial repercussions for users and damaged public confidence in this technology.
This project will examine documented vulnerabilities in historical SCs written in Solidity, Ethereum’s default programming language for SCs. It will detail the nature of the vulnerability, explain the affected code in a report, port the code of the SCs examined in the most recent version of Solidity, and use modern formal verification tools to detect the vulnerability. The focus will primarily be on the Reentrancy vulnerability of SCs, and code such as that of the first DAO SC.
Depending on the interest of the student, the project could utilise compiler techninques to automate some of the above tasks, give emphasis on some tasks or verification tools, or even implement prototype formal verification tools.
Previous work has used a new verification tool developed at TCD to detect four known vulnerabilities in real-world smart contracts. The projects here will mainly focus to replicate this “detective work” in other known vulnerable contracts.