Existing vulnerabilities in smart contracts

Vulnerabilities in smart contract have the potential to be very serious. Given that the smart contracts are placed on the blockchain, any party is able to inspect the smart contract for vulnerabilities and then exploit the resulting flaws. Further, once deployed, most of the smart contracts are not able to be updated meaning that flaws are irrevocable. Since the smart contract is likely to manage actual financial assets, people have a direct financial motive for attacking the smart contract.

The most well-known attack against a smart contract was the DAO attack in which an attacker managed to steal almost $50M before being detected. This attack was only reversed following a very controversial fork of the Ethereum blockchain. This attack was the result of a simple (and indeed well-known) programming flaw in the smart contract itself.

The need for formal verification of smart contracts has been widely recognised over the past two years and there has been some initial work done in this area.

Our Research program

  • Automatic formal verification of smart contracts

    Develop technology that enables an individual smart contract to be proven correct against user-specified requirements, assuming that the underlying blockchain and smart contract platform is correct.

  • Verified blockchain and smart contract platform

    Building a new smart contract platform that is provably correct by construction.

  • Testing frameworks for smart contracts

    Develop a high-quality, developer-friendly, testing framework that supports one or more popular smart contract languages.

Our Team

Chen Bangdao


Former associate professor of Shenzhen Institute of Advanced Technology of Chinese Academy of Sciences. Bachelor from Shanghai Jiaotong University, and PhD from the Department of Computers of University of Oxford. Rich research and engineering experiences in network security, payment security and communication security. Founded the first information security company in University of Oxford in January 2014.

Bill Roscoe

Chief Scientist

Former director of the Department of Computers of University of Oxford (2003-2014), member of Royal Academy of Engineering, chairman of the Information Security Committee and the Committee of Computer Sciences of University of Oxford, a renowned computer scientist in the world, and a senior scientist of University of Oxford (more than 40 years). His main researches and achievements include information security, computer system verification and concurrency etc. Sir Tony Hoare, his advisor, is one of the pioneers in computer sciences. Professor Bill Roscoe is of exceptional experiences in scientific research management, and the Department of Computers of University of Oxford rose from a small research organization with only 3 professors to a world’s top computer sciences organization with more than 30 full professors, 40 instructors and a total of more than 250 researchers.

Chen Zhong

Chief Scientist

Standing director of CCF, deputy director of the Information Security Committee of CCF, member of the Network and Data Communications Committee of CCF, professor of Peking University, former dean of the School of Software & Microelectronics of Peking University (2002-2010), founder and director of the Financial and Information Research Center of Peking University, director of the Network and Information Security Lab of Peking University, deputy director of the Review Board for Degrees in Engineering of Peking University. His research interests lies broadly in the doman-oriented software engineering, network and information security, system software and embedded systems, information systems and system integration.