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

Runtime Verification Enters a Protocol Verification Agreement with PlatON

Runtime Verification is excited to announce a new engagement with PlatON Networks, a privacy protecting new generation of public chain sponsored by LatticeX Foundation (Singapore). PlatON was forked from Ethereum, reborn with a brand new consensus algorithm and PlatON POS (proof of stake). The focus of this engagement is the formal modeling of PlatON’s Concurrent Byzantine Fault Tolerance (CBFT) protocol and verification of two mission critical properties - safety and liveness. The latter will likely be spread out over two different engagement phases.

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

Runtime Verification joins the Enterprise Ethereum Alliance

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.

Continue reading