A Language for Smart Contracts with Secure Control Flow (Technical Report)

TL;DR

This paper introduces SCIF, a new language for writing smart contracts that enforces security against control-flow attacks by extending information flow mechanisms, aiming to reduce vulnerabilities and improve security guarantees.

Contribution

SCIF is a novel language that enforces control flow security in smart contracts, integrating secure information flow principles into Solidity with minimal overhead.

Findings

SCIF effectively prevents control-flow attacks in smart contracts.

Implementation as a Solidity compiler enables practical adoption.

Case studies demonstrate SCIF's security and efficiency.

Abstract

Smart contracts are frequently vulnerable to control-flow attacks based on confused deputies, reentrancy, and incorrect error handling. These attacks exploit the complexity of interactions among multiple possibly unknown contracts. Existing best practices to prevent vulnerabilities rely on code patterns and heuristics that produce both false positives and false negatives. Even with extensive audits and heuristic tools, new vulnerabilities continue to arise, routinely costing tens of millions of dollars. We introduce SCIF, a language for secure smart contracts, that addresses these classes of control-flow attacks. By extending secure information flow mechanisms in a principled way, SCIF enforces both classic end-to-end information flow security and new security restrictions on control flow, even when SCIF contracts interact with malicious non-SCIF code. SCIF is implemented as a compiler to Solidity. We show how SCIF can secure contracts with minimal overhead through case studies of applications with intricate security reasoning and a large corpus of insecure code.