Posted on December 14, 2017 by Philip Daian
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.
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.
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.
Our remaining plans for the Viper project consist of three primary goals:
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.
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!
This research and development project was made possible by a grant from the Ethereum Foundation.