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 ERC-20 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

IELE: A New Virtual Machine for the Blockchain

IELE and K Team
Runtime Verification (RV) is proud to release their first version of IELE, a new virtual machine for the blockchain.

IELE Team Photo, left to right: Daejun Park (PhD student at UIUC, RV intern); Theodoros Kasampalis (PhD student at UIUC, RV intern); Yi Zhang (PhD student at UIUC, RV intern); Traian Serbanuta (RV; screen, left bottom); Grigore Rosu (RV president/CEO and UIUC professor; screen, center, taking the picture); Virgil Serbanuta (RV; screen, right bottom); David Young (RV); Brandon Moore (RV); Yiyi Wang (RV); Dwight Guth (RV).

Continue reading

RV Inc. & FSL @ UIUC Release First Formal Viper Tools

Taming the Viper

Runtime Verification, Inc. (RV) along with the Formal Systems Lab at the University of Illinois (FSL) have announced a joint initiative targeting the full formalization of the Viper smart contract programming language, using the K Framework to create a full formal definition of this research-oriented smart contract programming language. This effort is intended to yield a number of useful tools and artifacts, and to lay the foundation for the future of principled and formally rigorous smart contract development. Today, we are happy to announce the release of our first round of fully formal tools for review to the Ethereum community.

Continue reading

ERC20-K: Formal Executable Specification of ERC20

ERC20
The ERC20 standard is one of the most important standards for the implementation of tokens within Ethereum smart contracts. ERC20 provides basic functionality to transfer tokens and to be approved so they can be spent by another on-chain third party. Unfortunately, ERC20 leaves several corner cases unspecified, which makes it less than ideal to use in the formal verification of token implementations. Indeed, we at RV, Inc., have been asked to verify smart contracts for ERC20 compliance. However, we found that it is unclear what ERC20 compliance means, because the existing presentations of ERC20 are far from serving as mathematical models of the standard token. Consequently, we decided to create ERC20-K, a mathematically rigorous formalization of ERC20, making sure that all corner cases are thought through, explicitly covered, and thoroughly tested. From here on, when we claim that we prove implementations of ERC20 tokens correct, we mean that they provably satisfy the 13 rules of ERC20-K.

Continue reading

New Technologies for the Blockchain: IELE (virtual machine) and K (universal language framework)

IELE and K Team Runtime Verification has been recently awarded a research and development contract by IOHK to design a next generation virtual machine and a universal language framework to be used as core infrastructure for future blockchain technologies. The formal analysis and verification technology employed in this project has been developed and improved over more than 15 years of research and development, both in the Formal System Laboratory (FSL) at the University of Illinois at Urbana-Champaign and at Runtime Verification, with generous funding from organisations including NSF, NASA, DARPA, NSA, Boeing, Microsoft, Toyota, and Denso. It is about time that aircraft grade, software analysis technology used for mission critical software gets deployed to smart contracts, the blockchain and cryptocurrencies. The project will be executed by a team of Runtime Verification experts led by Prof. Rosu, who will work closely with students at the University of Illinois, also funded by IOHK, and with IOHK R&D personnel. IELE and K Team Photo, left to right: Daejun Park (PhD student at UIUC, RV intern); Theodoros Kasampalis (PhD student at UIUC, RV intern); Yi Zhang (PhD student at UIUC, RV intern); Traian Serbanuta (RV; screen, left bottom); Grigore Rosu (RV and UIUC; screen, center, taking the picture); Virgil Serbanuta (RV; screen, right bottom); David Young (RV); Brandon Moore (RV); Yiyi Wang (RV); Dwight Guth (RV). Also Chris Hathhorn (RV), who missed picture.

Continue reading

RV Inc. & FSL @ UIUC to Formalize Ethereum’s Viper

Runtime Verification, Inc. (RV) along with the Formal Systems Lab at the University of Illinois (FSL) are announcing a joint initiative targeting the full formalization of the Viper smart contract programming language, using the K Framework to create a full formal definition of this research-oriented smart contract programming language. We believe this effort will yield a number of useful tools and artifacts, and can lay the foundation for the future of principled and formally rigorous smart contract development.

Continue reading