Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Siqiu Yao, Haobin Ni, Stephanie Ma, Noah Schiff, Andrew C. Myers, Ethan Cecchetti

TL;DR

SCIF addresses the risk of control-flow attacks in open multi-contract ecosystems by introducing an information-flow based smart contract language that enforces both data integrity and secure control flow. It extends traditional IFC with explicit endorsements, dynamic trust checks, reentrancy locks, and distinct exception semantics, and targets secure compilation to Solidity. The approach demonstrates CDA safety, robust reentrancy protection, and explicit error handling through a formal Core SCIF model, a complete implementation, and extensive case studies across real-world vulnerable contracts, with modest runtime overhead. This work offers a principled, scalable foundation for secure multi-contract programming in decentralized environments and suggests avenues for extending IFC-based security to broader software contexts.

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.

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

TL;DR

SCIF addresses the risk of control-flow attacks in open multi-contract ecosystems by introducing an information-flow based smart contract language that enforces both data integrity and secure control flow. It extends traditional IFC with explicit endorsements, dynamic trust checks, reentrancy locks, and distinct exception semantics, and targets secure compilation to Solidity. The approach demonstrates CDA safety, robust reentrancy protection, and explicit error handling through a formal Core SCIF model, a complete implementation, and extensive case studies across real-world vulnerable contracts, with modest runtime overhead. This work offers a principled, scalable foundation for secure multi-contract programming in decentralized environments and suggests avenues for extending IFC-based security to broader software contexts.

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.
Paper Structure (41 sections, 7 equations, 16 figures, 2 tables)

This paper contains 41 sections, 7 equations, 16 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background
  3. The SCIF Threat Model
  4. Integrity via Information Flow
  5. Confused Deputy Attacks
  6. Reentrancy Vulnerabilities
  7. Exception-based Vulnerabilities
  8. Overview of SCIF
  9. Information Flow Labels
  10. CDA Prevention
  11. Reentrancy Attack Prevention
  12. Exception Handling
  13. Dynamic Integrity Checks
  14. Contract Interfaces
  15. Dependent labels and mappings
  16. ...and 26 more sections

Figures (16)

  • Figure 1: Exploitation of a confused deputy. Dashed arrows denote calls controlled by the untrusted user, and double blue lines denote calls carrying (or interfaces requiring) the trusted authority of the deputy. The callback is dashed and blue; hence, the attacker can exploit the target.
  • Figure 2: Simplified Solidity code for the Dexible bug.
  • Figure 3: Distilled Solidity code for the Uniswap bug.
  • Figure 4: Distilled Solidity code for the KoET bug.
  • Figure 5: Simplified Parity Wallet code in SCIF.
  • ...and 11 more figures

Theorems & Definitions (1)

  • Definition 1: $\ell$-CDA Event