Write Safer Smart Contracts – Susan Eisenbach
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 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.
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.
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 ....Marking :: (markers)
}....
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 is (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, but this is preliminary work, since Move has not been finalised. Move has a verification stage using the same technology we use, but currently its checks are quite constrained.
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 so far we only provide IDE support for VSCode although it should be straightforward to target other 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 to Move. 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.
Published at Fri, 20 Sep 2019 15:56:36 +0000
Bitcoin Pic Of The Moment
✅ This image from Marco Verch (trendingtopics) is available under Creative Commons 2.0. Please link to the original photo and the license. 📝 License for use outside of the Creative Commons is available by request.
By trendingtopics on 2019-03-07 03:10:25
