Formal Methods for Secure Blockchain-Oriented Programming

Despite their tender age, blockchain technologies are bringing a profound impact on the society and 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.

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 yet not well understood and 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.).

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, and we establish an interdisciplinary research program with groundbreaking results at the intersection among cryptography, semantics, verification, and game theory.

On a high-level, we plan to formalize the game-theoretic security properties of DeFi applications, develop synthesis and verification methods for smart contracts, including the first type system for game theoretic security, devise compositionality theorems whose assumptions will be captured in the smart contract typed interfaces, and finally complement the static type system with a proof-carrying code architecture in which security types are checked at run-time by miners, thereby going beyond what can be enforced at compilation time and enabling the secure composition and refinement of smart contracts.