by Stephen Skeirik
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:
- What an ideal programming language specification looks like.
- How this ideal framework powers nextgen program testing.
In this first part, we limit our focus to question (1). So, what should an ideal programming language specification look like? Several properties come to mind:
- Clarity: it should be unambiguous and straightforward.
- Completeness: It should be self-contained and describe how all possible programs execute.
- Testability: arbitrary programs should be executable against the specification to see whether their actual and intended results agree. …
by Musab A. Alturki
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. …
by Stephen Skeirik
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. …
by 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. …
by Rikard Hjort
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.
We want Ewasm to have a specification that you can run your smart-contract with. We have a prototype implementation of Ewasm that we have began using to verify an Ewasm contract with, which we are blogging about.
It is still early days, and right now we want to ramp up and make the prover more powerful, and the tools more accessible for early adopters. …
by Rikard Hjort and Stephen Skeirik
Welcome to the final installment in the series on formal verification brought to you by Runtime Verification and dlab. If you missed the first three parts, you can find them here:
- Introducing KWasm, and an intro to symbolic execution
- An intro to Formal Verification using WebAssembly (Wasm)
- Verifying a more complex Wasm function
This time around, we’ll be picking up the baton right where we left off as we explore how to verify programs written in Ethereum-flavored Wasm, or Ewasm. In particular, we are going to verify a function for querying the balance of an ERC20-type smart contract.
Ewasm is part of the Ethereum 2.0 roadmap. We expect to see people starting to write prototype smart contracts in Ewasm soon, and later real smart contracts, handling real money. There are other blockchains already using Wasm as a smart contract language, and even as a client language, for example by writing smart contracts in Rust. Wasm smart contracts are coming, and we are preparing our Wasm verification tools to be more powerful. And, we want to show you how to use them, and what features we are adding as we go along. …
by Stephen Skeirik
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.
The Long Road from English to Logic
English is the lingua franca of modern business. For that reason, unsurprisingly, we often write our requirements as simple English text documents. Unfortunately, for formal verification purposes, English language documents are far too imprecise and typically gloss over important implementation details. For this reason (as we will see later), we typically want a formal verification expert to help us rewrite our English language requirements document into a formal and mathematical requirements specification. For example, suppose we are designing a smart contract that implements an open bid auction. …
by Stephen Skeirik
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.
The question proponents of blockchain systems must ask themselves is: how can we salvage (a) the promise of blockchain technology for building a new class of distributed systems as well as (b) its reputation in the eyes of a wary public? Clearly, this is a multi-faceted issue that cannot be fully deconstructed in a single article. However, in this series we will argue that formal verification (more on that below) will play an increasing role answering both of these challenges (a)-(b). …
by Daejun Park
We, at Runtime Verification, are happy to report our successful completion of formal verification of the Ethereum 2.0 deposit contract, arguably one of the most important smart contracts to be deployed this year for the Ethereum community.
Deposit Contract
The deposit contract is a gateway to join Ethereum 2.0. To be validators who drive the entire Proof-of-Stake (PoS) chain, called Beacon chain, of Ethereum 2.0, you need to deposit a certain amount of Ether, as a “stake”, by sending a transaction (over the Ethereum 1.x network) to the deposit contract. The deposit contract records the history of deposits, and locks all the deposits in the Ethereum 1.x chain, which can be later claimed at the Beacon chain of Ethereum 2.0. Note that at an early stage of Ethereum 2.0, the deposit contract is a one-way function; you can move your funds from Ethereum 1.x to Ethereum 2.0, …
by Rikard Hjort and Stephen Skeirik
This blog post is the second in a series of posts written by Runtime Verification, Inc. and sponsored by dlab on web assembly (Wasm), and more specifically KWasm, a tool for doing formal verification of Wasm programs. If you missed the first post, feel free to take a look!
Today, we will be finishing our mini-series on exploring how to verify a fragment of the WRC20 contract, i.e., a Wasm implementation of the Ethereum smart contract ERC20, which provides an API for token exchange that is usable by other kinds of smart contracts (e.g., digital wallets). …
About
