Merge pull request #375 from JoranHonig/bugfix/taint_active_account

Check on active account vs environment (which is shallow copied)

mythril/analysis/modules/exceptions.py

@@ -24,9 +24,7 @@ def execute(statespace):
         for state in node.states:
 
             instruction = state.get_current_instruction()
-
             if(instruction['opcode'] == "ASSERT_FAIL"):
-
                 try:
                     model = solver.get_model(node.constraints)
                     address = state.get_current_instruction()['address']

mythril/analysis/modules/integer.py

@@ -108,7 +108,6 @@ def _verify_integer_overflow(statespace, node, expr, state, model, constraint, o
 
     return _try_constraints(node.constraints, [Not(constraint)]) is not None
 
-
 def _try_constraints(constraints, new_constraints):
     """
     Tries new constraints

mythril/analysis/solver.py

@@ -4,7 +4,7 @@ import logging
 
 def get_model(constraints):
     s = Solver()
-    s.set("timeout", 10000)
+    s.set("timeout", 100000)
 
     for constraint in constraints:
         s.add(constraint)

mythril/laser/ethereum/instructions.py

@@ -707,13 +707,8 @@ class Instruction:
             index = str(index)
 
         try:
-            # Create a fresh copy of the account object before modifying storage
-
-            for k in global_state.accounts:
-                if global_state.accounts[k] == global_state.environment.active_account:
-                    global_state.accounts[k] = deepcopy(global_state.accounts[k])
-                    global_state.environment.active_account = global_state.accounts[k]
-                    break
+            global_state.environment.active_account = deepcopy(global_state.environment.active_account)
+            global_state.accounts[global_state.environment.active_account.address] = global_state.environment.active_account
 
             global_state.environment.active_account.storage[index] = value
         except KeyError:
@@ -778,7 +773,7 @@ class Instruction:
                 new_state = copy(global_state)
                 new_state.mstate.pc = index
                 new_state.mstate.depth += 1
-                new_state.mstate.constraints.append(condi)
+                new_state.mstate.constraints.append(simplify(condi))
 
                 states.append(new_state)
             else:
@@ -786,12 +781,11 @@ class Instruction:
 
         # False case
         negated = Not(condition) if type(condition) == BoolRef else condition == 0
-        sat = not is_false(simplify(negated)) if type(condi) == BoolRef else not negated
 
-        if sat:
+        if (type(negated) == bool and negated) or (type(negated) == BoolRef and not is_false(simplify(negated))):
             new_state = copy(global_state)
             new_state.mstate.depth += 1
-            new_state.mstate.constraints.append(negated)
+            new_state.mstate.constraints.append(simplify(negated))
             states.append(new_state)
         else:
             logging.debug("Pruned unreachable states.")

mythril/laser/ethereum/state.py

@@ -38,8 +38,14 @@ class Account:
     def add_balance(self, balance):
         self.balance += balance
 
-    def get_storage(self, index):
-        return self.storage[index] if index in self.storage.keys() else BitVec("storage_" + str(index), 256)
+    # def get_storage(self, index):
+    #     return BitVec("storage_" + str(index), 256)
+    #     if index in self.storage.keys():
+    #         return self.storage[index]
+    #     else:
+    #         symbol = BitVec("storage_" + str(index), 256)
+    #         self.storage[index] = symbol
+    #         return symbol
 
     @property
     def as_dict(self):
@@ -78,6 +84,7 @@ class Environment:
     def __str__(self):
         return str(self.as_dict)
 
+
     @property
     def as_dict(self):
         return dict(active_account=self.active_account, sender=self.sender, calldata=self.calldata,
@@ -145,7 +152,7 @@ class GlobalState:
 
 
     def __copy__(self):
-        accounts = self.accounts
+        accounts = copy(self.accounts)
         environment = copy(self.environment)
         mstate = deepcopy(self.mstate)
         call_stack = copy(self.call_stack)

mythril/laser/ethereum/svm.py

@@ -70,7 +70,7 @@ class LaserEVM:
             try:
                 new_states, op_code = self.execute_state(global_state)
             except NotImplementedError:
-                logging.debug("Encountered unimplemented instruction")
+                logging.info("Encountered unimplemented instruction: {}".format(op_code))
                 continue
 
             if len(new_states) == 0:

mythril/laser/ethereum/taint_analysis.py

@@ -118,7 +118,7 @@ class TaintRunner:
         direct_children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid]
         children = []
         for child in direct_children:
-            if child.states[0].environment == environment:
+            if child.states[0].environment.active_account.address == environment.active_account.address:
                 children.append(child)
             else:
                 children += TaintRunner.children(child, statespace, environment)

tests/taint_runner_test.py

@@ -3,7 +3,7 @@ import pytest
 from pytest_mock import mocker
 from mythril.laser.ethereum.taint_analysis import *
 from mythril.laser.ethereum.svm import GlobalState, Node, Edge, LaserEVM
-from mythril.laser.ethereum.state import MachineState
+from mythril.laser.ethereum.state import MachineState, Account, Environment
 
 
 def test_execute_state(mocker):
@@ -57,12 +57,14 @@ def test_execute_node(mocker):
 
 
 def test_execute(mocker):
-    state_1 = GlobalState(None, None, None, MachineState(gas=10000000))
+    active_account = Account('0x00')
+    environment = Environment(active_account, None, None, None, None, None)
+    state_1 = GlobalState(None, environment, None, MachineState(gas=10000000))
     state_1.mstate.stack = [1, 2]
     mocker.patch.object(state_1, 'get_current_instruction')
     state_1.get_current_instruction.return_value = {"opcode": "PUSH"}
 
-    state_2 = GlobalState(None, None, None, MachineState(gas=10000000))
+    state_2 = GlobalState(None, environment, None, MachineState(gas=10000000))
     state_2.mstate.stack = [1, 2, 3]
     mocker.patch.object(state_2, 'get_current_instruction')
     state_2.get_current_instruction.return_value = {"opcode": "ADD"}
@@ -70,7 +72,7 @@ def test_execute(mocker):
     node_1 = Node("Test contract")
     node_1.states = [state_1, state_2]
 
-    state_3 = GlobalState(None, None, None, MachineState(gas=10000000))
+    state_3 = GlobalState(None, environment, None, MachineState(gas=10000000))
     state_3.mstate.stack = [1, 2]
     mocker.patch.object(state_3, 'get_current_instruction')
     state_3.get_current_instruction.return_value = {"opcode": "ADD"}

tests/testdata/input_contracts/environments.sol

@@ -0,0 +1,19 @@
+pragma solidity ^0.4.16;
+
+
+contract IntegerOverflow2 {
+    uint256 public count = 7;
+    mapping(address => uint256) balances;
+
+  function batchTransfer(address[] _receivers, uint256 _value) public returns(bool){
+    uint cnt = _receivers.length;
+    uint256 amount = uint256(cnt) * _value;
+
+    require(cnt > 0 && cnt <= 20);
+
+    balances[msg.sender] -=amount;
+
+    return true;
+  }
+
+}

tests/testdata/inputs/environments.sol.o

@@ -0,0 +1 @@
+60806040526004361061004c576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806306661abd1461005157806383f12fec1461007c575b600080fd5b34801561005d57600080fd5b50610066610104565b6040518082815260200191505060405180910390f35b34801561008857600080fd5b506100ea600480360381019080803590602001908201803590602001908080602002602001604051908101604052809392919081815260200183836020028082843782019150505050505091929192908035906020019092919050505061010a565b604051808215151515815260200191505060405180910390f35b60005481565b6000806000845191508382029050600082118015610129575060148211155b151561013457600080fd5b80600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008282540392505081905550600192505050929150505600a165627a7a7230582016b81221eb990028632ba9b34d3c01599d24acdb5b81dd6789845696f5db257c0029

tests/testdata/outputs_expected/environments.sol.o.easm

@@ -0,0 +1,259 @@
+0 PUSH1 0x80
+2 PUSH1 0x40
+4 MSTORE
+5 PUSH1 0x04
+7 CALLDATASIZE
+8 LT
+9 PUSH2 0x004c
+12 JUMPI
+13 PUSH1 0x00
+15 CALLDATALOAD
+16 PUSH29 0x0100000000000000000000000000000000000000000000000000000000
+46 SWAP1
+47 DIV
+48 PUSH4 0xffffffff
+53 AND
+54 DUP1
+55 PUSH4 0x06661abd
+60 EQ
+61 PUSH2 0x0051
+64 JUMPI
+65 DUP1
+66 PUSH4 0x83f12fec
+71 EQ
+72 PUSH2 0x007c
+75 JUMPI
+76 JUMPDEST
+77 PUSH1 0x00
+79 DUP1
+80 REVERT
+81 JUMPDEST
+82 CALLVALUE
+83 DUP1
+84 ISZERO
+85 PUSH2 0x005d
+88 JUMPI
+89 PUSH1 0x00
+91 DUP1
+92 REVERT
+93 JUMPDEST
+94 POP
+95 PUSH2 0x0066
+98 PUSH2 0x0104
+101 JUMP
+102 JUMPDEST
+103 PUSH1 0x40
+105 MLOAD
+106 DUP1
+107 DUP3
+108 DUP2
+109 MSTORE
+110 PUSH1 0x20
+112 ADD
+113 SWAP2
+114 POP
+115 POP
+116 PUSH1 0x40
+118 MLOAD
+119 DUP1
+120 SWAP2
+121 SUB
+122 SWAP1
+123 RETURN
+124 JUMPDEST
+125 CALLVALUE
+126 DUP1
+127 ISZERO
+128 PUSH2 0x0088
+131 JUMPI
+132 PUSH1 0x00
+134 DUP1
+135 REVERT
+136 JUMPDEST
+137 POP
+138 PUSH2 0x00ea
+141 PUSH1 0x04
+143 DUP1
+144 CALLDATASIZE
+145 SUB
+146 DUP2
+147 ADD
+148 SWAP1
+149 DUP1
+150 DUP1
+151 CALLDATALOAD
+152 SWAP1
+153 PUSH1 0x20
+155 ADD
+156 SWAP1
+157 DUP3
+158 ADD
+159 DUP1
+160 CALLDATALOAD
+161 SWAP1
+162 PUSH1 0x20
+164 ADD
+165 SWAP1
+166 DUP1
+167 DUP1
+168 PUSH1 0x20
+170 MUL
+171 PUSH1 0x20
+173 ADD
+174 PUSH1 0x40
+176 MLOAD
+177 SWAP1
+178 DUP2
+179 ADD
+180 PUSH1 0x40
+182 MSTORE
+183 DUP1
+184 SWAP4
+185 SWAP3
+186 SWAP2
+187 SWAP1
+188 DUP2
+189 DUP2
+190 MSTORE
+191 PUSH1 0x20
+193 ADD
+194 DUP4
+195 DUP4
+196 PUSH1 0x20
+198 MUL
+199 DUP1
+200 DUP3
+201 DUP5
+202 CALLDATACOPY
+203 DUP3
+204 ADD
+205 SWAP2
+206 POP
+207 POP
+208 POP
+209 POP
+210 POP
+211 POP
+212 SWAP2
+213 SWAP3
+214 SWAP2
+215 SWAP3
+216 SWAP1
+217 DUP1
+218 CALLDATALOAD
+219 SWAP1
+220 PUSH1 0x20
+222 ADD
+223 SWAP1
+224 SWAP3
+225 SWAP2
+226 SWAP1
+227 POP
+228 POP
+229 POP
+230 PUSH2 0x010a
+233 JUMP
+234 JUMPDEST
+235 PUSH1 0x40
+237 MLOAD
+238 DUP1
+239 DUP3
+240 ISZERO
+241 ISZERO
+242 ISZERO
+243 ISZERO
+244 DUP2
+245 MSTORE
+246 PUSH1 0x20
+248 ADD
+249 SWAP2
+250 POP
+251 POP
+252 PUSH1 0x40
+254 MLOAD
+255 DUP1
+256 SWAP2
+257 SUB
+258 SWAP1
+259 RETURN
+260 JUMPDEST
+261 PUSH1 0x00
+263 SLOAD
+264 DUP2
+265 JUMP
+266 JUMPDEST
+267 PUSH1 0x00
+269 DUP1
+270 PUSH1 0x00
+272 DUP5
+273 MLOAD
+274 SWAP2
+275 POP
+276 DUP4
+277 DUP3
+278 MUL
+279 SWAP1
+280 POP
+281 PUSH1 0x00
+283 DUP3
+284 GT
+285 DUP1
+286 ISZERO
+287 PUSH2 0x0129
+290 JUMPI
+291 POP
+292 PUSH1 0x14
+294 DUP3
+295 GT
+296 ISZERO
+297 JUMPDEST
+298 ISZERO
+299 ISZERO
+300 PUSH2 0x0134
+303 JUMPI
+304 PUSH1 0x00
+306 DUP1
+307 REVERT
+308 JUMPDEST
+309 DUP1
+310 PUSH1 0x01
+312 PUSH1 0x00
+314 CALLER
+315 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
+336 AND
+337 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
+358 AND
+359 DUP2
+360 MSTORE
+361 PUSH1 0x20
+363 ADD
+364 SWAP1
+365 DUP2
+366 MSTORE
+367 PUSH1 0x20
+369 ADD
+370 PUSH1 0x00
+372 SHA3
+373 PUSH1 0x00
+375 DUP3
+376 DUP3
+377 SLOAD
+378 SUB
+379 SWAP3
+380 POP
+381 POP
+382 DUP2
+383 SWAP1
+384 SSTORE
+385 POP
+386 PUSH1 0x01
+388 SWAP3
+389 POP
+390 POP
+391 POP
+392 SWAP3
+393 SWAP2
+394 POP
+395 POP
+396 JUMP
+397 STOP

tests/testdata/outputs_expected/environments.sol.o.json

@@ -0,0 +1 @@
+{"error": null, "issues": [{"address": 158, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A possible integer overflow exists in the function `_function_0x83f12fec`.\nThe addition or multiplication may result in a value higher than the maximum representable integer.", "function": "_function_0x83f12fec", "title": "Integer Overflow", "type": "Warning"}, {"address": 278, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A possible integer overflow exists in the function `_function_0x83f12fec`.\nThe addition or multiplication may result in a value higher than the maximum representable integer.", "function": "_function_0x83f12fec", "title": "Integer Overflow", "type": "Warning"}, {"address": 378, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A possible integer underflow exists in the function `_function_0x83f12fec`.\nThe subtraction may result in a value < 0.", "function": "_function_0x83f12fec", "title": "Integer Underflow", "type": "Warning"}], "success": true}

tests/testdata/outputs_expected/environments.sol.o.markdown

@@ -0,0 +1,37 @@
+# Analysis results for test-filename.sol
+
+## Integer Overflow
+
+- Type: Warning
+- Contract: Unknown
+- Function name: `_function_0x83f12fec`
+- PC address: 158
+
+### Description
+
+A possible integer overflow exists in the function `_function_0x83f12fec`.
+The addition or multiplication may result in a value higher than the maximum representable integer.
+
+## Integer Overflow
+
+- Type: Warning
+- Contract: Unknown
+- Function name: `_function_0x83f12fec`
+- PC address: 278
+
+### Description
+
+A possible integer overflow exists in the function `_function_0x83f12fec`.
+The addition or multiplication may result in a value higher than the maximum representable integer.
+
+## Integer Underflow
+
+- Type: Warning
+- Contract: Unknown
+- Function name: `_function_0x83f12fec`
+- PC address: 378
+
+### Description
+
+A possible integer underflow exists in the function `_function_0x83f12fec`.
+The subtraction may result in a value < 0.

tests/testdata/outputs_expected/environments.sol.o.text

@@ -0,0 +1,27 @@
+==== Integer Overflow ====
+Type: Warning
+Contract: Unknown
+Function name: _function_0x83f12fec
+PC address: 158
+A possible integer overflow exists in the function `_function_0x83f12fec`.
+The addition or multiplication may result in a value higher than the maximum representable integer.
+--------------------
+
+==== Integer Overflow ====
+Type: Warning
+Contract: Unknown
+Function name: _function_0x83f12fec
+PC address: 278
+A possible integer overflow exists in the function `_function_0x83f12fec`.
+The addition or multiplication may result in a value higher than the maximum representable integer.
+--------------------
+
+==== Integer Underflow ====
+Type: Warning
+Contract: Unknown
+Function name: _function_0x83f12fec
+PC address: 378
+A possible integer underflow exists in the function `_function_0x83f12fec`.
+The subtraction may result in a value < 0.
+--------------------
+