Flint: A New Language for Safe Smart Contracts on Ethereum

Background

Ethereum smart contracts (or DApps) have been the target of numerous attacks (TheDAO, Parity, KingOfTheEtherThrone, etc.), resulting in millions of dollars worth of Ether being locked or stolen. Vulnerabilities are often due to simple programmer errors, such as forgetting to write a keyword in a function signature. Static and dynamic analysis tools (Manticore, Mythril, Oyente, etc.) have been developed for Solidity—currently the most widely used language for writing smart contracts for Ethereum. These tools try to find some vulnerabilities before the contracts are deployed and cannot be updated.

Flint

Flint is a new statically-typed programming language for writing inherently safer smart contracts. Flint features a variety of novel contract-oriented features, such as caller capabilities, immutability by default, and Asset types, which help developers write smart contracts. The project is currently under active development. The short introductory paper Writing Safe Smart Contracts in Flint, gives a high-level overview of Flint and its motivations, and has been awarded the ACM SRC 1st Prize at <Programming> 2018.

Compiler and Documentation

The Flint compiler is under development and is open-source on GitHub. Documentation and instructions on how to get started with Flint is available in The Flint Programming Language Guide.

Language Overview

The Flint Programming Language Guide gives a high-level overview of the language, and helps getting started with smart contract development in Flint.

Caller Capabilities

Caller capabilities require programmers to think about who should be able to call the contract’s sensitive functions. Capabilities are checked statically for internal calls (unlike Solidity modifiers), and at runtime for calls originating from external contracts.

Example:

// State declaration
contract Bank {
  var manager: Address
}
// Functions are declared in caller capability blocks,
// which specify which users are allowed to call them.
Bank :: (manager) {
  
  // Only `manager` of the Bank can call `clear`.
  func clear(address: Address) {
    // body
  }
}

Immutability by default

Restricting writes to state in functions helps programmers more easily reason about the smart contract. A function which writes to the contract’s state needs to be annotated with the mutating keyword.

Example:

Bank :: (any) {
  mutating func incrementCount() {
    // count is a state property
    count += 1
  }
 
  func getCount() -> Int {
    return count
  }
 
  func decrementCount() {
    // error: Use of mutating statement in a nonmutating function
    // count -= 1
  }
}

Asset types

Assets, such as Ether, are often at the center of smart contracts. Flint puts assets at the forefront through the special Asset trait.

Flint’s Asset type ensure a contract’s state always truthfully represents its Ether value, preventing attacks such as TheDAO.

A restricted set of atomic operations can be performed on Assets. It is impossible to create, duplicate, or lose Assets (such as Ether) in unprivileged code. This prevents attacks relating to double-spending and re-entrancy.

Example use:

Bank :: account <- (balances.keys) {
  @payable
  mutating func deposit(implicit value: inout Wei) {
    // Omitting the next line would cause a compiler warning:
    // the value received should be recorded.           
    balances[address].transfer(&value)
  }
}
 mutating func withdraw() {
   // balances[account] is automatically 
   // set to 0 before transferring.
   send(account, &balances[account])
 }
}

The Asset feature is still in development. The FIP-0001: Introduce the Asset trait proposal includes more details.

Safer semantics

In the spirit of reducing vulnerabilities relating to unexpected language semantics, such as wrap-arounds due to integer overflows, Flint aims to provide safer operations. For instance, arithmetic operations on Int are safe by default: an overflow/underflow causes the Ethereum transaction to be reverted.

What’s next

On top of finishing the implementation of the compiler, the long terms goals for Flint include:

1. Gas estimation: provide estimates about the gas execution cost of a function. Gas upper bounds are emitted as part of the contract’s interface, making it possible to obtain the estimation of a call to an external Flint function.
2. Formalization: specify well-defined semantics for the language.
3. The Flint Package Manager: create a package manager which runs as a Flint smart contract on Ethereum. It would store contract APIs as well as safety and gas cost information of dependencies.
4. Tooling: build novel tools around smart contract development, such as new ways of simulating and visualizing different transaction orderings.

The Flint Programming Language is developed by Franklin Schrans, Sophia Drossopoulou, and Susan Eisenbach from Imperial College London.