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.

Why formalize?

At both RV and FSL, we believe strongly in a semantics-first approach to language development. This semantics-first approach means establishing a rigorous, mathematically formal, and human-readable definition of a programming language early in development. We believe this approach has several advantages.

The image above highlights this approach: first, core language semantics are developed for programming languages like C, Javascript, Java, EVM, and Viper. Then, a language independent framework (in this case the K Framework) takes these semantics as input and generates a range of useful tools, including interpreters (such a fast EVM interpreter was described in our KEVM work), static and dynamic analysis tools, deductive verifiers, and model checkers.

In short, we do not believe it is desirable to cater such tools directly to the target language. The target language may change, requiring frequent changes to the surrounding tools and introducing massive inefficiencies. Language-specific tools may also bake in language-specific hacks or shortcuts that are often difficult to understand or detect. And, language-specific tools require the duplication of core language-independent infrastructure across projects, a major inefficiency in software quality tool development.

Our semantics-first approach, on the other hand, allows for an executable (can be used as an interpreter) semantics to evolve with the language, providing the above tools through a language-independent semantic framework and allowing the reuse of such core tool infrastructure across programming languages and language versions. This approach also provides developers with an interpreter usable as a reference implementation for testing and compiler development, and provides a clear human-readable yet precise language definition that can be independently useful.

We believe the creation of such formal tools from our semantics of Viper will be practically useful towards developing sophisticated analysis and verification tools that directly bolster smart contract rigor and security, an obvious gain for the Ethereum community and all smart-contract enabled blockchains.

Why Viper?

There are several reasons that we've chosen Viper as a target of formalization. They include:

1. Potential for widespread use on the Ethereum platform and network: As a proponent of cutting edge formal verification techniques and tools, we want to deploy our technology where it will make an impact. There is no question that the best opportunity in the smart contract space is currently the Ethereum network, which has seen widespread adoption and use. We are excited to contribute cutting edge tools to the Ethereum community featuring the latest in aircraft-grade formal verification.
2. Security-first design: Viper is designed with security in mind, prioritizing security, auditability, and simplicity over ease of use, efficiency, or other convenience features for developers. We believe that languages must be designed for security first in the smart contract ecosystem, and the emphasis on simplicity means that we can quickly develop useful tools.
3. Novelty: Viper is a brand new, experimental language still rapidly evolving and very much in the initial design phases. We believe formalizing such a language early will allow the language designers to add features that make verification, program reasoning, and semantic definitions more efficient while encouraging good practices in the development of early contracts based on this language.

Overall, we are incredibly excited about the future of Viper in smart contract development and verification and the opportunity to build a principled and secure smart contract programming language, and look forward to building rigorous guarantees and usable tools for Viper smart contracts.

Artifacts and work plan

As part of this new Viper-based project, the following work is planned:

1. 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.
   Useful artifacts: Verified ERC20 token code, reusable and extensible core ERC20 property proofs for EVM-level tokens, the first formally verified Viper smart contract.
2. Jan 15, 2018: Prove EVM-level equivalence of the Viper and Solidity bytecode in the Solidity-compatible example above using the KEVM semantics (performing appropriate modifications when they're not equivalent, and potentially even fixing bugs in the two compilers). Then create and release tools for the community to create their own such proofs. Once this EVM-level equivalence infrastructure is in place, for both Solidity and Viper, we plan to also propose a test-suite to its release cycle that proves equivalence of any EVM output that has changed between versions on identical programs.
   Useful artifacts: Assurance for both Viper and Solidity ERC20 code for compiler/programmer-error freedom, Solidity and Viper compiler tests that ensure no examples output incompatible bytecode in minor releases, general framework for proving EVM contract equivalence.
3. Feb 1, 2018: Give a formal K semantic to Viper, like we did with the many other languages enumerated including EVM. Repeat the Viper ERC20 proofs from (1) at the Viper/source code level (the previous proofs target EVM).
   Useful artifacts: ERC20 specifications at both the EVM and Viper level, a formal model of Viper usable for testing / as an interpreter.
4. Mar 1, 2018: Define a (not necessarily optimal) translator from Viper to EVM using K, to serve as a foundation for validating external Viper-to-EVM compilers. Indeed, its output (EVM programs) can be compared with the output of the external compilers using the equivalence checker described at 2 above.
   Useful artifacts: Viper compiler tests proving the correct behavior of the Python viper compiler, test-case generation for the Viper compiler (potentially). Annotation language for Viper contract proofs, allowing developers to easily annotate desired properties without writing complex specifications.

We reserve the right to make changes to this schedule as we receive input from the community and the stakeholders in this project, including the developers of Viper. We are aiming for maximum utility and impact for the Ethereum community, and will iterate rapidly to see what works and where we can apply this semantics-based technology effectively.

We will also be in close contact with the Viper team and developers, providing any feedback that we believe useful to enhancing the security of contracts built on Viper, making Viper easier to model, or making Viper contracts easier to verify.

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.

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!

We will also be posting updates on our brand new Twitter page @rv_inc, which we hope any interested developers will follow and interact with.

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

Acknowledgment

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