The Gitcoin Grant
We launched a Gitcoin Grant to help us build KWasm and KEwasm, executable semantics and formal verification tools for Ethereum 2.0, written in the K framework.
K tools blur the line between specification and implementation. The code is human-readable and a great reference for understanding Wasm and Ewasm, but it also generates a correct-by-construction interpreter.
In this second part of our four part series, we will discuss the process of formalizing system requirements and how it fits into the larger context of formal verification for blockchain systems and smart contracts.
Recall that formal verification is all about knowing whether our system implementation (e.g., blockchain system/smart contract), satisfies our system requirements.
Today’s article is about the process of converting our requirements document into an equivalent formal, mathematical requirements specification.
Blockchain technology coupled with smart contracts offers a tantalizing promise: enabling distributed, trusted, and verifiable computational platforms for applications with rigorous security requirements like finance, secure messaging, and more. Unfortunately, one does not have to look very hard to see that the path to this promise is fraught with danger, e.g., see articles on Mt. Gox, the DAO, this attack on Ethereum classic, and a smart contract bug. While blockchain systems may be sound in theory, in practice, blockchain systems and smart contracts are still highly prone to developer error.
We, at Runtime Verification, are happy to report our successful completion of formal verification of the Ethereum 2.0 deposit contract, arguably one of the most important smart contracts to be deployed this year for the Ethereum community.
Smart contract failures can cost millions of dollars and can even lead to death of companies and of cryptocurrencies. Moreover, smart contracts are easier to attack by hackers than ordinary software, simply because they are public on the blockchain and anyone can invoke them from anywhere. Therefore, there is an unprecedented need to guarantee the correctness of code.
It is well-known that the only way to guarantee code correctness is through the use of rigorous formal methods, where the correctness of the smart contract is expressed mathematically as a formal property, the programming language or virtual machine is also expressed mathematically as a formal model, and the former is rigorously proved from the latter. Moreover, the correctness of smart contracts must be independently checkable, without having to trust their authors or any auditing authorities. Therefore, they must be provided with machine checkable correctness certificates.
Yet another smart contract bug
Recently, a hidden DoS bug (called Gridlock) was revealed in Edgeware's Lockdrop smart contract that has locked hundreds of millions of dollars worth of Ether. Because of this bug, Edgeware had to newly deploy the fixed version of the contract, and as a result, two Lockdrop contracts (old version and new version) currently live in parallel on mainnet. (This means that you can send a transaction to either of these contracts to lock your Ether, until the old one is attacked and becomes incapable.)
In this article, we will review the Gridlock bug and discuss how formal verification can help to prevent this type of bugs.
Ethereum 2.0 is coming. And rest assured, it will be formally specified and verified!
Ethereum 2.0 is a new sharded PoS protocol that, at its early stage (called Phase 0), lives in parallel with the existing PoW chain (called Eth1 chain). While the Eth1 chain is powered by miners, the new PoS chain (called Beacon chain) will be driven by validators.
In February of this year Runtime Verification, Inc, (RV) received the very first security grant from the Ethereum Foundation to formally model/specify and verify the Casper smart contract.
Denis Bogdanas and Daejun Park
The ERC777 standard is a new token standard, designed to be an alternative to the ERC20 standard, improving usability by giving account holders more control over token transactions, while keeping backward compatibility with ERC20. It defines an "operator" who can be thought of as a (trusted) third party to whom an infinite amount of "allowances" is approved to spend on behalf of the token owner. It also introduces the concept of a "hook", a callback function that is triggered when an operator performs a token transfer. The hook can either accept or reject the token transfer, allowing the token holders to have a finer-grained control of delegating the token transfer to operators. This hook can be also used to notify the token holders that they have received tokens, which is an important feature missed in ERC20.
Brian Marick and Daejun Park
Runtime Verification Inc provides Formal Smart Contract Verification services.
The previous post explained the overall process of formally verifying a smart contract. It wasn't enough, though, to let you imagine what you'd work with as you did the work. This post expands on the previous one using the recent experience of one of us (Park), who verified several implementations of the ERC-20 standard written to run on the Ethereum Virtual Machine (EVM).