ERC777-K: Formal Executable Specification of 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.
Foreseeing the massive adoption of this new token standard by the community in the near future, we at Runtime Verification have specified ERC777-K, a mathematically rigorous formalization of ERC777, to facilitate formal verification of potential ERC777 token implementations. Specifically, it is a formal executable semantics of ERC777, being parameterized by the implementation-dependent behaviors to admit all standard-conforming implementations. In the process of the formalization, we made sure that all corner cases are thought through, explicitly covered, and thoroughly tested. We also discovered a number of ambiguities in the standard which we documented and delivered to the authors of ERC777. From here on, when we claim that we prove implementations of ERC777 tokens correct, we mean that they provably satisfy the rules of ERC777-K.
Why K
We have chosen K as a semantic framework for our formalization effort for several reasons.
First, K is executable. So the defined semantic models can be tested to find early errors in their design and to accumulate confidence in their adequacy.
Second, K provides a suite of formal analysis tools that can be used in combination with any semantics:
Thus, we can use K to verify that a token contract satisfies the ERC777 specification, and also verify properties about the ERC777 specification itself (e.g., "the total supply is not changed by applications of ERC777 send operations").
Third, K is modular. This allows us to compositionally define semantics for execution environments or programming languages on top of ERC777-K, giving the feel of "plug-and-play ERC777 into your favorite language". Moreover, once done, we can then verify complex programs in the resulting languages.
Fourth, K is under active development and we have control over its design and implementation, so it can quickly respond to future needs of ERC777-K.
Highlights of ERC777-K
ERC777-K is parametric in addresses, values, and maxvalue. This way it can be easily instantiated to various target execution environments besides EVM, such as eWASM or IELE, and to various programming languages besides Solidity, such as Vyper or Plutus.
ERC777-K is also parametric in the implementation-dependent behaviors. It can be easily instantiated to admit any standard-conforming implementation besides the reference implementation. This means that ERC777-K can be quickly used to verify any potential ERC777 implementation. For example, according to the ERC777 standard, if someone sends tokens to another who has no receiver hook (i.e., a callback function) registered, the token contract can freely choose to either accept or revert the send operation. We designed ERC777-K to be easily configured to have either behavior by adjusting configuration parameters. Indeed, we considered all possible parameter combinations when testing ERC777-K. (We will get to that below.)
Furthermore, ERC777-K is parametric in the execution environment. It can be plugged-and-played within any execution environment which has a formal semantics, such as a virtual machine or a programming language. The ERC777 functions are simply added to the target VM/language's syntax, and the ERC777 semantics smoothly composes with the VM/language's semantics, yielding a variant of the VM/language with ERC777 support. We have done that with a simple imperative language, IMP. The video below shows an interactive program in IMP that calls the ERC777 functions. This can be easily adapted to language implementations, where ERC777 can be regarded as a library.
ERC777-K is executable. This not only allows us to elegantly integrate it with programming languages (as mentioned above), but also allows us to test it. Indeed, like code, a formal specification can also have errors, especially when there is no other formal specification to formally compare with. Unlike code, which can be verified against a specification, there is nothing we can do to prove a formal specification correct: since it serves as a definition, it is correct by definition. The best we can do is to accumulate confidence in its correctness, by various means. One of the most tangible means is to test it. To this end, we provide more than 200 unit tests for our ERC777 semantics; these can be easily translated to tests for implementations of ERC777. These tests can serve as a conformance test suite to check if different ERC777 implementations converge on the standard. The conformance test is critical to prevent divergent behaviors across different implementations that are potential security vulnerabilities for any token clients assuming consistent behavior across ERC777 implementations, and we believe this will help to establish a more principled token contract development practice.
Technical Details and Download
ERC777-K is thoroughly commented and freely available under the UIUC license (as permissive as the MIT license) on Github:
Comments and contributions are highly appreciated.
Get involved
All software is released under the 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 examples and tests. 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!
Follow us on Twitter @rv_inc for news and updates.
Acknowledgments
We thank Fabian Vogelsteller, Jordi Baylina, and Jacques Dafflon for their support and help with understanding the standard.
