IOHK: Virtual Machines and Contract Code Correctness

Ethereum 6 min, 29 sec READ

by Martin Banov

Taking a mission-critical approach to blockchain: bringing formal methods and functional programming to the decentralized world.

Ethereum is a programmable blockchain in that it enables users to structure all kinds of operations, not limiting them to a pre-defined set  (e.g., the Bitcoin blockchain only facilitates Bitcoin transactions). At its core is the Ethereum Virtual Machine (EVM) which is the runtime environment for Ethereum-based smart contracts (described in the yellow paper as a "transactional singleton machine with shared-state"). 

At any point, Ethereum nodes agree on a shared global state that is modified over time by transactions accepted into the blockchain. Contract accounts may contain code which is executed in the EVM in parallel by all nodes each time they receive a transaction. The EVM is fairly simple compared to a desktop or mobile operating system and a detailed diagram illustrating how EVM computations fit into blocks can be found here.

This "world computer" concept is the main idea behind Ethereum, but when a blockchain is equipped with a code executing VM shared across the whole network, it becomes critically important that any contract code deployed on the live network is not flawed or vulnerable and behaves as expected (given that large sums of money can be at stake). 

What Are Testnets?

When writing programs that target the EVM (Ethereum's contract code execution environment), one needs to pay for their deployment and (write) operations in gas. This cost fluctuates depending on network load and can at times be prohibitive as well as carrying financial risks given vulnerable or buggy code is deployed on the live network, as changes on the mainnet cannot be rolled back or undone and thus that creates a forever exploitable contract.

This is why testnets are extensively used in development on smart contract enabled blockchains. Testnets are duplicate testbeds of the blockchain and its execution environment (e.g., the Ethereum blockchain) except for that their Ether (or whatever native currency) is valueless. They are used for development purposes to provide safety layers for experimentation and performance assessment in a simulated environment before deploying any code on the live mainnet.

Public testnets are connected to the Internet and available to all. The following public testnets are available for Ethereum:

• Ropsten network closely resembles the mainnet, as Ether can be PoW mined or demanded through the Ropsten Faucet (a website providing free test Ether). 
• Kovan was launched by the Parity team and only works with the Parity node, in addition to using PoA (Proof-of-Authority) instead of PoW mining as its consensus mechanism. This means that only certain nodes are authorized to append blocks of validated transactions and one can only get Kovan Ether by requesting it from the dedicated faucets of such nodes. This makes it somewhat more reliable and resistant to spam attacks.
• Rinkeby shares the advantages of Kovan with two differences - there is no Parity support, it only works with the Geth client, and with a slightly modified PoA mechanism. Rinkeby Ether can be requested from an authorized faucet.

And, of course, one can always spin up a private local blockchain, with a Genesis file generated from which a client like Geth builds the chain. Private testnets are convenient for teamwork in closed environments that need to reproduce the working environment without exposing the network to the outside world.

Recently, the IOHK team have begun setting up a series of testnets for their iterative improvements of the EVM (that they will be launching throughout 2018), starting with KEVM - the first correct-by-construction formal schematic of the EVM, followed by its register-based version, IELE.

Input Output Hong Kong (IOHK)

IOHK is an engineering company committed to advancing peer-to-peer technologies and establishing industry standards in the realm of distributed ledger technologies. IOHK is particularly focused on formal methods that assure high standards of security and code correctness in software engineering and set to refining distributed systems engineering as a rigorous discipline grounded in mathematical proofs. Founded by Charles Hoskinson in 2015, IOHK works alongside with three different projects it is philosophically allied with - Cardano, Ethereum Classic and ZenCash.

K Framework: Virtual Machines and Universal Language for the Blockchain

K is a semantic framework used to design and develop programming languages and virtual machines. K basically allows one to define a language (i.e., the syntax and semantics) and assemble the needed tooling around it. IOHK makes extensive use of the K framework in formal analysis and constructing virtual machines for blockchain platforms. 

In their endeavors to improve upon the EVM and build a generic language framework that can be used as core infrastructure underpinning blockchain systems, IOHK are collaborating with Runtime Verification, a University of Illinois startup using formal verification-based techniques to improve the reliability of software systems. 

The K Framework allows you to automatically generate parser, compiler, interpreter, etc. from grammatical syntax and semantic definitions of a language in a way that is correct by construction.

Several languages have so far been given complete formal semantics in K, including C, Java, and JavaScript with Solidity and Plutus (Cardano's smart contracts language) actively developed. Just like JavaScript is contained in the browser, Solidity can be thought of as a being contained on the blockchain and targeting the EVM. 

KEVM: Formal Specification of the EVM

The first testnet IOHK launched on May 28th with the KEVM testnet, a correct-by-construction revamp of the Ethereum Virtual Machine (EVM) laid out in the K framework. KEVM essentially defines the EVM semantics in K, so it supports Ethereum executable applications while also ascertaining smart contract correctness.

Developers could take any EVM executable application and run it on the KEVM, using that to verify and prove that a smart contract executes as intended. This is done by formally specifying a contract’s attributes in K in conjunction with the KEVM specification and then verifying those properties using the K framework.

IELE: A Register-Based Virtual Machine That Can Run Solidity

IELE is an improved EVM-like virtual machine inspired from both LLVM and EVM and building upon the KEVM specification. IELE is collaboratively developed with IOHK and Runtime Verification, whose founder, Professor Grigore Rosu, has described the project as follows: 

IELE is the crown jewel of our research over the past decade, combining our experience in designing and formalizing many programming languages and virtual machines, with the latest, cutting-edge research in formal semantics and program analysis and verification.

“IELE is a critical component of a large-scale research and development project funded by IOHK, whose ultimate objective is to set, by example, a high standard for the third generation of cryptocurrencies in terms of scalability, security, and programmability.

A simple representation of a stack runtime with push and pop operations. A stack machine is a type of computer that operates on a stack of numbers rather than numbers in registers.

In contrast to the EVM itself, which is a stack-based machine, IELE is architected as a register-based machine that handles an unbounded number of registers and integers (so no need to worry about stack or arithmetic overflows any longer) in closely following the design rationale and representation of the LLVM. The performance improvements are to include efficient gas optimization model that is uniform across all languages and automated contract verification techniques. 

Summary

Many of the solutions developed by IOHK will ultimately be to the benefit of all blockchain-based smart contract platforms and bring an ecosystem closer together while also bridging collaboration between other professional communities and academia (e.g., the functional programming and formal methods communities). The high-security assurances provided by IOHK's methodology to software engineering should afford smart contracts the reliability needed for broader adoption among financial sectors, institutional settings, and academic institutions.