Blockchain Security


Decentralized cryptocurrencies such as Bitcoin have gained significant popularity due to the numerous applications they enable. Over the years, cryptocurrencies have been gaining expressiveness in terms of the computations one can compute on top of the blockchain. Today, cryptocurrencies such as Ethereum allow users to run arbitrary applications, called smart contracts. A key challenge in developing smart contracts is to ensure that they are correct and free of security vulnerabilities, as bugs in their implementation may result in tremendous financial losses.

To goal of this project is to research and design novel techniques that would significantly ease the task of developing correct and reliable smart contracts. To address these challenges, we develop automated analysis and synthesis techniques for smart contracts. These include both static analysis as well as dynamic analysis techniques (e.g. symbolic execution), synthesis of secure code, automatic generation of patches for contract code, and others.

Securify: Formal Verification for Ethereum Smart Contracts

As part of this project, we have developed Securify, the first automated system for formal verification of smart contracts.


The main advantages of Securify over other solutions is that it is the first security checker that provides: (i) automation, to enable all users to verify contracts, (ii) guarantees, to avoid reporting vulnerable contracts are safe, and (iii) extensibility, to capture new security vulnerability that are regularly discovered. Securify is capable to pinpoint the instructions that may cause security issues and therefore provides practical and useful guidelines to contract developers.

Existing solutions based on executing the contract check only a subset of the possible paths and can therefore miss critical security problems. Further, approaches based on interactive-theorem provers can provide strong guarantees, for all paths, but they cannot be easily automated or easily extended. In contrast, Securify combines the best of both worlds: it analyzes all paths while being fully automated. Further, Securify features a designated domain-specific language for specifying vulnerabilities, which makes it easy to keep Securify up-to-date with current security and other reliability issues.

You can find access to the beta version of Securify at: http://www.securify.ch

Contact Us

If you are interested in getting access to the full release of Securify, please send an email to: contact@securify.ch

People behind Securify

Florian Buenzli

More info

Dr. Petar Tsankov

More info

Andrei Dan

More info







Dr. Dana Drachsler-Cohen

More info

Dr. Arthur Gervais

More info







Prof. Dr. Martin Vechev

More info

Disclaimer

This service by ETH Zurich, Department of Computer Science, Software Reliability Lab, is free of charge. We accept only legal pieces of code. All entries are logged for research and improvement of service. ETH Zurich does not warrant any rights or service levels, nor does it acquire any rights on the code entered. Swiss law is applicable. The place of jurisdiction is Zurich, Switzerland. By sending code to this site, you warrant that all your entries are in your sole responsibility and you do not infringe any laws or third-party rights like copyrights and the like. ETH Zurich and its employees shall not be liable for any entries and for any damages resulting thereof. You agree to indemnify, defend and hold them harmless from any legal or financial demands or arising out of the breach of these terms of use, especially from third-party claims regarding infringement of copyrights and the like.