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

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.

An EVM translation semantics for Viper

One of the goals in our initial Viper work plan was a semantics of Viper defined as a translation from Viper to EVM:

Mar 1, 2018: Define a translator from Viper to EVM using K, to serve as a foundation for validating external Viper-to-EVM compilers.

We are proud to announce the early completion of this line of work, with a complete translation semantics of Viper available to download and use for smart contract authors. With this work, users can use a formally defined translation from Viper to LLL and from LLL to EVM to write smart contracts, compiling their Viper code to EVM with a simple Python command that provides a replacement for the native Viper compiler:

python3.6 kviper.py tests/examples/token/ERC20.v.py

(this is still an early, unaudited release and care should be taken with funds)

As we describe in our overview of the semantics, this work lead to the identification of over 16 bugs in the existing Viper implementation and compiler, one of which was a major security vulnerability with the potential to cause substantial loss of funds and confidence in the Viper language. As our overview notes, finding bugs through review in the process of formalizing a previously ad-hoc implementation is both expected and demonstrates the value of formal, peer-reviewed language models.

In addition to the practical value of formalizing Viper, we seek to improve the documentation of the language by providing formal syntax of Viper, updating the original BNF documentation provided by the language to a complete grammar usable for deriving a parser. Other useful related artifacts include a formal definition of LLL by translation to EVM, allowing developers to compile LLL to EVM through a mathematically complete and rigorous definition for the first time.

One of our stated goals in the formalization of Viper was to provide feedback to language designers, guiding the evolution of the language into a standards-bearing smart contract language informed by both strong design principles and a thorough design process. Towards this end, we have also submitted a Viper Improvement Proposal arguing for changes to Viper's scoping rules, enhancing auditability and clarifying important language rules for the development of Viper analysis tools. As we continue to work with Viper, we expect more such language design proposals to continue refining Viper into the simple, auditable, high-assurance language the needs of the smart contract development community demand.

EVM-Level Viper ERC20 specifications

Another goal in our Viper work plan concerned the creation of the first formally verified Viper contract, extending previous work we have done on verifying ERC20 properties to Viper:

Dec 1, 2017: Repeat our HKG proofs discussed in the KEVM technical report on the EVM code generated by Viper from its versions of ERC20 (with both Solidity-compatible and Viper-specific datatypes). Prove as many Viper ERC20 properties as possible, to serve as a mathematically rigorous, standalone description of the Viper ERC20.

To this end, we are happy to announce the release of our verified Viper ERC20 wrapped Ether contract, in which we verify the ERC20-compliance of a standard Viper token included in the default Viper distribution. While this is not a complete verification of these contracts in that we verify ERC20 compliance only, it represents an important stepping stone and proof of concept towards the use of K's Viper model and KEVM in the formal verification of Viper contracts. As explained in our original KEVM paper, despite its limited scope, the verification we perform is capable of exposing a wide range of bugs in ERC-compatible functions.

Because of the importance of the ERC20 standard to the general Ethereum ecosystem and cryptocurrency as a whole, we have also created a language-independent specification for ERC20, which generalizes the concept of a token beyond the EVM and Solidity-specific specification of ERC20. We intend to verify ERC20-compliance of tokens using these high-level, language-independent rules, and are proceeding to repeat our Viper ERC20 verification using this comprehensive specification of required ERC20 behavior. We also plan on releasing this refinement of ERC20 as an EIP, allowing for continuity of the ERC20 standard across changes to the Ethereum virtual machine while removing the dependence of ERC20 on Solidity-specific constructs like the uint256 data type.

Future plans

Our remaining plans for the Viper project consist of three primary goals:

1. Integration: A great deal of work remains in integrating our above artifacts into the Ethereum Foundation's Viper distribution. This includes integration with CI tests and automated test infrastructure, including our formally-verified compiler in Viper's standard test suite and expanding this test suite for full coverage of both the formal Viper semantics and the Viper compiler implementation.
2. Independent Semantics: As explained in our original work plan, one major goal of the Viper formalization project is the creation of an independent semantics of Viper which does not require a translation to EVM, providing an EVM-independent specification of the language that can remain portable across updates to the virtual machine (including the planned transition to EWASM). We believe that such an independent semantics will provide a substantial boon to the practicality and generality of the Viper language while helping evaluate the impact of any changes to the underlying execution machinery (eg - EVM) on Viper programs.
   An independent semantics would also allow developers to write proofs without reasoning about EVM-specific constructs, like gas and exception behavior. Developers can reason about their program at a high level, over the abstract Viper model, with tools automatically generated from this independent semantics and the EVM semantics able to check that no EVM implementation details introduce unexpected behaviors into contract execution. We see this as a necessary step towards high assurance contract and language development, substantially simplifying reasoning about many smart contracts.
3. Equivalence: Our final planned artifact for the Viper project is an equivalence-checker for EVM programs, formally proving that two different EVM programs have equivalent behavior in all cases. This equivalence checker is useful for ensuring that Viper and Solidity are able to produce completely compatible code, lending assurance to the independently developed compilers of both languages. Also, this equivalence checker can be used in combination with the formal semantics of Viper in this post to extend the Viper test suite: for each program, the test suite can use both the K Viper semantics and the official Viper implementation to compile every program, proving them equivalent and providing further assurance of the correctness of both artifacts.

As we continue to make progress towards all of these three goals, we welcome community input, feedback, and discussion, and will continue to post updates on our blog and on our new Twitter page @rv_inc.

Get involved

In the spirit of open source, community-driven development, we will be holding all project discussions on our new K Framework Riot channels at #k:matrix.org.

All software is released under the MIT-like UIUC license, and will be totally free for the community to use as they see fit. We welcome contributions on Git, and look forward to feedback on our formally generated Viper compiler.

We encourage any interested parties to engage us, ask questions, contribute code, or build experience with our tools. We are also always looking for contributors able to work on documentation, efficient install/quickstart process for new developers, and more proof examples. We are hiring, and will be sure to keep an eye open for helpful contributors!

Let's build more secure smart contracts for everybody, together!

Acknowledgment

This research and development project was made possible by a grant from the Ethereum Foundation.