New scanner audits smart contracts more reliably

Q: Petar Tsankov, in early 2017 a team of researchers, including Professor M. Vechev, Dr H. Ritzdorf and yourself, founded the start-up ChainSecurity. To what aim?

PT: At the time, we were working on several research projects in the area of security and privacy for smart contracts at the ICE Center at ETH – an interdisciplinary and inter-department R&D centre with the mission of facilitating research-industrial interaction in the areas of AI, blockchain, security, and networks. Securify was the first of many projects that we made available to the public and its release triggered a massive interest in the community, which essentially forced us to incorporate a start-up. We decided to take on this challenge together: founding a start-up and then building easy-to-use security scanners for smart contracts to raise the level of security in the Ethereum ecosystem.

Q: Let us start at the beginning: what exactly is a smart contract and what does a smart contract scanner do?

PT: Like a traditional contract, a smart contract usually defines certain rules. For example, a smart travel contract implements a flight ticket insurance policy. Unlike a traditional contract, the smart contract is a piece of software that runs on a blockchain platform, such as Ethereum. The insurance holder purchases the insurance using crypto currency. In case of an insurance claim, e.g. a cancelled flight, the insured amount will be paid out in crypto currency too. One main benefit of smart contracts is that they are executed securely by the blockchain. Another key benefit is lower costs by cutting out the middleman. A smart contract does not require the costly services of an insurance company.
A smart contract scanner is a tool that inspects the smart contract’s source code and identifies critical security vulnerabilities. For example, a vulnerability in a decentralized insurance smart contract may allow an attacker to drain all the funds from the smart contract and leave no funds for users with valid claims.

Q: And the Ethereum environment is where the contracts are created and stored?

PT: You could say that. Ethereum is an open-source, public, blockchain-based distributed computing platform on which contracts can be set up and deployed to handle money transactions. This means that users can write any type of contract and simply deploy it on Ethereum.

Q: Which specific problem(s) had to be solved to successfully develop a smart scanner that is more reliable and easier to use?

PT: Existing smart scanners would only inspect a subset of all contract behaviours and thereby risk missing critical security liabilities. However, making the jump from inspecting some to all behaviours of the contract is highly nontrivial, as the number of possible behaviours can exceed even the number of atoms in the universe.

Q: What were the main technical challenges you had to overcome? How did you succeed?

PT: The main technical challenge in building a security scanner for smart contracts was finding a way to effectively explore all the potential behaviours of the contract. After six months, we had come up with a new abstraction, tailored specifically to the domain of smart contracts, enabling them to scan all behaviours for vulnerabilities in just a few minutes. In short, the new abstraction allows specific features of the smart contract to be inspected, instead of explicitly enumerating the vast number of all individual behaviours of the contract. Another key challenge was figuring out which features are sufficient to determine whether a contract is vulnerable or secure. For example, for many of the critical vulnerabilities, it is sufficient to check how critical variables depend on each other, making it unnecessary to enumerate behaviours one by one.

Q: Your new smart scanner called Securify was released in June 2018. What are the practical benefits?

PT: The algorithm that provides the basis of the new technology offers several advantages regarding thoroughness and usability. First, Securify is able to prove the safety of the contract for specific properties. Second, it is scalable enough to handle Ethereum projects of large size. Third, with the ability to scan for 18 critical vulnerabilities, it is currently the most comprehensive security analyser for Ethereum contracts. And fourth, Securify allows for improved usability as it supports the scanning of git repositories, which is a widely used protocol for storing and tracking the changes of software projects.

Q: Do you and your partners already have a next challenge in mind?

PT: Yes. We have been working in parallel on other challenges for a while now. One limitation of our publicly available security scanner is that it only checks for known security vulnerabilities. We are now working on a new technology that will enable security experts to certify a smart contract with respect to custom requirements provided in the specification. Moreover, we also have a new result that can make smart contracts privacy-compliant, even when deployed on public blockchains (where all data is visible to anyone). This technology is essential to be able to use blockchains in compliance with regulations such as the General Data Protection Regulation (GDPR), which was recently adopted by the EU to protect the privacy of all individuals within the European Union. I believe that these two results address key challenges in constructing secure and privacy-compliant smart contracts.