A Formal Model in K of the Beacon Chain: Ethereum 2.0’s Primary Proof-of-Stake Blockchain

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?

Continue reading

The RV Bounded Model Checker – A lightweight semantics-based tool

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.

Continue reading

How Formal Verification Could Help to Prevent Gridlock Bug

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.

Continue reading

A Subtle Rust Bug

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.

Continue reading

Formal Verification of Ethereum 2.0 Deposit Contract (Part I)

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.

Continue reading

ERC777-K: Formal Executable Specification of ERC777

Denis Bogdanas and Daejun Park

ERC777

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.

Continue reading

Formal Verification of ERC20 Contracts

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).

Continue reading

How Formal Verification of Smart Contracts Works

Brian Marick and Daejun Park

Runtime Verification Inc provides Formal Smart Contract Verification services.

In this post, we'll describe – in general terms – the process of verifying a smart contract. Later posts in this series will provide more detail, contrast verification to other automated ways of increasing assurance, and cover other topics.

The pieces that matter for testing

Let's look at what any sort of verification has to work with, starting here:


The solidity compiler converts a smart contract into bytecodes

A smart contract is written in a programming language (commonly Solidity) and then translated into bytecodes. Once a smart contract is reduced to bytecodes, it can be deployed on the blockchain as a contract account at some address. An address is a huge number (for reasons irrelevant to this post.)

Continue reading

K Framework – An Overview

Why K

Unlike natural language, which allows interpretation and miscommunication, programming languages are meant to tell computers precisely what to do. Without a rigorous definition of a programming language that unambiguously says what each program does, also called a formal semantics, it is impossible to guarantee reliable, safe or secure operation of computing systems. K is a framework that allows you to define, or implement, the formal semantics of your programming language in an intuitive and modular way. Once you do that, K offers you a suite of tools for your language, including both an executable model and a program verifier.

Why Formal Semantics

Formal semantics of programming languages is a very old field of study, started long before many of us were born, in late 60's (Floyd-Hoare, or axiomatic semantics) to 70's (Scott-Strachey, or denotational semantics) and 80's (various types of operational semantics).

Unfortunately, formal semantics have a negative connotation among practitioners, who think that formal semantics of real programming languages are hard to define, difficult to understand, and ultimately useless. This is partly fueled by the fact that most formal semantics require a solid mathematical background to be understood and even more math to be defined, use cryptic notations that make little sense to non-logicians, such as backwards A and E symbols and a variety of Greek letters, and in the end sell themselves as "helping you better understand your language" and nothing else. Continue reading

K Framework Enables Verification of Smart Contracts

K-Framework-enables-verification-of-EVM

The age of cryptocurrency is here. A high percentage of cryptocurrency transactions are taking place on the Ethereum blockchain, which uses a computer program or “smart contract” to execute them. In December, Ethereum became the first cryptocurrency to amass one million transactions in a single 24-hour period.

However, any programming mistakes create openings for the theft of the virtual currency. While there are many safeguards to protect against security breaches, to date there hasn’t been a way to guarantee the formal verification of these contracts. For instance, last month hackers in Tokyo broke into the Coincheck, Inc. and stole $500 million in digtal tokens.

In a fruitful collaboration with Prof. Grigore Rosu's Formal Systems Laboratory (FSL) at UIUC, Runtime Verification (RV) has used the K framework to successfully build and test a mathematical model of the Etherem Virtual Machine, which makes it possible to formally verify the accuracy of smart contracts.
Continue reading