Write Safer Smart Contracts

Susan Eisenbach
Sep 20 · 5 min read

Background

In April 2018 we posted an article on Medium introducing Flint, our Smart Contract Language designed to support the development of safer contracts. Since then much has happened, both in the smart contract world and with the development of Flint.

There have been numerous attacks on Ethereum smart contracts since our article. This is unfortunate, but confirms that smart contract programmers would greatly benefit from better development tools. We need confidence that smart contracts will not have unexpected outcomes.

There have been several new blockchains, many of which are programmed using pre-blockchain programming languages. More recently, Facebook has proposed a permissioned blockchain Libra and if it becomes successful it will be a real game changer.

Flint

Flint is being developed as an open source project on GitHub, and includes a language guide. One of its novelties is that the programmer needs to decide who can call which code before writing the actual code. This is done by using Flint’s Protection Blocks. Secondly, Flint has Assets for handling money and anything of value.

Protection Blocks: Smart contracts often carry out sensitive operations which need to be protected from unauthorised calls. A call can be unauthorised because the caller shouldn’t be allowed to make the call (e.g. only club administrators should be able to add new members), or because the contract is not in a valid state to execute the call (e.g. until you join a club you cannot participate in its activities). Flint requires programmers to think systematically about which users are allowed to call a smart contract’s functions, and what state the contract has to be in, before defining it.

Assets: Flint supports special operations for handling Assets such as Wei or Libra in smart contracts. Transfer operations are performed atomically, and ensure that the state of a contract is always consistent. In particular, Assets in Flint cannot be accidentally created, duplicated, or destroyed, but they can be atomically split, merged, and transferred to other Asset variables. Using Asset types avoids a class of vulnerabilities in which smart contracts’ internal state does not accurately represent their true balance.

Flint also has a range of programming language features well established to help with writing correct programs. Since contracts cannot be corrected, Flint type errors need to be found before contracts are released and so Flint has static type checking. Flint’s code is by default private and immutable. A programmer has to explicitly override either of these defaults. Integers do not wrap around, rather overflow causes an exception and contract execution terminates. The only loop construct is the for-in loop which is used to iterate over arrays, dictionaries and ranges. Contracts and structs must define public initialisers, and all state properties will be initialised during their execution. Flint’s fallback functions cannot change any state. Default fallback functions rollback the contract.

We have been working on giving Flint an ecosystem to support programmers, added verification to our compiler, and targeting the Libra blockchain.

Ecosystem

The modern programmer expects their tooling to be extensive and may not use a language if it lacks certain tools. Flint currently provides syntax highlighting support in several editors and IDE support in Vscode, including visualisation of contract structure and gas cost estimation. There is a mocking framework and a test framework. Flint also has an interactive console (REPL) and can use a third party local Ethereum blockchain.

Verification

Smart contracts handle money and any bugs in them cannot be fixed. So they have to be correct when they are placed on a blockchain. To date neither testing nor separate verification tools have been sufficient to prevent serious errors in blockchain contracts. The main problem with verification tools is not their functionality. Rather developers don’t always use them before releasing code onto a blockchain.

In addition to the Flint language design removing the possibilities of all kinds of errors we have added a verification pass to the compiler. Our pass provides two different capabilities. Firstly, it checks for common program errors such as out of bound array accesses and division by zero. Secondly, we have extended Flint with simple predicates for programmers to write specifications within their programs. In addition to assertions, Flint has contract invariants, function preconditions and postconditions. The specifications are checked at compile stage (using the intermediate verification language Boogie and the theorem prover Z3). The code snippet below contains an example invariant and postcondition.

contract Marking { 
var lecturer: Address
var markers: [Address]
var numMarkers: Int = 0
var grades: [Address: Int]
invariant(numMarkers == markers.size)
}
....Marking :: (markers) {
public func assignGrade(student: Address, grade: Int)
mutates (grades)
post
(forall (a, Address, dictContains(grades, a) ==>
(grades[a] == prev(grades[a]) ||
(a == student && grades[a] == grade)))
)
{
grades[student] = grade
}
}
....

Ethereum and Libra

Flint was designed to be a safe high level language for running on an Ethereum blockchain. It has many implicit assumptions that are Ethereum-based such as code is divided into contracts, functions can be declared as payable if one wants to transfer money to or from them, and code is rolled back if there are problems. The Ethereum language, Solidity, is object-oriented as is Flint (although it lacks inheritance).

Libra is quite different. Its intermediate language Move has modules rather than contracts and is not object-oriented; rather it has abstract data types. An important Move feature is its resources (think money). There can only be one copy of a resource. A resource can be moved between functions, but it no longer is accessible in the first function once it is moved. We have implemented a translation to Move. Move has a verification stage using the same technology we use, but currently its checks are quite constrained.

What’s next?

We see all three strands of our new work continuing. Installing a new version of Flint could be easier to do. Our ecosystem doesn’t have tools like Rust’s Cargo and Rustup and it should. We don’t have a debugger and we need to target popular IDEs.

Our verification pass does not yet deal with strings. Our specification constructs could be made more powerful.

Our Libra implementation targets the Move Intermediate Representation. However, Move has not yet been fully finalised; minor changes are currently being made on a weekly basis. There is a promise that Move will have collections and these are needed to translate Flint arrays.

Finally, and most importantly, we need people to test Flint by writing code. Only when real users use our language and tooling will we find ‘features’ we should change.

Flint is being developed by students in the research group of Professors Susan Eisenbach and Sophia Drossopoulou at the Department of Computing, Imperial College London. This work is supported by an Ethereum Foundation Wave 4 grant.

Please send us an email if you might want to work on the language or toolchain.

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade