K-Michelson: a Case Study on Formal, Executable Language Specification (Part 1)

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:

  1. What an ideal programming language specification looks like.
  2. How this ideal framework powers nextgen program testing.

Continue reading

Runtime Verification and Algorand announce a new engagement to build formal tools for Algorand’s smart contract ecosystem

We are pleased to announce that Runtime Verification has been awarded a grant by Algorand Foundation to develop a formal semantic framework for Algorand’s smart contracts. The grant is part of its recently launched 250 Million ALGO Ecosystem Grants Program, a multi-year program that aims to support research and development of the Algorand ecosystem. We are very excited to have the opportunity to collaborate with Algorand in forming the future of Algorand’s smart contract architecture and supporting its growing community of developers. We have previously successfully completed a prior engagement with Algorand to formally model and verify safety of the platform’s consensus protocol, and we look forward to using the knowledge and experiences gained in this new engagement.

Continue reading

Formal Verification Framework for Michelson

Introduction

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.

Continue reading

Formally Verifying Finality in Gasper: The Core of the Beacon Chain

Musab A. Alturki, Elaine Li and Daejun Park

Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. A key component of Gasper is a finality mechanism that ensures durability of transactions and the continuous operation of the system even under attacks.

We are happy to report the successful completion of another major 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 formally proved key correctness properties of finality in Gasper and used these results to show that these properties also hold in an abstraction of Gasper’s implementation in the Beacon Chain. The models and proof scripts are all available online.

In this post, we focus on the first part of this achievement, which is verifying Gasper’s properties. So what’s Gasper? How are its properties formally verified? And why is this important?

Continue reading

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