Formal Methods for Secure Blockchain-Oriented Programming

Introduction

Despite their tender age, blockchain technologies are bringing a profound impact on society and the economy. The swift technological advancements in this domain, however, are not always accompanied by solid scientific foundations, which often follow and try to catch up a posteriori with the proposed engineering solutions.

Challenges in Smart Contracts

The most prominent examples are smart contracts: the total value locked in Decentralized Finance (DeFi) nears 50B USD and, yet, vulnerabilities leading to dramatic financial loss regularly plague virtually all smart contract platforms. The fundamental issue is that security properties for DeFi applications are not yet well understood. Existing verification techniques support basic reachability properties for individual smart contracts, falling short of capturing the game-theoretic and cross-layer security requirements of the DeFi ecosystem (miner bribery, miner extractable value, etc.).

Project Overview

BlockSec will develop the first framework to enforce game-theoretic security in DeFi applications. To achieve this goal, we advocate a holistic approach based on formal methods, embracing verification, synthesis, and consensus techniques.

Research Program

We will establish an interdisciplinary research program with groundbreaking results at the intersection among:

1. Cryptography
2. Semantics
3. Verification
4. Game theory

Goals and Methodology

On a high level, we plan to:

1. Formalize the game-theoretic security properties of DeFi applications.
2. Develop synthesis and verification methods for smart contracts, including the first type system for game-theoretic security.
3. Devise compositionality theorems whose assumptions will be captured in the smart contract typed interfaces.
4. Complement the static type system with a proof-carrying code architecture in which security types are checked at run-time by miners.

This approach will go beyond what can be enforced at compilation time and enable the secure composition and refinement of smart contracts.