Comprehensive Blockchain Security @ ICE

The ICE center initiative to secure blockchains aims to conduct fundamental research on the key challenges of blockchain platforms and to develop state-of-the-art solutions together with infrastructure providers such as the Ethereum foundation and the Web3 foundation.

To achieve this mission, the ICE center conducts research across all layers of blockchain platforms:

  Enforcing data privacy on public blockchains   Learn more
  Security analysis and correctness certification of smart contracts   Learn more
  Validating the correctness of smart contract compilers   Learn more
  Correctness and security guarantees of next-generation consensus algorithms   Learn more
  Protecting blockchains against network-level attacks   Learn more


Data privacy for smart contracts

Smart contracts on public blockchains leak all of their data, making them unsuitable to handle private data and precluding their adoption in many realistic scenarios. In this project, we develop new languages that can be used to enforce data privacy of smart contracts using cryptographic primitives, such as non-interactive zero knowledge proofs.

Security and certificatoin of smart contracts

Millions worth of USD have been lost due to security issues in smart contracts. In this project, we develop scalable security scanners that can identify security bugs in smart contracts. Further, we build automated verifiers that can certify the correctness of smart contracts with respect to their formal specification.

This project is partially funded by the Ethereum foundation.

Validating the correctness of blockchain compilers

The correctness of compilers is of crucial importance to the Ethereum ecosystem as smart contracts are typically validated and audited with respect to requirements at the source level. The goal of this project is to develop an automated framework for large-scale, systematic testing and validation of blockchain compilers (such as solc).

This project is funded by the Ethereum foundation.

Correctness and security guarantees of consensus protocols

Next-generation consensus algorithms will use new primitives, such as finality gadgets that will allow a separation of block production and the finality of blocks. Ensuring consensus algorithms operate correctly is notoriously difficult, and in this project we tackle this problem.

This project is sponsored by the Web3 foundation.

Protecting blockchains against network-level attacks

In this project we study the impact that Internet routing attacks (such as BGP hijacks) on the security of blockchain protocols.


VerX: Functional Verification of Smart Contracts
Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, Martin Vechev
IEEE S&P 2020

zkay: Specifying and Enforcing Data Privacy in Smart Contracts
Samuel Steffen, Benjamin Bichsel, Mario Gersbach, Noa Melchior, Petar Tsankov, Martin Vechev
ACM CCS 2019

Learning to Fuzz from Symbolic Execution with Application to Smart Contracts
Jingxuan He, Mislav Balunovic, Nodar Ambroladze, Petar Tsankov, Martin Vechev
ACM CCS 2019

SABRE: Protecting Bitcoin against Routing Attacks
Maria Apostolaki, Gian Marti, Jan Müller, Laurent Vanbever
NDSS Symposium 2019

Securify: Practical Security Analysis of Smart Contracts
Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Buenzli, Martin Vechev
ACM CCS 2018

Hijacking Bitcoin: Routing Attacks on Cryptocurrencies
Maria Apostolaki, Aviv Zohar, Laurent Vanbever
IEEE S&P 2017