Consensys / mythril

Security analysis tool for EVM bytecode. Supports smart contracts built for Ethereum, Hedera, Quorum, Vechain, Rootstock, Tron and other EVM-compatible blockchains.
https://mythx.io/
MIT License
3.84k stars 736 forks source link

`-o jsonv2` head and tail #865

Closed rocky closed 5 years ago

rocky commented 5 years ago

Description

Using -o jsonv2 I see that the head and tail descriptions are not quite right:

$ $MYTH -t1 -o jsonv2 -x tokensalechallenge.sol  | json_pp
{
   "sourceFormat" : "evm-byzantium-bytecode",
   "issues" : [
      {
         "extra" : {},
         "description" : {
            "tail" : "The binary multiply operation can result in an integer overflow.\n",
            "head" : "The multiply can overflow."
         },
         "locations" : [
            {
               "sourceMap" : "432:1:0"
            }
         ],
         "swcID" : "SWC-101",
         "swcTitle" : "Integer Overflow and Underflow",
         "severity" : "High"
      }
   ],
   "meta" : {},
   "sourceType" : "raw-bytecode",
   "sourceList" : [
      "0x8a4475692da568ed931a2d787cdec347d03ce3009f377dd69e5514763355e675"
   ]
}

Solidity code is:

/*
 * @source: https://capturetheether.com/challenges/math/token-sale/
 * @author: Steve Marx
 */

pragma solidity ^0.4.21;

contract TokenSaleChallenge {
    mapping(address => uint256) public balanceOf;
    uint256 constant PRICE_PER_TOKEN = 1 ether;

    function TokenSaleChallenge(address _player) public payable {
        require(msg.value == 1 ether);
    }

    function isComplete() public view returns (bool) {
        return address(this).balance < 1 ether;
    }

    function buy(uint256 numTokens) public payable {
        require(msg.value == numTokens * PRICE_PER_TOKEN);

        balanceOf[msg.sender] += numTokens;
    }

    function sell(uint256 numTokens) public {
        require(balanceOf[msg.sender] >= numTokens);

        balanceOf[msg.sender] -= numTokens;
        msg.sender.transfer(numTokens * PRICE_PER_TOKEN);
    }
}

Expected behavior

head text should be the tail text and the tail text can be the empty string.

Are there other situations like this?

Additional Environment or Context

$ git log
commit 2b668a7a4fd31bb36608ffa2da9b53c7d810d5e0 (HEAD -> enhance/844, origin/enhance/844)
muellerberndt commented 5 years ago

I changed this as follows:

         "description" : {
            "head" : "The binary multiplication can overflow.",
            "tail" : "The operands of the multiplication operation are not sufficiently constrained. The multiplication could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
         },

Does that make sense?

rocky commented 5 years ago

Thanks this is great.

JoranHonig commented 5 years ago

Closing this because @b-mueller's change should be in #852