runtimeverification / erc20-semantics

ERC20 in K

ERC20-K: Formal Executable Specification of ERC20

Author: Grigore Rosu

Date: 6 December 2017

Abstract

The ERC20 standard is one of the most important standards for the implementation of tokens within Ethereum smart contracts. ERC20 provides basic functionality to transfer tokens and to be approved so they can be spent by another on-chain third party. Unfortunately, ERC20 leaves several corner cases unspecified, which makes it less than ideal to use in the formal verification of token implementations. ERC20-K is a complete formal specification of the ERC20 standard. Specifically, it is a formal executable semantics of a refinement of the ERC20 standard, using the K framework.

ERC20-K clarifies what data (accounts, allowances, etc.) are handled by the various ERC20 functions and the precise meaning of those functions on such data. ERC20-K also clarifies the meaning of all the corner cases that the ERC20 standard omits to discuss, such as transfers from yourself to yourself or transfers that result in arithmetic overflows, following the most natural implementations that aim at minimizing gas consumption.

Being executable, ERC20-K can also be tested for increased confidence. Driven by the semantic rules that form ERC20-K, as well as by their side conditions, we manually but systematically produced and provide a test-suite consisting of several dozens of tests which we believe cover all the corner cases. We encourage you to analyze these tests and use them to test your implementations. Please contribute with more tests if you think that we left any interesting behaviors uncovered.

Motivation

KEVM makes it possible to rigorously verify smart contracts at the Ethereum Virtual Machine (EVM) level against higher level specifications. The most requested property to verify so far was correctness of ERC20 tokens written in languages like Solidity or Viper. But what does "correctness of ERC20 tokens" really mean? When formal verification is sought, a property (or specification) that the code must satisfy must be available. Moreover, such a specification should be unambiguous and capable of answering all the questions regarding corner-case behaviors. To our knowledge, there was no such formal specification for ERC20, or for ERC20 variants, available at the time of this writing (December 2017).

The existing ERC20 specifications are either too informal to serve as a formal specification for verification purposes, or they are not executable, incomplete and use unnecessarily advanced logical formalisms. For example, the Ethereum wiki and github variants are rather informal and imprecise, in spite of being called formalized by a coindesk article, and so are the ERC20 descriptions by McDonald, Seibel, McKie, etc., as well as the Stackoverflow explanations. On the other hand, when actual formalizations as a mathematical theory were attempted, such as McRainface's, they are paper-based (i.e., not executable) and using logical formalisms that are hard to understand by most developers, such as linear logic.

Structure

The main ERC20-K specification is defined and extensively commented in this file:

• erc20.md

The following folder contains unit tests for the ERC20-K specification, that is, small programs that exercise the various ERC20 functions in various contexts. For that, a programming language needs to be first defined on top of ERC20-K:

• tests

Contribute

We welcome contributions! The easiest way to contribute is to add more tests to existing languages in the folder tests. A more involved way to contribute is to add new languages under tests, together with their own unit tests. It would be nice to cover a variety of language paradigms, such as more imperative language, object-oriented, functional, and even logical programming languages. Finally, you can adopt ERC20-K as the standard specification of ERC20 when testing and verifying smart contracts and this way: (1) we as a community converge on one formal standard for token correctness, as opposed to each group having different versions and opinions about what correctness means, most likely missing some corner cases and thus allowing vulnerabilities; and (2) we as a community improve the test suite, for the benefit of us all.

Acknowledgments

We thank the K team who defined the KEVM semantics (see technical report, too) and verified smart contracts for ERC20 compliance. It is their effort that inevitably led to the quest for a formal specification of ERC20. In particular, we would like to thank Philip Daian for brainstorming and help with understanding the corner cases of ERC20.

We also warmly thank IOHK not only for their generous funding support of both KEVM and IELE, but also for the stimulating technical discussions we had with their research team. Discussions about IELE and about the planned separation between the settlement and the computational layers in Cardano, in particular, led to the question of whether the ERC20 specification can be defined in a more abstract way that makes it usable in combination with computational layers different from EVM.

erc20-semantics's Issues

kompile error！

zch@ubuntu:~/erc20-semantics-k5/tests/imp$ kompile imp.k
ocamlc: unknown option '-match-context-rows'.
usage: ocamlfind ocamlc [options] file ...
-package Refer to package when compiling
-linkpkg Link the packages in
-predicates

Add predicate

when resolving package properties
-dontlink Do not link in package and its ancestors
-syntax

Use preprocessor with predicate

-ppopt Append option to preprocessor invocation
-ppxopt , Append options to ppx invocation for package
-dllpath-pkg Add -dllpath for this package
-dllpath-all Add -dllpath for all linked packages
-ignore-error Ignore the 'error' directive in META files
-passopt Pass option directly to ocamlc/opt/mklib/mktop
-passrest Pass all remaining options directly
-only-show Only show the constructed command, but do not exec it
STANDARD OPTIONS:
-a Build a library
-absname Show absolute filenames in error messages
-annot Save information in .annot
-bin-annot Save typedtree in .cmt
-c Compile only (do not link)
-cc Use as the C compiler and linker
-cclib Pass option to the C linker
-ccopt Pass option to the C compiler and linker
-compat-32 Check that generated bytecode can run on 32-bit platforms
-config Print configuration values and exit
-custom Link in custom mode
-custom Link in custom mode
-dllib Use the dynamically-loaded library
-dllpath

Add to the run-time search path for shared libraries
-dtypes (deprecated) same as -annot
-for-pack Generate code that can later be `packed' with
ocamlc -pack -o .cmo
-g Save debugging information
-i Print inferred interface
-I Add to the list of include directories
-impl Compile as a .ml file
-intf Compile as a .mli file
-intf-suffix Suffix for interface files (default: .mli)
-intf_suffix (deprecated) same as -intf-suffix
-keep-docs Keep documentation strings in .cmi files
-keep-locs Keep locations in .cmi files
-labels Use commuting label mode
-linkall Link all modules, even unused ones
-make-runtime Build a runtime system with given C objects and libraries
-make_runtime (deprecated) same as -make-runtime
-modern (deprecated) same as -labels
-no-alias-deps Do not record dependencies for module aliases
-no-app-funct Deactivate applicative functors
-no-check-prims Do not check runtime for primitives
-noassert Do not compile assertion checks
-noautolink Do not automatically link C libraries specified in .cma files
-nolabels Ignore non-optional labels in types
-nostdlib Do not add default directory to the list of include directories
-o Set output file name to
-open Opens the module before typing
-output-obj Output an object file instead of an executable
-output-complete-obj Output an object file, including runtime, instead of an executable
-pack Package the given .cmo files into one .cmo
-pp Pipe sources through preprocessor
-ppx Pipe abstract syntax trees through preprocessor
-principal Check principality of type inference
-rectypes Allow arbitrary recursive types
-runtime-variant Use the variant of the run-time system
-safe-string Make strings immutable
-short-paths Shorten paths in types
-strict-sequence Left-hand part of a sequence must have type unit
-strict-formats Reject invalid formats accepted by legacy implementations
(Warning: Invalid formats may behave differently from
previous OCaml versions, and will become always-rejected
in future OCaml versions. You should use this flag
to detect and fix invalid formats.)
-thread Generate code that supports the system threads library
-unsafe Do not compile bounds checking on array and string access
-unsafe-string Make strings mutable (default)
-use-runtime Generate bytecode for the given runtime system
-use_runtime (deprecated) same as -use-runtime
-v Print compiler version and location of standard library and exit
-verbose Print calls to external commands
-version Print version and exit
-vmthread Generate code that supports the threads library with VM-level
scheduling
-vnum Print version number and exit
-w Enable or disable warnings according to :
+ enable warnings in
- disable warnings in
@ enable warnings in and treat them as errors
can be:
a single warning number
.. a range of consecutive warning numbers
a predefined set
default setting is "+a-4-6-7-9-27-29-32..39-41..42-44-45-48-50"
-warn-error Enable or disable error status for warnings according
to . See option -w for the syntax of .
Default setting is "-a"
-warn-help Show description of warning numbers
-where Print location of standard library and exit

• Treat as a file name (even if it starts with `-')
  -nopervasives (undocumented)
  -use-prims (undocumented)
  -dsource (undocumented)
  -dparsetree (undocumented)
  -dtypedtree (undocumented)
  -drawlambda (undocumented)
  -dlambda (undocumented)
  -dinstr (undocumented)
  -help Display this list of options
  --help Display this list of options
  [Error] Critical: ocamlopt returned nonzero exit code: 2
  Examine output to see errors.
  [Warning] Compiler: Could not find main syntax module with name IMP-SYNTAX in
  definition. Use --syntax-module to specify one. Using IMP as default.
  [Warning] Compiler: missing entry for hook BAG.concat
  [Warning] Compiler: missing entry for hook BAG.element
  [Warning] Compiler: missing entry for hook BAG.unit

Cannot compile

Hi
First of all thanks for creating this!

I've tried compiling erc20.k but it fails with the following message:

[Error] Compiler: Could not find sorts: [Bool]
	Source(/mount/erc20.k)
	Location(16,19,16,22)

Any help would be much appreciated. Thanks

Detail

Installed k-framework using docker

Created a container, copied erc20.k and ran

k-distribution/target/release/k/bin/kompile /mount/erc20.k 

Log

root@21880d35cb6b:/k# k-distribution/target/release/k/bin/kompile /mount/erc20.k 

WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$2 (file:/k/k-distribution/target/release/k/lib/java/guice-4.0-beta5.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of com.google.inject.internal.cglib.core.$ReflectUtils$2
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
[Error] Compiler: Could not find sorts: [Bool]
	Source(/mount/erc20.k)
	Location(16,19,16,22)