Compositional Security for Reentrant Applications

TL;DR

This paper addresses the challenge of ensuring secure composition of smart contracts by formalizing reentrancy vulnerabilities and proposing a security type system that enforces secure information flow and reentrancy protections.

Contribution

It introduces a formal definition of reentrancy, a security condition for protecting invariants, and a type system combined with runtime mechanisms for secure smart contract composition.

Findings

The type system provably enforces secure information flow.

Runtime mechanisms ensure security even with unknown code.

Helps locate and fix recent vulnerabilities.

Abstract

The disastrous vulnerabilities in smart contracts sharply remind us of our ignorance: we do not know how to write code that is secure in composition with malicious code. Information flow control has long been proposed as a way to achieve compositional security, offering strong guarantees even when combining software from different trust domains. Unfortunately, this appealing story breaks down in the presence of reentrancy attacks. We formalize a general definition of reentrancy and introduce a security condition that allows software modules like smart contracts to protect their key invariants while retaining the expressive power of safe forms of reentrancy. We present a security type system that provably enforces secure information flow; in conjunction with run-time mechanisms, it enforces secure reentrancy even in the presence of unknown code; and it helps locate and correct recent high-profile vulnerabilities.