Decoding Mythril's inputs

sunbeomso commented 4 years ago

Description

For full Solidity code and further details, please see How to Reproduce.

Mythril reported that totalSupply - _value in burn function may underflow (see below), and generated corresponding transactions below. I have decoded the input data of the last two transactions after the deployment as following:

"input": "0x79c65068ffffffffffffffffffffffffaffeaffeaffeaffeaffeaffeaffeaffeaffeaffeffffffffffffffffffffffffffffffffffffffffffffffffff",
"name": "mintToken(address,uint256)"
==> Decoded as: mintToken(0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe,1606938044258990275541962092341162602522202993782792835301375

"input": "0x42966c686d",
"name": "burn(uint256)",
==> Decoded as: burn(109)

I generated those transactions in my testnet and checked that if an underflow can occur in the burn function with the following code:

    function burn(uint256 _value) public returns (bool success) {                                                                                                                             
        require(balanceOf[msg.sender] >= _value);                                                                                                                                                                                                                                                              
        balanceOf[msg.sender] -= _value;                                                                                                                          
        assert (totalSupply  >=  _value); // I inserted this assertion to check the underflow when the exception occurs
        totalSupply -= _value;                                                                             
        Burn(msg.sender, _value);                                                                       
        return true; 
    }

However, these inputs fail to reproduce the underflow.

How to Reproduce

Testing file: https://etherscan.io/address/0xd1f55c30aa2f9e26c3ddf267ab61d3bd821f272a#code

My command:

sudo docker exec CONTAINER myth analyze /tmp/test.sol:Tracto --execution-timeout 1800 -o json --solv 0.4.25 -m integer,exceptions

Mythril's output (removed some parts irrelevant to this issue):

    "issues": [
        {
            "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
            "function": "burn(uint256)",
            "severity": "High",
            "swc-id": "101",
            "title": "Integer Underflow",
            "tx_sequence": {
                ...
                "steps": [
                    {
                        "address": "",
                        "calldata": "",
                        "input": "0x60806040526040805190810160405280600e81526020017f59756d657269756d20546f6b656e000000000000000000000000000000000000815250600190805190602001906200005192919062000175565b506040805190810160405280600381526020017f59554d0000000000000000000000000000000000000000000000000000000000815250600290805190602001906200009f92919062000175565b506008600360006101000a81548160ff021916908360ff160217905550600360009054906101000a900460ff1660ff16600a0a63302d4ba602600455348015620000e857600080fd5b50336000806101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600454600560003073ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000208190555062000224565b828054600181600116156101000203166002900490600052602060002090601f016020900481019282601f10620001b857805160ff1916838001178555620001e9565b82800160010185558215620001e9579182015b82811115620001e8578251825591602001919060010190620001cb565b5b509050620001f89190620001fc565b5090565b6200022191905b808211156200021d57600081600090555060010162000203565b5090565b90565b611c7880620002346000396000f300608060405260043610610128576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806306fdde031461012d578063095ea7b3146101bd57806318160ddd14610222578063184bd3941461024d57806323b872dd14610290578063313ce5671461031557806342966c6814610346578063611efc091461038b57806370a08231146103d857806379c650681461042f57806379cc67901461047c5780638da5cb5b146104e157806395d89b4114610538578063a9059cbb146105c8578063b414d4b614610615578063cae9ca5114610670578063d50a3d2c1461071b578063dd62ed3e14610768578063e4849b32146107df578063e724529c146107ff578063f2fde38b1461084e578063fffe088d14610891575b600080fd5b34801561013957600080fd5b506101426108e8565b6040518080602001828103825283818151815260200191508051906020019080838360005b83811015610182578082015181840152602081019050610167565b50505050905090810190601f1680156101af5780820380516001836020036101000a031916815260200191505b509250505060405180910390f35b3480156101c957600080fd5b50610208600480360381019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610986565b604051808215151515815260200191505060405180910390f35b34801561022e57600080fd5b50610237610a13565b6040518082815260200191505060405180910390f35b34801561025957600080fd5b5061028e600480360381019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610a19565b005b34801561029c57600080fd5b506102fb600480360381019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610ab8565b604051808215151515815260200191505060405180910390f35b34801561032157600080fd5b5061032a610be5565b604051808260ff1660ff16815260200191505060405180910390f35b34801561035257600080fd5b5061037160048036038101908080359060200190929190505050610bf8565b604051808215151515815260200191505060405180910390f35b34801561039757600080fd5b506103d6600480360381019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610cfc565b005b3480156103e457600080fd5b50610419600480360381019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610ef7565b6040518082815260200191505060405180910390f35b34801561043b57600080fd5b5061047a600480360381019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610f0f565b005b34801561048857600080fd5b506104c7600480360381019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611080565b604051808215151515815260200191505060405180910390f35b3480156104ed57600080fd5b506104f661129a565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b34801561054457600080fd5b5061054d6112bf565b6040518080602001828103825283818151815260200191508051906020019080838360005b8381101561058d578082015181840152602081019050610572565b50505050905090810190601f1680156105ba5780820380516001836020036101000a031916815260200191505b509250505060405180910390f35b3480156105d457600080fd5b50610613600480360381019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291908035906020019092919050505061135d565b005b34801561062157600080fd5b50610656600480360381019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505061136c565b604051808215151515815260200191505060405180910390f35b34801561067c57600080fd5b50610701600480360381019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190803590602001908201803590602001908080601f016020809104026020016040519081016040528093929190818152602001838380828437820191505050505050919291929050505061138c565b604051808215151515815260200191505060405180910390f35b34801561072757600080fd5b50610766600480360381019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291908035906020019092919050505061150f565b005b34801561077457600080fd5b506107c9600480360381019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611709565b6040518082815260200191505060405180910390f35b6107fd6004803603810190808035906020019092919050505061172e565b005b34801561080b57600080fd5b5061084c600480360381019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291908035151590602001909291905050506117ab565b005b34801561085a57600080fd5b5061088f600480360381019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506118d0565b005b34801561089d57600080fd5b506108a661196e565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b60018054600181600116156101000203166002900480601f01602080910402602001604051908101604052809291908181526020018280546001816001161561010002031660029004801561097e5780601f106109535761010080835404028352916020019161097e565b820191906000526020600020905b81548152906001019060200180831161096157829003601f168201915b505050505081565b600081600660003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506001905092915050565b60045481565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff16141515610a7457600080fd5b80600760006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff16021790555050565b6000600660008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020548211151515610b4557600080fd5b81600660008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008282540392505081905550610bda848484611994565b600190509392505050565b600360009054906101000a900460ff1681565b600081600560003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205410151515610c4857600080fd5b81600560003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008282540392505081905550816004600082825403925050819055503373ffffffffffffffffffffffffffffffffffffffff167fcc16f5dbb4873280815c1ee09dbd06736cffcc184412cf7a71a0fdb75d397ca5836040518082815260200191505060405180910390a260019050919050565b600760009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff16141515610d5857600080fd5b80600560003073ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205410151515610da657600080fd5b80600560003073ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000206000828254039250508190555080600560008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020600082825401925050819055508173ffffffffffffffffffffffffffffffffffffffff167fc6851889326b4ff916523ef06f539b4cf0b81d78fc6e0f97c30e6223d1831990826040518082815260200191505060405180910390a28173ffffffffffffffffffffffffffffffffffffffff163073ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef836040518082815260200191505060405180910390a35050565b60056020528060005260406000206000915090505481565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff16141515610f6a57600080fd5b80600560008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008282540192505081905550806004600082825401925050819055503073ffffffffffffffffffffffffffffffffffffffff1660007fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef836040518082815260200191505060405180910390a38173ffffffffffffffffffffffffffffffffffffffff163073ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef836040518082815260200191505060405180910390a35050565b600081600560008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054101515156110d057600080fd5b600660008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054821115151561115b57600080fd5b81600560008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000206000828254039250508190555081600660008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008282540392505081905550816004600082825403925050819055508273ffffffffffffffffffffffffffffffffffffffff167fcc16f5dbb4873280815c1ee09dbd06736cffcc184412cf7a71a0fdb75d397ca5836040518082815260200191505060405180910390a26001905092915050565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60028054600181600116156101000203166002900480601f0160208091040260200160405190810160405280929190818152602001828054600181600116156101000203166002900480156113555780601f1061132a57610100808354040283529160200191611355565b820191906000526020600020905b81548152906001019060200180831161133857829003601f168201915b505050505081565b611368338383611994565b5050565b60086020528060005260406000206000915054906101000a900460ff1681565b60008084905061139c8585610986565b15611506578073ffffffffffffffffffffffffffffffffffffffff16638f4ffcb1338630876040518563ffffffff167c0100000000000000000000000000000000000000000000000000000000028152600401808573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018481526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200180602001828103825283818151815260200191508051906020019080838360005b8381101561149657808201518184015260208101905061147b565b50505050905090810190601f1680156114c35780820380516001836020036101000a031916815260200191505b5095505050505050600060405180830381600087803b1580156114e557600080fd5b505af11580156114f9573d6000803e3d6000fd5b5050505060019150611507565b5b509392505050565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff1614151561156a57600080fd5b80600560003073ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054101515156115b857600080fd5b80600560003073ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000206000828254039250508190555080600560008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020600082825401925050819055508173ffffffffffffffffffffffffffffffffffffffff167fc6851889326b4ff916523ef06f539b4cf0b81d78fc6e0f97c30e6223d1831990826040518082815260200191505060405180910390a28173ffffffffffffffffffffffffffffffffffffffff163073ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef836040518082815260200191505060405180910390a35050565b6006602052816000526040600020602052806000526040600020600091509150505481565b61175a336000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1683611994565b3373ffffffffffffffffffffffffffffffffffffffff167f5e5e995ce3133561afceaa51a9a154d5db228cd7525d34df5185582c18d3df09826040518082815260200191505060405180910390a250565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff1614151561180657600080fd5b80600860008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060006101000a81548160ff0219169083151502179055507f48335238b4855f35377ed80f164e8c6f3c366e54ac00b96a6402d4a9814a03a58282604051808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001821515151581526020019250505060405180910390a15050565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff1614151561192b57600080fd5b806000806101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff16021790555050565b600760009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60008273ffffffffffffffffffffffffffffffffffffffff16141515156119ba57600080fd5b80600560008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205410151515611a0857600080fd5b600560008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205481600560008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205401111515611a9657600080fd5b600860008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060009054906101000a900460ff16151515611aef57600080fd5b600860008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060009054906101000a900460ff16151515611b4857600080fd5b80600560008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000206000828254039250508190555080600560008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020600082825401925050819055508173ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef836040518082815260200191505060405180910390a35050505600a165627a7a723058202d4d706814a2a056ab527a8823298eefeb1621c07bfeb0b153d27e1495b0ca5f0029",
                        "name": "unknown",
                        "origin": "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe",
                        "value": "0x0"
                    },
                    {
                        "address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
                        "calldata": "0x79c65068ffffffffffffffffffffffffaffeaffeaffeaffeaffeaffeaffeaffeaffeaffeffffffffffffffffffffffffffffffffffffffffffffffffff",
                        "input": "0x79c65068ffffffffffffffffffffffffaffeaffeaffeaffeaffeaffeaffeaffeaffeaffeffffffffffffffffffffffffffffffffffffffffffffffffff",
                        "name": "mintToken(address,uint256)",
                        "origin": "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe",
                        "value": "0x0"
                    },
                    {
                        "address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
                        "calldata": "0x42966c686d",
                        "input": "0x42966c686d",
                        "name": "burn(uint256)",
                        "origin": "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe",
                        "value": "0x0"
                    }
                ]
            }
        },

Expected behavior

My second transaction (burn(109)) is supposed to be reverted, but I couldn't get any failures. Regarding decoding, I double-checked possible mistakes with two abi-decoders:

Two decoders output exactly the same result I reported.

Could you check if there is anything I missed?

Environment

Mythril version: v 0.21.21 (from docker image)
Solidity compiler and version: 0.5.12
Python version: 3.6.9 (the one installed in the docker container)
OS and Version: Ubuntu 18.04 (Host OS)

norhh commented 4 years ago

You missed taking the padding into account for burn(), it’s not 109, it’s a huge number as mythril ignores padding the right hand side

sunbeomso commented 4 years ago

@norhh

Does Mythril "never" pad zeros?
Given only Mythril's non-padded inputs, is it always possible to decode Mythril's inputs correctly? I think there may be some ambiguous cases, e.g., multiple arguments or non-fixed sized array cases.
If the correct decoding is always possible, could recommend a way to do it?

norhh commented 4 years ago

In case of multiple args mythril pads everything except the last input. If the correct decoding is always possible, could recommend a way to do it? Just check the size of the last chunk, if it's not the size of an int256 then pad it to that.

sunbeomso commented 4 years ago

@norhh

Thank you for explaining it.

Just check the size of the last chunk, if it's not the size of an int256 then pad it to that.

What if some previous (which is not located in the last chunk) chunks have dynamic types?

sunbeomso commented 4 years ago

@norhh

In case of multiple args mythril pads everything except the last input.

Does Mythril always pad with '0', or does it sometimes pad with 'f'?

In the below example, the address type argument is ffffffffffffffffffffffffaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe, i.e., input[8:8+64]. It seems that Mythril padded with 'f', not '0'.

"input": "0x79c65068ffffffffffffffffffffffffaffeaffeaffeaffeaffeaffeaffeaffeaffeaffeffffffffffffffffffffffffffffffffffffffffffffffffff",
"name": "mintToken(address,uint256)"
==> Decoded as: mintToken(0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe,1606938044258990275541962092341162602522202993782792835301375

norhh commented 4 years ago

It seems that Mythril padded with 'f', not '0'. That can't exactly be called as padding,it's just some solution. Does Mythril always pad with '0', or does it sometimes pad with 'f'? I mean the 0 padding at the end.

norhh commented 4 years ago

What if some previous (which is not located in the last chunk) chunks have dynamic types? That shouldn't matter, excluding the function signature if the output len() isn't divisible by 64 then it should be padded with 0s to make it divisible.

sunbeomso commented 4 years ago

@norhh Thanks, I will try.

Consensys / mythril