Skip to content

Latest commit

 

History

History
120 lines (82 loc) · 20.6 KB

README.md

File metadata and controls

120 lines (82 loc) · 20.6 KB
Raw

2018-03-12

Formal Verification of DSToken ERC20 Token Contract

We present a formal verification of DSToken ERC20 token contract.

The DSToken ERC20 token is a high-profile ERC20 token contract written in Solidity by DappHub.

We found that the DSToken ERC20 token deviates from the ERC20-K (and thus ERC20-EVM) specification as follows:

  • Stoppable modifier: The transfer, transferFrom and approve functions are defined with the stoppable modifier (inherited from DSStop). The stoppable modifier ensures that the function will throw an exception if the stopped variable is set to true by authorized users.

Target Smart Contract

The target contract of our formal verification has the following Solidity source code, taken from the Github repository https://github.com/dapphub/ds-token at commit bb98ff:

We formally verified the full functional correctness of the following ERC20 functions:

Verification Artifacts

Solidity Source Code and Compiled EVM Bytecode

We took the source code of DSToken and DSTokenBase with the additional libraries DSAuth, DSMath, DSStop and DSNote, and compiled it to the EVM bytecode using the solc compiler (version 0.4.18+commit.9cf6e910.Linux.g++).

The EVM (runtime) bytecode generated by the solc compiler is the following:

The (annotated) EVM assembly disassembled from the bytecode is the following:

Mechanized Specifications and Proofs

Due to its deviation from ERC20-K, we could not verify the DSToken ERC20 token against the original ERC20-EVM specification. In order to show that it is "correct" w.r.t. ERC20-K (thus ERC20-EVM) modulo the deviation, we modified the specification to capture the deviation and successfully verified the contract against the modified ERC20-EVM specification. Below are the changes made to the original ERC20-EVM specification:

  • To capture the stoppable modifier for transfer, transferFrom and approve, we added the following entry in storage:

    #hashedLocation({COMPILER}, {_STOPPED}, .IntList) |-> #packed(STOPPED, OWNER)

    We have also added the following required condition (i.e., stopped being false) for the success cases:

    andBool STOPPED ==Int 0

    and its complement (i.e., stopped being true) for the failure cases:

    andBool STOPPED ==Int 1

The full changes made in ERC20-EVM are shown in here. The specifications of other functions except transfer, transferFrom and approve are the same as the original ERC20-EVM.

We took the modified ERC20-EVM specification and instantiated it with the program-specific parameters shown below.

[pgm]
compiler: "Solidity"
_supply: 0
_balances: 1
_allowances: 2
_stopped: 4
code: "0x60606040526004361061011d576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806306fdde031461012257806307da68f514610153578063095ea7b31461016857806313af4035146101c257806318160ddd146101fb57806323b872dd14610224578063313ce5671461029d5780633452f51d146102c65780635ac801fe1461033257806369d3e20e1461035957806370a082311461038e57806375f12b21146103db5780637a9e5e4b146104085780638402181f146104415780638da5cb5b146104ad57806390bc16931461050257806395d89b4114610537578063a9059cbb14610568578063be9a6555146105c2578063bf7e214f146105d7578063dd62ed3e1461062c575b600080fd5b341561012d57600080fd5b610135610698565b60405180826000191660001916815260200191505060405180910390f35b341561015e57600080fd5b61016661069e565b005b341561017357600080fd5b6101a8600480803573ffffffffffffffffffffffffffffffffffffffff1690602001909190803590602001909190505061079e565b604051808215151515815260200191505060405180910390f35b34156101cd57600080fd5b6101f9600480803573ffffffffffffffffffffffffffffffffffffffff16906020019091905050610878565b005b341561020657600080fd5b61020e610957565b6040518082815260200191505060405180910390f35b341561022f57600080fd5b610283600480803573ffffffffffffffffffffffffffffffffffffffff1690602001909190803573ffffffffffffffffffffffffffffffffffffffff16906020019091908035906020019091905050610960565b604051808215151515815260200191505060405180910390f35b34156102a857600080fd5b6102b0610a3c565b6040518082815260200191505060405180910390f35b34156102d157600080fd5b610318600480803573ffffffffffffffffffffffffffffffffffffffff169060200190919080356fffffffffffffffffffffffffffffffff16906020019091905050610a42565b604051808215151515815260200191505060405180910390f35b341561033d57600080fd5b610357600480803560001916906020019091905050610a68565b005b341561036457600080fd5b61038c60048080356fffffffffffffffffffffffffffffffff16906020019091905050610aac565b005b341561039957600080fd5b6103c5600480803573ffffffffffffffffffffffffffffffffffffffff16906020019091905050610c6d565b6040518082815260200191505060405180910390f35b34156103e657600080fd5b6103ee610cb6565b604051808215151515815260200191505060405180910390f35b341561041357600080fd5b61043f600480803573ffffffffffffffffffffffffffffffffffffffff16906020019091905050610cc9565b005b341561044c57600080fd5b610493600480803573ffffffffffffffffffffffffffffffffffffffff169060200190919080356fffffffffffffffffffffffffffffffff16906020019091905050610da8565b604051808215151515815260200191505060405180910390f35b34156104b857600080fd5b6104c0610dcf565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b341561050d57600080fd5b61053560048080356fffffffffffffffffffffffffffffffff16906020019091905050610df5565b005b341561054257600080fd5b61054a610fb6565b60405180826000191660001916815260200191505060405180910390f35b341561057357600080fd5b6105a8600480803573ffffffffffffffffffffffffffffffffffffffff16906020019091908035906020019091905050610fbc565b604051808215151515815260200191505060405180910390f35b34156105cd57600080fd5b6105d5611096565b005b34156105e257600080fd5b6105ea611196565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b341561063757600080fd5b610682600480803573ffffffffffffffffffffffffffffffffffffffff1690602001909190803573ffffffffffffffffffffffffffffffffffffffff169060200190919050506111bc565b6040518082815260200191505060405180910390f35b60075481565b6106cc336000357fffffffff0000000000000000000000000000000000000000000000000000000016611243565b15156106d457fe5b60008060043591506024359050806000191682600019163373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19163460003660405180848152602001806020018281038252848482818152602001925080828437820191505094505050505060405180910390a46001600460146101000a81548160ff0219169083151502179055505050565b6000600460149054906101000a900460ff161515156107b957fe5b60008060043591506024359050806000191682600019163373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19163460003660405180848152602001806020018281038252848482818152602001925080828437820191505094505050505060405180910390a461086e85856114a4565b9250505092915050565b6108a6336000357fffffffff0000000000000000000000000000000000000000000000000000000016611243565b15156108ae57fe5b80600460006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff167fce241d7ca1f669fee44b6fc00b8eba2df3bb514eed0f6f668f8f89096e81ed9460405160405180910390a250565b60008054905090565b6000600460149054906101000a900460ff1615151561097b57fe5b60008060043591506024359050806000191682600019163373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19163460003660405180848152602001806020018281038252848482818152602001925080828437820191505094505050505060405180910390a4610a31868686611596565b925050509392505050565b60065481565b6000610a6083836fffffffffffffffffffffffffffffffff16610fbc565b905092915050565b610a96336000357fffffffff0000000000000000000000000000000000000000000000000000000016611243565b1515610a9e57fe5b806007816000191690555050565b610ada336000357fffffffff0000000000000000000000000000000000000000000000000000000016611243565b1515610ae257fe5b600460149054906101000a900460ff16151515610afb57fe5b60008060043591506024359050806000191682600019163373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19163460003660405180848152602001806020018281038252848482818152602001925080828437820191505094505050505060405180910390a4610c01600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054846fffffffffffffffffffffffffffffffff166118f9565b600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550610c62600054846fffffffffffffffffffffffffffffffff166118f9565b600081905550505050565b6000600160008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020549050919050565b600460149054906101000a900460ff1681565b610cf7336000357fffffffff0000000000000000000000000000000000000000000000000000000016611243565b1515610cff57fe5b80600360006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff167f1abebea81bfa2637f28358c371278fb15ede7ea8dd28d2e03b112ff6d936ada460405160405180910390a250565b6000610dc78333846fffffffffffffffffffffffffffffffff16610960565b905092915050565b600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b610e23336000357fffffffff0000000000000000000000000000000000000000000000000000000016611243565b1515610e2b57fe5b600460149054906101000a900460ff16151515610e4457fe5b60008060043591506024359050806000191682600019163373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19163460003660405180848152602001806020018281038252848482818152602001925080828437820191505094505050505060405180910390a4610f4a600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054846fffffffffffffffffffffffffffffffff16611912565b600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550610fab600054846fffffffffffffffffffffffffffffffff16611912565b600081905550505050565b60055481565b6000600460149054906101000a900460ff16151515610fd757fe5b60008060043591506024359050806000191682600019163373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19163460003660405180848152602001806020018281038252848482818152602001925080828437820191505094505050505060405180910390a461108c858561192b565b9250505092915050565b6110c4336000357fffffffff0000000000000000000000000000000000000000000000000000000016611243565b15156110cc57fe5b60008060043591506024359050806000191682600019163373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19163460003660405180848152602001806020018281038252848482818152602001925080828437820191505094505050505060405180910390a46000600460146101000a81548160ff0219169083151502179055505050565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b6000600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054905092915050565b60003073ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff161415611282576001905061149e565b600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff1614156112e1576001905061149e565b600073ffffffffffffffffffffffffffffffffffffffff16600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff161415611341576000905061149e565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663b70096138430856000604051602001526040518463ffffffff167c0100000000000000000000000000000000000000000000000000000000028152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001827bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff191681526020019350505050602060405180830381600087803b151561148057600080fd5b6102c65a03f1151561149157600080fd5b5050506040518051905090505b92915050565b600081600260003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff167f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925846040518082815260200191505060405180910390a36001905092915050565b600081600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054101515156115e357fe5b81600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015151561166b57fe5b6116f1600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205483611912565b600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506117ba600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205483611912565b600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550611846600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836118f9565b600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef846040518082815260200191505060405180910390a3600190509392505050565b6000828284019150811015151561190c57fe5b92915050565b6000828284039150811115151561192557fe5b92915050565b600081600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015151561197857fe5b6119c1600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205483611912565b600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550611a4d600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836118f9565b600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef846040518082815260200191505060405180910390a360019050929150505600a165627a7a72305820fb55366ece8a4477c9397b20e007129a3014819c6fb99d9f51c9903e245fadbc0029"
gasCap: 100000

The resulting specification is the following:

The specification is written in eDSL, a domain-specific language for EVM specifications, which must be known in order to thoroughly understand our EVM-level specification. Refer to resources for background on our technology. The above file provides the eDSL specification template parameters. The full K reachability logic specification is automatically derived by instantiating a specification template with these template parameters.

Run the following command in the root directory of this repository to generate the full specification under the directory specs/ds-token-erc20:

$ make ds-token-erc20

Run the EVM verifier to prove that the specification is satisfied by (the compiled EVM bytecode of) the target functions. See these instructions for more details of running the verifier.

Resources

Disclaimer