In a previous post, we introduced the K-Michelson project, a formal verification framework for Michelson smart contracts, and described our overall project goals. In this two-part series, we will investigate:
- What an ideal programming language specification looks like.
- How this ideal framework powers nextgen program testing.
Runtime Verification Inc. (RV) is pleased to announce that we are partnering with the Tezos Foundation via the Tezos Ecosystem Grants program to develop a formal verification framework for the Michelson smart contract language! From its inception, the Tezos blockchain was designed with convenience, security, and extensibility in mind. However, unlike the status quo of predecessor technologies like Bitcoin, the true vision of a thriving Tezos ecosystem is more than just a secure digital currency exchange―it is a platform for developing and publishing distributed applications via smart contracts using its smart contract language Michelson. To fully realize this vision, Michelson smart contract developers will require tooling that enables them to confidently write and test smart contracts.
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.