Musab A. Alturki, Denis Bogdanas, Chris Hathhorn and Daejun Park
With the upcoming major update to version 2.0 (code-named Serenity), Ethereum is transitioning into a sharded, proof-of-stake (PoS) consensus mechanism. It brings better energy-efficiency, security and scalability. The specific PoS protocol of Ethereum 2.0 is known as the Beacon Chain.
We are happy to report the first milestone in an ongoing collaboration between Runtime Verification and Ethereum Foundation, to build a formal framework for modeling and verifying the Beacon Chain. We have completed the executable formal model of Beacon Chain in the K Framework. The K specification, along with the technical report describing this work, are both available online.
So what’s the Beacon Chain? How was its model in K developed? Why is this development important?
Runtime Verification, a premium provider of formal verification services announced that it has joined the Enterprise Ethereum Alliance (EEA), the defacto standards organization for enterprise blockchain – one that is backed by the largest developer community in the world and a worldwide member-base.
As a member of the EEA, Runtime Verification will collaborate with industry leaders in pursuit of Ethereum-based enterprise technology best practices, open standards, and open-source reference architectures.
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.
Here at Runtime Verification, we are spending time developing and improving tools for the K Framework. In particular, one of the projects I have been working on is a new execution engine for concrete execution of programs in K semantics, which compiles to LLVM.
Because we compile to LLVM, we are able to make use of code in any programming language that targets LLVM. In particular, we use Rust for the portion of the runtime which handles operations over lists, maps, and sets.
Yesterday I discovered a very subtle bug in our Rust code which was causing our tests to fail. It was affecting the hash algorithm we use for maps and sets, which in turn caused a map lookup operation to fail even though the key it was supposed to look up was in fact in the map.
Musab A. Alturki, Brandon Moore, Karl Palmskog and Lucas Pena
Earlier this year, Runtime Verification was engaged by Algorand to verify its consensus protocol. We are happy to report that the first part of the effort, namely modeling the protocol and proving its safety theorem, has been successfully completed. Specifically, we have used a proof assistant (Coq) to systematically identify assumptions under which the protocol is mathematically guaranteed to not fork.
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.
At Runtime Verification, we are using Haskell to develop the next generation of formal verification tools based on the K Framework. This article describes how we use algebraic data types to write expressive Haskell code.
Bool represents a single bit of information:
data Bool = False | True
The popular term “boolean blindness” refers to the information lost by functions that operate on
Bool when richer structures are available. Erasing such structure can give code a bad smell. Using more structure can produce interfaces that are easier to document, use, decompose, and generalize.
Earlier this Fall, Runtime Verification opened a subsidiary in Bucharest, Romania. The new company, Runtime Verification SRL, is located in the heart of the capital city and already staffed by seven persons. The operation’s focus will be two-fold; support the development of the new K in Haskell, and deliver smart contract verification audits for clients building products and services for the Ethereum community and beyond. The founding team consists of Traian Serbanuta (co-inventor of the K-framework), Virgil Serbanuta, Denis Bogdanas, Vladimir Ciobanu, Denisa Diaconescu, Ana Pantilie, and Andrei Vacaru.
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.