Flint

The project goal was to prevent programmers for the Ethereum Virtual Machine (EVM) from writing insecure code, by implementing novel type specifications and compiler-enforced constraints.

I started working on the Flint Programming Language in 2018, as part of a first-year summer undergraduate research opportunity, under the supervision of Professors Susan Eisenbach and Sophia Drossopoulou. Its original developer was Franklin Schrans for his MEng thesis. He introduced novel concepts such as “Caller Protection”, which allowed for static and runtime checks on originating callers of a particular function, and “Asset Traits” which semantically prevent creation ex-nihilo or implicit destruction. In addition, Arithmetic operations on Int are safe by default: an overflow/underflow causes the Ethereum transaction to be reverted.

Caller Protections

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

// State declaration
contract Bank {
  var manager: Address
}

// Functions are declared in protection blocks,
// which specifies which users are allowed to call them.
Bank :: (manager) { // manager is a state property.

  // Only the `manager` of the Bank can call `clear`.
  func clear(address: Address) {
    // body
  }
}

// Anyone can initialize the contract.
Bank :: (any) {
  public init(manager: Address) {
    self.manager = manager
  }
}

Next Steps

The challenge posed when I joined was to:

1. Expand the novel features to cover other broad categories of vulnerabilities
2. Implement sufficient “standard” features to make the language usable in practice (for example, I implemented: for loops, subscript type checking, address literals, nested arrays and dictionaries, and allowing for lazy caller protection with function-based caller checks).

The primary focus however was on the novel features. I implemented and designed several new features, including:

• Attempt Calls
• Type States
• Event Framework: Removed the confusion between approve() (the function call) and Approval() (the event emission). This was a common source of confusion for programmers due to their near-identical format, and enforcing a unique type and usage only with log clarified these two use cases. For instance: log Approval(from: caller, to: spender, value: value)
• Traits & Assets (e.g. Asset Traits): Generalizing the existing concept of “Asset Traits” into “Traits” which describe partial behaviour of contracts or structures, and “Assets” which are traits with compiler-guaranteed properties of no unprivileged creation/destruction, and safe internal/external transfers.

Type States

Type States integrate a design pattern of stateful contracts into the language itself, which both require programmers to think about what state a function can be called in and also to prevent vulnerabilities (e.g. Parity Multi-Sig wallet) from mistakes concerning administrating state. States are checked statically for internal calls (unlike Solidity modifiers), and at runtime for calls originating from external contracts.

// Enumeration of states.
contract Auction (Preparing, InProgress) {}

Auction @(Preparing, InProgress) :: caller <- (any) {
  public init() {
    // ...
    become Preparing
  }
}

Auction @(Preparing) :: (beneficiary) {
  public func setBeneficiary(beneficiary: Address) mutates (beneficiary) {
    self.beneficiary = beneficiary
  }

  func openAuction() -> Bool {
    // ...
    become InProgress
  }
}

Attempt Calls

In the EVM, functions can call to an external ‘contract’ implicitly hand over control flow. This external code has no guarantees of functionality and can be malicious or fail silently. Attempt calls allow the programmer to explicitly specify how to handle responses (for instance call! causes a transaction rollback on an error), and limit the versatility of calls (preventing external contracts from re-entering the current contract’s functions which leads to unforeseen control flow exploits).

Wallet :: (any) {
  public func forcefulWithdraw() -> Optional<Bool> {
    try! withdraw()
    // withdraw did not fail
    return true
  }

  public func awareWithdraw() -> Bool {
    let successful: Bool = try? withdraw()
    // withdraw has no state impact when it fails and returns False
    return successful
  }
}

Asset Traits

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 ensures 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
   func deposit(implicit value: inout Wei) mutates (balances) {
    // Omitting this line causes a
    // compiler warning: the value received should be recorded.
    balances[address].transfer(&value)
  }

  func withdraw() mutates(account, balances) {
    // balances[account] is automatically set to 0 before transferring.
    send(account, &balances[account])
  }
}