KWasm and KEwasm: executable semantics and formal verification tools for Ethereum 2.0

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.

Continue reading

Formal Verification 101 for Blockchain Systems and Smart Contracts: Formalizing Requirements

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.

Continue reading

Formal Verification 101 for Blockchain Systems and Smart Contracts

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.

Continue reading

K vs. Coq as Language Verification Frameworks (Part 3 of 3)

Musab A. Alturki and Brandon Moore

This is the third and last part of the “K vs. Coq as Language Verification Frameworks” post series. After illustrating how the syntactic structures of a language are defined (Part 1), and how its semantics can be defined and tested (Part 2) in both K and Coq, we now describe how the third step in the verification workflow, which is specifying and verifying correctness properties, can be achieved. We use the same working example SUM and assume all the language definitions of IMP and SUM described in the previous parts.

Continue reading

K vs. Coq as Language Verification Frameworks (Part 2 of 3)

Musab A. Alturki and Brandon Moore

In Part 1 of this post, we began by generally introducing the steps needed to verify the correctness of programs in a language verification framework, such as K and Coq. We then described how the first step, defining language syntax and program structure, can be accomplished in both K and Coq for our working example program SUM in the language IMP, highlighting the main differences between the two frameworks.

In this second part of the post, we build on the definitions introduced in the previous part and describe how the semantics of the language and testing the semantics, the second step in the process, can be achieved in K and Coq using the same example SUM. Part 3 of the series explains how the third step (specifying and verifying properties) can be done.

Continue reading

K vs. Coq as Language Verification Frameworks (Part 1 of 3)

Musab A. Alturki and Brandon Moore

Formally verifying programs, like verifying smart contracts in blockchain systems or verifying airplane flight controllers in embedded devices, is a powerful technique for assuring correctness and increasing reliability of systems. In this context, the question of “Why use K as opposed to Coq?” seems to come up quite often when discussing K with colleagues who may not be familiar with K, but have heard about or used Coq before. In this series of posts, we make an attempt at highlighting some of the important ways in which K and Coq differ as formal verification frameworks for languages through a working example. We hope to convey to the reader why we believe K is more suitable in this context. Before we continue, we’d like to note that we have extensive experience with Coq, both as users and as library/framework developers.

Continue reading

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