Merge branch 'features/integeroverflow' of git://github.com/JoranHonig/mythril into JoranHonig-features/integeroverflow

pull/120/head
Bernhard Mueller 7 years ago
commit 9e340d64c9
  1. 2
      myth
  2. 190
      mythril/analysis/modules/integer.py
  3. 21
      tests/testdata/inputs/overflow.sol
  4. 365
      tests/testdata/outputs_expected/overflow.sol.easm
  5. 168
      tests/testdata/outputs_expected/overflow.sol.graph.html
  6. 39
      tests/testdata/outputs_expected/overflow.sol.json
  7. 46
      tests/testdata/outputs_expected/overflow.sol.markdown
  8. 42
      tests/testdata/outputs_expected/overflow.sol.text

@ -34,6 +34,8 @@ from mythril.analysis.security import fire_lasers
from mythril.analysis.report import Report
from mythril.leveldb.client import EthLevelDB
# logging.basicConfig(level=logging.DEBUG)
def searchCallback(code_hash, code, addresses, balances):
print("Matched contract with code hash " + code_hash)

@ -7,17 +7,21 @@ import re
import copy
import logging
'''
MODULE DESCRIPTION:
Check for integer underflows.
For every SUB instruction, check if there's a possible state where op1 > op0.
For every ADD instruction, check if there's a possible state where op1 + op0 > 2^32 - 1
'''
def execute(statespace):
"""
Executes analysis module for integer underflow
:param statespace: Statespace to analyse
:return: Found issues
"""
logging.debug("Executing module: INTEGER")
issues = []
@ -26,52 +30,178 @@ def execute(statespace):
node = statespace.nodes[k]
for state in node.states:
logging.debug("Checking for integer underflow")
issues += _check_integer_underflow(state, node)
logging.debug("Checking for integer overflow")
issues += _check_integer_overflow(statespace, state, node)
return issues
def _check_integer_overflow(statespace, state, node):
"""
Checks for integer overflow
:param statespace: statespace that is being examined
:param state: state from node to examine
:param node: node to examine
:return: found issue
"""
issues = []
# Check the instruction
instruction = state.get_current_instruction()
if instruction['opcode'] != "ADD":
return []
instruction = state.get_current_instruction()
constraints = copy.deepcopy(node.constraints)
if(instruction['opcode'] == "SUB"):
# Formulate overflow constraints
stack = state.mstate.stack
op0, op1 = stack[-1], stack[-2]
stack = state.mstate.stack
# An integer overflow is possible if op0 + op1,
constraints.append(UGT(op0 + op1, (2 ** 32) - 1))
try:
model = solver.get_model(constraints)
# If we get to this point then there has been an integer overflow
# Find out if the overflowed value is actually used
interesting_usages = _search_children(statespace, node, (op0 + op1), index=node.states.index(state))
# Stop if it isn't
if len(interesting_usages) == 0:
return issues
issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Overflow ",
"Warning")
issue.description = "A possible integer overflow exists in the function {}.\n " \
"Addition will result in a lower value.".format(node.function_name)
issue.debug = solver.pretty_print_model(model)
issues.append(issue)
except UnsatError:
logging.debug("[INTEGER_OVERFLOW] no model found")
return issues
op0 = stack[-1]
op1 = stack[-2]
constraints = copy.deepcopy(node.constraints)
def _check_integer_underflow(state, node):
"""
Checks for integer underflow
:param state: state from node to examine
:param node: node to examine
:return: found issue
"""
issues = []
instruction = state.get_current_instruction()
if type(op0) == int and type(op1) == int:
continue
if instruction['opcode'] == "SUB":
if (re.search(r'calldatasize_', str(op0))) \
or (re.search(r'256\*.*If\(1', str(op0), re.DOTALL) or re.search(r'256\*.*If\(1', str(op1), re.DOTALL)) \
or (re.search(r'32 \+.*calldata', str(op0), re.DOTALL) or re.search(r'32 \+.*calldata', str(op1), re.DOTALL)):
stack = state.mstate.stack
# Filter for patterns that contain bening nteger underflows.
op0 = stack[-1]
op1 = stack[-2]
# Pattern 1: (96 + calldatasize_MAIN) - (96), where (96 + calldatasize_MAIN) would underflow if calldatasize is very large.
# Pattern 2: (256*If(1 & storage_0 == 0, 1, 0)) - 1, this would underlow if storage_0 = 0
constraints = copy.deepcopy(node.constraints)
continue
# Filter for patterns that contain bening nteger underflows.
logging.debug("[INTEGER_UNDERFLOW] Checking SUB " + str(op0) + ", " + str(op1) + " at address " + str(instruction['address']))
# Pattern 1: (96 + calldatasize_MAIN) - (96), where (96 + calldatasize_MAIN) would underflow if calldatasize is very large.
# Pattern 2: (256*If(1 & storage_0 == 0, 1, 0)) - 1, this would underlow if storage_0 = 0
if type(op0) == int and type(op1) == int:
return []
if re.search(r'calldatasize_', str(op0)):
return []
if re.search(r'256\*.*If\(1', str(op0), re.DOTALL) or re.search(r'256\*.*If\(1', str(op1), re.DOTALL):
return []
if re.search(r'32 \+.*calldata', str(op0), re.DOTALL) or re.search(r'32 \+.*calldata', str(op1), re.DOTALL):
return []
allowed_types = [int, BitVecRef, BitVecNumRef]
logging.debug("[INTEGER_UNDERFLOW] Checking SUB {0}, {1} at address {2}".format(str(op0), str(op1),
str(instruction['address'])))
if type(op0) in allowed_types and type(op1) in allowed_types:
constraints.append(UGT(op1,op0))
allowed_types = [int, BitVecRef, BitVecNumRef]
try:
if type(op0) in allowed_types and type(op1) in allowed_types:
constraints.append(UGT(op1, op0))
model = solver.get_model(constraints)
try:
issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Underflow", "Warning")
model = solver.get_model(constraints)
issue.description = "A possible integer underflow exists in the function " + node.function_name + ".\n" \
"The subtraction may result in a value < 0."
issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Underflow",
"Warning")
issue.debug = solver.pretty_print_model(model)
issues.append(issue)
issue.description = "A possible integer underflow exists in the function " + node.function_name + ".\n" \
"The subtraction may result in a value < 0."
except UnsatError:
logging.debug("[INTEGER_UNDERFLOW] no model found")
issue.debug = solver.pretty_print_model(model)
issues.append(issue)
except UnsatError:
logging.debug("[INTEGER_UNDERFLOW] no model found")
return issues
def _check_usage(state, expression):
"""Delegates checks to _check_{instruction_name}()"""
opcode = state.get_current_instruction()['opcode']
if opcode == 'JUMPI':
if _check_jumpi(state, expression):
return [state]
elif opcode == 'SSTORE':
if _check_sstore(state, expression):
return [state]
return []
def _check_jumpi(state, expression):
""" Check if conditional jump is dependent on the result of expression"""
assert state.get_current_instruction()['opcode'] is 'JUMPI'
condition = state.mstate.stack[-2]
return str(expression) in str(condition)
def _check_sstore(state, expression):
""" Check if store operation is dependent on the result of expression"""
assert state.get_current_instruction()['opcode'] is 'SSTORE'
value = state.mstate.stack[-2]
return str(expression) in str(value)
def _search_children(statespace, node, expression, index=0, depth=0, max_depth=64):
"""
Checks the statespace for children states, with JUMPI or SSTORE instuctions,
for dependency on expression
:param statespace: The statespace to explore
:param node: Current node to explore from
:param expression: Expression to look for
:param index: Current state index node.states[index] == current_state
:param depth: Current depth level
:param max_depth: Max depth to explore
:return: List of states that match the opcodes and are dependent on expression
"""
logging.debug("SEARCHING NODE for usage of an overflowed variable %d", node.uid)
results = []
if depth >= max_depth:
return []
# Explore current node from index
for j in range(index, len(node.states)):
current_state = node.states[j]
current_instruction = current_state.get_current_instruction()
if current_instruction['opcode'] in ('JUMPI', 'SSTORE'):
results += _check_usage(current_state, expression)
# Recursively search children
children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid]
for child in children:
results += _search_children(statespace, child, expression, depth=depth+1, max_depth=max_depth)
return results

@ -0,0 +1,21 @@
contract Over {
mapping(address => uint) balances;
uint public totalSupply;
function Token(uint _initialSupply) {
balances[msg.sender] = totalSupply = _initialSupply;
}
function sendeth(address _to, uint _value) public returns (bool) {
require(balances[msg.sender] - _value >= 0);
balances[msg.sender] -= _value;
balances[_to] += _value;
balances[_to] = 2;
return true;
}
function balanceOf(address _owner) public constant returns (uint balance) {
return balances[_owner];
}
}

@ -0,0 +1,365 @@
0 PUSH1 0x60
2 PUSH1 0x40
4 MSTORE
5 PUSH1 0x04
7 CALLDATASIZE
8 LT
9 PUSH2 0x0062
12 JUMPI
13 PUSH1 0x00
15 CALLDATALOAD
16 PUSH29 0x0100000000000000000000000000000000000000000000000000000000
46 SWAP1
47 DIV
48 PUSH4 0xffffffff
53 AND
54 DUP1
55 PUSH4 0x18160ddd
60 EQ
61 PUSH2 0x0067
64 JUMPI
65 DUP1
66 PUSH4 0x6241bfd1
71 EQ
72 PUSH2 0x0090
75 JUMPI
76 DUP1
77 PUSH4 0x70a08231
82 EQ
83 PUSH2 0x00b3
86 JUMPI
87 DUP1
88 PUSH4 0xa3210e87
93 EQ
94 PUSH2 0x0100
97 JUMPI
98 JUMPDEST
99 PUSH1 0x00
101 DUP1
102 REVERT
103 JUMPDEST
104 CALLVALUE
105 ISZERO
106 PUSH2 0x0072
109 JUMPI
110 PUSH1 0x00
112 DUP1
113 REVERT
114 JUMPDEST
115 PUSH2 0x007a
118 PUSH2 0x015a
121 JUMP
122 JUMPDEST
123 PUSH1 0x40
125 MLOAD
126 DUP1
127 DUP3
128 DUP2
129 MSTORE
130 PUSH1 0x20
132 ADD
133 SWAP2
134 POP
135 POP
136 PUSH1 0x40
138 MLOAD
139 DUP1
140 SWAP2
141 SUB
142 SWAP1
143 RETURN
144 JUMPDEST
145 CALLVALUE
146 ISZERO
147 PUSH2 0x009b
150 JUMPI
151 PUSH1 0x00
153 DUP1
154 REVERT
155 JUMPDEST
156 PUSH2 0x00b1
159 PUSH1 0x04
161 DUP1
162 DUP1
163 CALLDATALOAD
164 SWAP1
165 PUSH1 0x20
167 ADD
168 SWAP1
169 SWAP2
170 SWAP1
171 POP
172 POP
173 PUSH2 0x0160
176 JUMP
177 JUMPDEST
178 STOP
179 JUMPDEST
180 CALLVALUE
181 ISZERO
182 PUSH2 0x00be
185 JUMPI
186 PUSH1 0x00
188 DUP1
189 REVERT
190 JUMPDEST
191 PUSH2 0x00ea
194 PUSH1 0x04
196 DUP1
197 DUP1
198 CALLDATALOAD
199 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
220 AND
221 SWAP1
222 PUSH1 0x20
224 ADD
225 SWAP1
226 SWAP2
227 SWAP1
228 POP
229 POP
230 PUSH2 0x01ab
233 JUMP
234 JUMPDEST
235 PUSH1 0x40
237 MLOAD
238 DUP1
239 DUP3
240 DUP2
241 MSTORE
242 PUSH1 0x20
244 ADD
245 SWAP2
246 POP
247 POP
248 PUSH1 0x40
250 MLOAD
251 DUP1
252 SWAP2
253 SUB
254 SWAP1
255 RETURN
256 JUMPDEST
257 CALLVALUE
258 ISZERO
259 PUSH2 0x010b
262 JUMPI
263 PUSH1 0x00
265 DUP1
266 REVERT
267 JUMPDEST
268 PUSH2 0x0140
271 PUSH1 0x04
273 DUP1
274 DUP1
275 CALLDATALOAD
276 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
297 AND
298 SWAP1
299 PUSH1 0x20
301 ADD
302 SWAP1
303 SWAP2
304 SWAP1
305 DUP1
306 CALLDATALOAD
307 SWAP1
308 PUSH1 0x20
310 ADD
311 SWAP1
312 SWAP2
313 SWAP1
314 POP
315 POP
316 PUSH2 0x01f3
319 JUMP
320 JUMPDEST
321 PUSH1 0x40
323 MLOAD
324 DUP1
325 DUP3
326 ISZERO
327 ISZERO
328 ISZERO
329 ISZERO
330 DUP2
331 MSTORE
332 PUSH1 0x20
334 ADD
335 SWAP2
336 POP
337 POP
338 PUSH1 0x40
340 MLOAD
341 DUP1
342 SWAP2
343 SUB
344 SWAP1
345 RETURN
346 JUMPDEST
347 PUSH1 0x01
349 SLOAD
350 DUP2
351 JUMP
352 JUMPDEST
353 DUP1
354 PUSH1 0x01
356 DUP2
357 SWAP1
358 SSTORE
359 PUSH1 0x00
361 DUP1
362 CALLER
363 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
384 AND
385 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
406 AND
407 DUP2
408 MSTORE
409 PUSH1 0x20
411 ADD
412 SWAP1
413 DUP2
414 MSTORE
415 PUSH1 0x20
417 ADD
418 PUSH1 0x00
420 SHA3
421 DUP2
422 SWAP1
423 SSTORE
424 POP
425 POP
426 JUMP
427 JUMPDEST
428 PUSH1 0x00
430 DUP1
431 PUSH1 0x00
433 DUP4
434 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
455 AND
456 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
477 AND
478 DUP2
479 MSTORE
480 PUSH1 0x20
482 ADD
483 SWAP1
484 DUP2
485 MSTORE
486 PUSH1 0x20
488 ADD
489 PUSH1 0x00
491 SHA3
492 SLOAD
493 SWAP1
494 POP
495 SWAP2
496 SWAP1
497 POP
498 JUMP
499 JUMPDEST
500 PUSH1 0x00
502 DUP1
503 DUP3
504 PUSH1 0x00
506 DUP1
507 CALLER
508 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
529 AND
530 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
551 AND
552 DUP2
553 MSTORE
554 PUSH1 0x20
556 ADD
557 SWAP1
558 DUP2
559 MSTORE
560 PUSH1 0x20
562 ADD
563 PUSH1 0x00
565 SHA3
566 SLOAD
567 SUB
568 LT
569 ISZERO
570 ISZERO
571 ISZERO
572 PUSH2 0x0244
575 JUMPI
576 PUSH1 0x00
578 DUP1
579 REVERT
580 JUMPDEST
581 DUP2
582 PUSH1 0x00
584 DUP1
585 CALLER
586 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
607 AND
608 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
629 AND
630 DUP2
631 MSTORE
632 PUSH1 0x20
634 ADD
635 SWAP1
636 DUP2
637 MSTORE
638 PUSH1 0x20
640 ADD
641 PUSH1 0x00
643 SHA3
644 PUSH1 0x00
646 DUP3
647 DUP3
648 SLOAD
649 SUB
650 SWAP3
651 POP
652 POP
653 DUP2
654 SWAP1
655 SSTORE
656 POP
657 DUP2
658 PUSH1 0x00
660 DUP1
661 DUP6
662 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
683 AND
684 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
705 AND
706 DUP2
707 MSTORE
708 PUSH1 0x20
710 ADD
711 SWAP1
712 DUP2
713 MSTORE
714 PUSH1 0x20
716 ADD
717 PUSH1 0x00
719 SHA3
720 PUSH1 0x00
722 DUP3
723 DUP3
724 SLOAD
725 ADD
726 SWAP3
727 POP
728 POP
729 DUP2
730 SWAP1
731 SSTORE
732 POP
733 PUSH1 0x01
735 SWAP1
736 POP
737 SWAP3
738 SWAP2
739 POP
740 POP
741 JUMP
742 STOP

@ -0,0 +1,168 @@
<html>
<head>
<style type="text/css">
#mynetwork {
background-color: #232625;
}
body {
background-color: #232625;
color: #ffffff;
font-size: 10px;
}
</style>
<link href="https://cdnjs.cloudflare.com/ajax/libs/vis/4.21.0/vis.min.css" rel="stylesheet" type="text/css" />
<script src="https://cdnjs.cloudflare.com/ajax/libs/vis/4.21.0/vis.min.js"></script>
<script>
var options = {
autoResize: true,
height: '100%',
width: '100%',
manipulation: false,
height: '90%',
layout: {
randomSeed: undefined,
improvedLayout:true,
hierarchical: {
enabled:true,
levelSeparation: 450,
nodeSpacing: 200,
treeSpacing: 100,
blockShifting: true,
edgeMinimization: true,
parentCentralization: false,
direction: 'LR', // UD, DU, LR, RL
sortMethod: 'directed' // hubsize, directed
}
},
nodes:{
borderWidth: 1,
borderWidthSelected: 2,
chosen: true,
shape: 'box',
font: {
align: 'left',
color: '#FFFFFF',
},
},
edges:{
font: {
color: '#ffffff',
size: 12, // px
face: 'arial',
background: 'none',
strokeWidth: 0, // px
strokeColor: '#ffffff',
align: 'horizontal',
multi: false,
vadjust: 0,
}
},
physics:{
enabled: false,
}
}
var nodes = [
{id: '18', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '98 JUMPDEST\n99 PUSH1 0x00\n101 DUP1\n102 REVERT\n', 'fullLabel': '98 JUMPDEST\n99 PUSH1 0x00\n101 DUP1\n102 REVERT\n', 'truncLabel': '98 JUMPDEST\n99 PUSH1 0x00\n101 DUP1\n102 REVERT\n', 'isExpanded': false},
{id: '23', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '122 JUMPDEST\n123 PUSH1 0x40\n125 MLOAD\n126 DUP1\n127 DUP3\n128 DUP2\n(click to expand +)', 'fullLabel': '122 JUMPDEST\n123 PUSH1 0x40\n125 MLOAD\n126 DUP1\n127 DUP3\n128 DUP2\n129 MSTORE\n130 PUSH1 0x20\n132 ADD\n133 SWAP2\n134 POP\n135 POP\n136 PUSH1 0x40\n138 MLOAD\n139 DUP1\n140 SWAP2\n141 SUB\n142 SWAP1\n143 RETURN\n', 'truncLabel': '122 JUMPDEST\n123 PUSH1 0x40\n125 MLOAD\n126 DUP1\n127 DUP3\n128 DUP2\n(click to expand +)', 'isExpanded': false},
{id: '22', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '346 JUMPDEST\n347 PUSH1 0x01\n349 SLOAD\n350 DUP2\n351 JUMP\n', 'fullLabel': '346 JUMPDEST\n347 PUSH1 0x01\n349 SLOAD\n350 DUP2\n351 JUMP\n', 'truncLabel': '346 JUMPDEST\n347 PUSH1 0x01\n349 SLOAD\n350 DUP2\n351 JUMP\n', 'isExpanded': false},
{id: '21', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '114 JUMPDEST\n115 PUSH2 0x007a\n118 PUSH2 0x015a\n121 JUMP\n', 'fullLabel': '114 JUMPDEST\n115 PUSH2 0x007a\n118 PUSH2 0x015a\n121 JUMP\n', 'truncLabel': '114 JUMPDEST\n115 PUSH2 0x007a\n118 PUSH2 0x015a\n121 JUMP\n', 'isExpanded': false},
{id: '24', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '110 PUSH1 0x00\n112 DUP1\n113 REVERT\n', 'fullLabel': '110 PUSH1 0x00\n112 DUP1\n113 REVERT\n', 'truncLabel': '110 PUSH1 0x00\n112 DUP1\n113 REVERT\n', 'isExpanded': false},
{id: '20', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '103 _function_0x18160ddd\n104 CALLVALUE\n105 ISZERO\n106 PUSH2 0x0072\n109 JUMPI\n', 'fullLabel': '103 _function_0x18160ddd\n104 CALLVALUE\n105 ISZERO\n106 PUSH2 0x0072\n109 JUMPI\n', 'truncLabel': '103 _function_0x18160ddd\n104 CALLVALUE\n105 ISZERO\n106 PUSH2 0x0072\n109 JUMPI\n', 'isExpanded': false},
{id: '29', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '177 JUMPDEST\n178 STOP\n', 'fullLabel': '177 JUMPDEST\n178 STOP\n', 'truncLabel': '177 JUMPDEST\n178 STOP\n', 'isExpanded': false},
{id: '28', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '352 JUMPDEST\n353 DUP1\n354 PUSH1 0x01\n356 DUP2\n357 SWAP1\n358 SSTORE\n(click to expand +)', 'fullLabel': '352 JUMPDEST\n353 DUP1\n354 PUSH1 0x01\n356 DUP2\n357 SWAP1\n358 SSTORE\n359 PUSH1 0x00\n361 DUP1\n362 CALLER\n363 PUSH20 0xffffffff(...)\n384 AND\n385 PUSH20 0xffffffff(...)\n406 AND\n407 DUP2\n408 MSTORE\n409 PUSH1 0x20\n411 ADD\n412 SWAP1\n413 DUP2\n414 MSTORE\n415 PUSH1 0x20\n417 ADD\n418 PUSH1 0x00\n420 SHA3\n421 DUP2\n422 SWAP1\n423 SSTORE\n424 POP\n425 POP\n426 JUMP\n', 'truncLabel': '352 JUMPDEST\n353 DUP1\n354 PUSH1 0x01\n356 DUP2\n357 SWAP1\n358 SSTORE\n(click to expand +)', 'isExpanded': false},
{id: '27', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '155 JUMPDEST\n156 PUSH2 0x00b1\n159 PUSH1 0x04\n161 DUP1\n162 DUP1\n163 CALLDATALOAD\n(click to expand +)', 'fullLabel': '155 JUMPDEST\n156 PUSH2 0x00b1\n159 PUSH1 0x04\n161 DUP1\n162 DUP1\n163 CALLDATALOAD\n164 SWAP1\n165 PUSH1 0x20\n167 ADD\n168 SWAP1\n169 SWAP2\n170 SWAP1\n171 POP\n172 POP\n173 PUSH2 0x0160\n176 JUMP\n', 'truncLabel': '155 JUMPDEST\n156 PUSH2 0x00b1\n159 PUSH1 0x04\n161 DUP1\n162 DUP1\n163 CALLDATALOAD\n(click to expand +)', 'isExpanded': false},
{id: '30', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '151 PUSH1 0x00\n153 DUP1\n154 REVERT\n', 'fullLabel': '151 PUSH1 0x00\n153 DUP1\n154 REVERT\n', 'truncLabel': '151 PUSH1 0x00\n153 DUP1\n154 REVERT\n', 'isExpanded': false},
{id: '26', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '144 Token(uint256)\n145 CALLVALUE\n146 ISZERO\n147 PUSH2 0x009b\n150 JUMPI\n', 'fullLabel': '144 Token(uint256)\n145 CALLVALUE\n146 ISZERO\n147 PUSH2 0x009b\n150 JUMPI\n', 'truncLabel': '144 Token(uint256)\n145 CALLVALUE\n146 ISZERO\n147 PUSH2 0x009b\n150 JUMPI\n', 'isExpanded': false},
{id: '35', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '234 JUMPDEST\n235 PUSH1 0x40\n237 MLOAD\n238 DUP1\n239 DUP3\n240 DUP2\n(click to expand +)', 'fullLabel': '234 JUMPDEST\n235 PUSH1 0x40\n237 MLOAD\n238 DUP1\n239 DUP3\n240 DUP2\n241 MSTORE\n242 PUSH1 0x20\n244 ADD\n245 SWAP2\n246 POP\n247 POP\n248 PUSH1 0x40\n250 MLOAD\n251 DUP1\n252 SWAP2\n253 SUB\n254 SWAP1\n255 RETURN\n', 'truncLabel': '234 JUMPDEST\n235 PUSH1 0x40\n237 MLOAD\n238 DUP1\n239 DUP3\n240 DUP2\n(click to expand +)', 'isExpanded': false},
{id: '34', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '427 JUMPDEST\n428 PUSH1 0x00\n430 DUP1\n431 PUSH1 0x00\n433 DUP4\n434 PUSH20 0xffffffff(...)\n(click to expand +)', 'fullLabel': '427 JUMPDEST\n428 PUSH1 0x00\n430 DUP1\n431 PUSH1 0x00\n433 DUP4\n434 PUSH20 0xffffffff(...)\n455 AND\n456 PUSH20 0xffffffff(...)\n477 AND\n478 DUP2\n479 MSTORE\n480 PUSH1 0x20\n482 ADD\n483 SWAP1\n484 DUP2\n485 MSTORE\n486 PUSH1 0x20\n488 ADD\n489 PUSH1 0x00\n491 SHA3\n492 SLOAD\n493 SWAP1\n494 POP\n495 SWAP2\n496 SWAP1\n497 POP\n498 JUMP\n', 'truncLabel': '427 JUMPDEST\n428 PUSH1 0x00\n430 DUP1\n431 PUSH1 0x00\n433 DUP4\n434 PUSH20 0xffffffff(...)\n(click to expand +)', 'isExpanded': false},
{id: '33', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '190 JUMPDEST\n191 PUSH2 0x00ea\n194 PUSH1 0x04\n196 DUP1\n197 DUP1\n198 CALLDATALOAD\n(click to expand +)', 'fullLabel': '190 JUMPDEST\n191 PUSH2 0x00ea\n194 PUSH1 0x04\n196 DUP1\n197 DUP1\n198 CALLDATALOAD\n199 PUSH20 0xffffffff(...)\n220 AND\n221 SWAP1\n222 PUSH1 0x20\n224 ADD\n225 SWAP1\n226 SWAP2\n227 SWAP1\n228 POP\n229 POP\n230 PUSH2 0x01ab\n233 JUMP\n', 'truncLabel': '190 JUMPDEST\n191 PUSH2 0x00ea\n194 PUSH1 0x04\n196 DUP1\n197 DUP1\n198 CALLDATALOAD\n(click to expand +)', 'isExpanded': false},
{id: '36', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '186 PUSH1 0x00\n188 DUP1\n189 REVERT\n', 'fullLabel': '186 PUSH1 0x00\n188 DUP1\n189 REVERT\n', 'truncLabel': '186 PUSH1 0x00\n188 DUP1\n189 REVERT\n', 'isExpanded': false},
{id: '32', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '179 balanceOf(address)\n180 CALLVALUE\n181 ISZERO\n182 PUSH2 0x00be\n185 JUMPI\n', 'fullLabel': '179 balanceOf(address)\n180 CALLVALUE\n181 ISZERO\n182 PUSH2 0x00be\n185 JUMPI\n', 'truncLabel': '179 balanceOf(address)\n180 CALLVALUE\n181 ISZERO\n182 PUSH2 0x00be\n185 JUMPI\n', 'isExpanded': false},
{id: '42', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '320 JUMPDEST\n321 PUSH1 0x40\n323 MLOAD\n324 DUP1\n325 DUP3\n326 ISZERO\n(click to expand +)', 'fullLabel': '320 JUMPDEST\n321 PUSH1 0x40\n323 MLOAD\n324 DUP1\n325 DUP3\n326 ISZERO\n327 ISZERO\n328 ISZERO\n329 ISZERO\n330 DUP2\n331 MSTORE\n332 PUSH1 0x20\n334 ADD\n335 SWAP2\n336 POP\n337 POP\n338 PUSH1 0x40\n340 MLOAD\n341 DUP1\n342 SWAP2\n343 SUB\n344 SWAP1\n345 RETURN\n', 'truncLabel': '320 JUMPDEST\n321 PUSH1 0x40\n323 MLOAD\n324 DUP1\n325 DUP3\n326 ISZERO\n(click to expand +)', 'isExpanded': false},
{id: '41', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '580 JUMPDEST\n581 DUP2\n582 PUSH1 0x00\n584 DUP1\n585 CALLER\n586 PUSH20 0xffffffff(...)\n(click to expand +)', 'fullLabel': '580 JUMPDEST\n581 DUP2\n582 PUSH1 0x00\n584 DUP1\n585 CALLER\n586 PUSH20 0xffffffff(...)\n607 AND\n608 PUSH20 0xffffffff(...)\n629 AND\n630 DUP2\n631 MSTORE\n632 PUSH1 0x20\n634 ADD\n635 SWAP1\n636 DUP2\n637 MSTORE\n638 PUSH1 0x20\n640 ADD\n641 PUSH1 0x00\n643 SHA3\n644 PUSH1 0x00\n646 DUP3\n647 DUP3\n648 SLOAD\n649 SUB\n650 SWAP3\n651 POP\n652 POP\n653 DUP2\n654 SWAP1\n655 SSTORE\n656 POP\n657 DUP2\n658 PUSH1 0x00\n660 DUP1\n661 DUP6\n662 PUSH20 0xffffffff(...)\n683 AND\n684 PUSH20 0xffffffff(...)\n705 AND\n706 DUP2\n707 MSTORE\n708 PUSH1 0x20\n710 ADD\n711 SWAP1\n712 DUP2\n713 MSTORE\n714 PUSH1 0x20\n716 ADD\n717 PUSH1 0x00\n719 SHA3\n720 PUSH1 0x00\n722 DUP3\n723 DUP3\n724 SLOAD\n725 ADD\n726 SWAP3\n727 POP\n728 POP\n729 DUP2\n730 SWAP1\n731 SSTORE\n732 POP\n733 PUSH1 0x01\n735 SWAP1\n736 POP\n737 SWAP3\n738 SWAP2\n739 POP\n740 POP\n741 JUMP\n', 'truncLabel': '580 JUMPDEST\n581 DUP2\n582 PUSH1 0x00\n584 DUP1\n585 CALLER\n586 PUSH20 0xffffffff(...)\n(click to expand +)', 'isExpanded': false},
{id: '40', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '499 JUMPDEST\n500 PUSH1 0x00\n502 DUP1\n503 DUP3\n504 PUSH1 0x00\n506 DUP1\n(click to expand +)', 'fullLabel': '499 JUMPDEST\n500 PUSH1 0x00\n502 DUP1\n503 DUP3\n504 PUSH1 0x00\n506 DUP1\n507 CALLER\n508 PUSH20 0xffffffff(...)\n529 AND\n530 PUSH20 0xffffffff(...)\n551 AND\n552 DUP2\n553 MSTORE\n554 PUSH1 0x20\n556 ADD\n557 SWAP1\n558 DUP2\n559 MSTORE\n560 PUSH1 0x20\n562 ADD\n563 PUSH1 0x00\n565 SHA3\n566 SLOAD\n567 SUB\n568 LT\n569 ISZERO\n570 ISZERO\n571 ISZERO\n572 PUSH2 0x0244\n575 JUMPI\n', 'truncLabel': '499 JUMPDEST\n500 PUSH1 0x00\n502 DUP1\n503 DUP3\n504 PUSH1 0x00\n506 DUP1\n(click to expand +)', 'isExpanded': false},
{id: '39', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '267 JUMPDEST\n268 PUSH2 0x0140\n271 PUSH1 0x04\n273 DUP1\n274 DUP1\n275 CALLDATALOAD\n(click to expand +)', 'fullLabel': '267 JUMPDEST\n268 PUSH2 0x0140\n271 PUSH1 0x04\n273 DUP1\n274 DUP1\n275 CALLDATALOAD\n276 PUSH20 0xffffffff(...)\n297 AND\n298 SWAP1\n299 PUSH1 0x20\n301 ADD\n302 SWAP1\n303 SWAP2\n304 SWAP1\n305 DUP1\n306 CALLDATALOAD\n307 SWAP1\n308 PUSH1 0x20\n310 ADD\n311 SWAP1\n312 SWAP2\n313 SWAP1\n314 POP\n315 POP\n316 PUSH2 0x01f3\n319 JUMP\n', 'truncLabel': '267 JUMPDEST\n268 PUSH2 0x0140\n271 PUSH1 0x04\n273 DUP1\n274 DUP1\n275 CALLDATALOAD\n(click to expand +)', 'isExpanded': false},
{id: '43', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '263 PUSH1 0x00\n265 DUP1\n266 REVERT\n', 'fullLabel': '263 PUSH1 0x00\n265 DUP1\n266 REVERT\n', 'truncLabel': '263 PUSH1 0x00\n265 DUP1\n266 REVERT\n', 'isExpanded': false},
{id: '38', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '256 sendeth(address,uint256)\n257 CALLVALUE\n258 ISZERO\n259 PUSH2 0x010b\n262 JUMPI\n', 'fullLabel': '256 sendeth(address,uint256)\n257 CALLVALUE\n258 ISZERO\n259 PUSH2 0x010b\n262 JUMPI\n', 'truncLabel': '256 sendeth(address,uint256)\n257 CALLVALUE\n258 ISZERO\n259 PUSH2 0x010b\n262 JUMPI\n', 'isExpanded': false},
{id: '44', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '98 JUMPDEST\n99 PUSH1 0x00\n101 DUP1\n102 REVERT\n', 'fullLabel': '98 JUMPDEST\n99 PUSH1 0x00\n101 DUP1\n102 REVERT\n', 'truncLabel': '98 JUMPDEST\n99 PUSH1 0x00\n101 DUP1\n102 REVERT\n', 'isExpanded': false},
{id: '37', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '87 DUP1\n88 PUSH4 0xa3210e87\n93 EQ\n94 PUSH2 0x0100\n97 JUMPI\n', 'fullLabel': '87 DUP1\n88 PUSH4 0xa3210e87\n93 EQ\n94 PUSH2 0x0100\n97 JUMPI\n', 'truncLabel': '87 DUP1\n88 PUSH4 0xa3210e87\n93 EQ\n94 PUSH2 0x0100\n97 JUMPI\n', 'isExpanded': false},
{id: '31', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '76 DUP1\n77 PUSH4 0x70a08231\n82 EQ\n83 PUSH2 0x00b3\n86 JUMPI\n', 'fullLabel': '76 DUP1\n77 PUSH4 0x70a08231\n82 EQ\n83 PUSH2 0x00b3\n86 JUMPI\n', 'truncLabel': '76 DUP1\n77 PUSH4 0x70a08231\n82 EQ\n83 PUSH2 0x00b3\n86 JUMPI\n', 'isExpanded': false},
{id: '25', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '65 DUP1\n66 PUSH4 0x6241bfd1\n71 EQ\n72 PUSH2 0x0090\n75 JUMPI\n', 'fullLabel': '65 DUP1\n66 PUSH4 0x6241bfd1\n71 EQ\n72 PUSH2 0x0090\n75 JUMPI\n', 'truncLabel': '65 DUP1\n66 PUSH4 0x6241bfd1\n71 EQ\n72 PUSH2 0x0090\n75 JUMPI\n', 'isExpanded': false},
{id: '19', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '13 PUSH1 0x00\n15 CALLDATALOAD\n16 PUSH29 0x01000000(...)\n46 SWAP1\n47 DIV\n48 PUSH4 0xffffffff\n(click to expand +)', 'fullLabel': '13 PUSH1 0x00\n15 CALLDATALOAD\n16 PUSH29 0x01000000(...)\n46 SWAP1\n47 DIV\n48 PUSH4 0xffffffff\n53 AND\n54 DUP1\n55 PUSH4 0x18160ddd\n60 EQ\n61 PUSH2 0x0067\n64 JUMPI\n', 'truncLabel': '13 PUSH1 0x00\n15 CALLDATALOAD\n16 PUSH29 0x01000000(...)\n46 SWAP1\n47 DIV\n48 PUSH4 0xffffffff\n(click to expand +)', 'isExpanded': false},
{id: '17', color: {border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}, size: 150, 'label': '0 PUSH1 0x60\n2 PUSH1 0x40\n4 MSTORE\n5 PUSH1 0x04\n7 CALLDATASIZE\n8 LT\n(click to expand +)', 'fullLabel': '0 PUSH1 0x60\n2 PUSH1 0x40\n4 MSTORE\n5 PUSH1 0x04\n7 CALLDATASIZE\n8 LT\n9 PUSH2 0x0062\n12 JUMPI\n', 'truncLabel': '0 PUSH1 0x60\n2 PUSH1 0x40\n4 MSTORE\n5 PUSH1 0x04\n7 CALLDATASIZE\n8 LT\n(click to expand +)', 'isExpanded': false}
];
var edges = [
{from: '17', to: '18', 'arrows': 'to', 'label': 'Not(ULE(4, calldatasize_Over))', 'smooth': {'type': 'cubicBezier'}},
{from: '22', to: '23', 'arrows': 'to', 'label': '', 'smooth': {'type': 'cubicBezier'}},
{from: '21', to: '22', 'arrows': 'to', 'label': '', 'smooth': {'type': 'cubicBezier'}},
{from: '20', to: '21', 'arrows': 'to', 'label': 'callvalue == 0', 'smooth': {'type': 'cubicBezier'}},
{from: '20', to: '24', 'arrows': 'to', 'label': 'Not(callvalue == 0)', 'smooth': {'type': 'cubicBezier'}},
{from: '19', to: '20', 'arrows': 'to', 'label': 'Extract(0xff, 0xe0, calldata_Over_0) == 0x18160ddd', 'smooth': {'type': 'cubicBezier'}},
{from: '28', to: '29', 'arrows': 'to', 'label': '', 'smooth': {'type': 'cubicBezier'}},
{from: '27', to: '28', 'arrows': 'to', 'label': '', 'smooth': {'type': 'cubicBezier'}},
{from: '26', to: '27', 'arrows': 'to', 'label': 'callvalue == 0', 'smooth': {'type': 'cubicBezier'}},
{from: '26', to: '30', 'arrows': 'to', 'label': 'Not(callvalue == 0)', 'smooth': {'type': 'cubicBezier'}},
{from: '25', to: '26', 'arrows': 'to', 'label': 'Extract(0xff, 0xe0, calldata_Over_0) == 0x6241bfd1', 'smooth': {'type': 'cubicBezier'}},
{from: '34', to: '35', 'arrows': 'to', 'label': '', 'smooth': {'type': 'cubicBezier'}},
{from: '33', to: '34', 'arrows': 'to', 'label': '', 'smooth': {'type': 'cubicBezier'}},
{from: '32', to: '33', 'arrows': 'to', 'label': 'callvalue == 0', 'smooth': {'type': 'cubicBezier'}},
{from: '32', to: '36', 'arrows': 'to', 'label': 'Not(callvalue == 0)', 'smooth': {'type': 'cubicBezier'}},
{from: '31', to: '32', 'arrows': 'to', 'label': 'Extract(0xff, 0xe0, calldata_Over_0) == 0x70a08231', 'smooth': {'type': 'cubicBezier'}},
{from: '41', to: '42', 'arrows': 'to', 'label': '', 'smooth': {'type': 'cubicBezier'}},
{from: '40', to: '41', 'arrows': 'to', 'label': 'True', 'smooth': {'type': 'cubicBezier'}},
{from: '39', to: '40', 'arrows': 'to', 'label': '', 'smooth': {'type': 'cubicBezier'}},
{from: '38', to: '39', 'arrows': 'to', 'label': 'callvalue == 0', 'smooth': {'type': 'cubicBezier'}},
{from: '38', to: '43', 'arrows': 'to', 'label': 'Not(callvalue == 0)', 'smooth': {'type': 'cubicBezier'}},
{from: '37', to: '38', 'arrows': 'to', 'label': 'Extract(0xff, 0xe0, calldata_Over_0) == 0xa3210e87', 'smooth': {'type': 'cubicBezier'}},
{from: '37', to: '44', 'arrows': 'to', 'label': 'Not(Extract(0xff, 0xe0, calldata_Over_0) == 0xa3210e87)', 'smooth': {'type': 'cubicBezier'}},
{from: '31', to: '37', 'arrows': 'to', 'label': 'Not(Extract(0xff, 0xe0, calldata_Over_0) == 0x70a08231)', 'smooth': {'type': 'cubicBezier'}},
{from: '25', to: '31', 'arrows': 'to', 'label': 'Not(Extract(0xff, 0xe0, calldata_Over_0) == 0x6241bfd1)', 'smooth': {'type': 'cubicBezier'}},
{from: '19', to: '25', 'arrows': 'to', 'label': 'Not(Extract(0xff, 0xe0, calldata_Over_0) == 0x18160ddd)', 'smooth': {'type': 'cubicBezier'}},
{from: '17', to: '19', 'arrows': 'to', 'label': 'ULE(4, calldatasize_Over)', 'smooth': {'type': 'cubicBezier'}}
];
</script>
</head>
<body>
<p>Mythril / LASER Symbolic VM</p>
<p><div id="mynetwork"></div><br/></p>
<script type="text/javascript">
var container = document.getElementById('mynetwork');
var nodesSet = new vis.DataSet(nodes);
var edgesSet = new vis.DataSet(edges);
var data = {'nodes': nodesSet, 'edges': edgesSet}
var gph = new vis.Network(container, data, options);
gph.on("click", function (params) {
// parse node id
var nodeID = params['nodes']['0'];
if (nodeID) {
var clickedNode = nodesSet.get(nodeID);
if(clickedNode.isExpanded) {
clickedNode.label = clickedNode.truncLabel;
}
else {
clickedNode.label = clickedNode.fullLabel;
}
clickedNode.isExpanded = !clickedNode.isExpanded;
nodesSet.update(clickedNode);
}
});
</script>
</body>
</html>

@ -0,0 +1,39 @@
{
"success": true,
"error": null,
"issues": [
{
"title": "Integer Underflow",
"description": "A possible integer underflow exists in the function sendeth(address,uint256).\nThe subtraction may result in a value < 0.",
"function": "sendeth(address,uint256)",
"type": "Warning",
"address": 649,
"debug": "<DEBUG-DATA>",
"filename": "<TESTDATA>/inputs/overflow.sol",
"lineno": 12,
"code": "balances[msg.sender] -= _value"
},
{
"title": "Integer Overflow ",
"description": "A possible integer overflow exists in the function sendeth(address,uint256).\n Addition will result in a lower value",
"function": "sendeth(address,uint256)",
"type": "Warning",
"address": 725,
"debug": "<DEBUG-DATA>",
"filename": "<TESTDATA>/inputs/overflow.sol",
"lineno": 13,
"code": "balances[_to] += _value"
},
{
"title": "Integer Underflow",
"description": "A possible integer underflow exists in the function sendeth(address,uint256).\nThe subtraction may result in a value < 0.",
"function": "sendeth(address,uint256)",
"type": "Warning",
"address": 567,
"debug": "<DEBUG-DATA>",
"filename": "<TESTDATA>/inputs/overflow.sol",
"lineno": 11,
"code": "balances[msg.sender] - _value"
}
]
}

@ -0,0 +1,46 @@
# Analysis Results
## Integer Underflow
- Type: Warning
- Contract: Over
- Function name: `sendeth(address,uint256)`
- PC address: 649
### Description
A possible integer underflow exists in the function sendeth(address,uint256).
The subtraction may result in a value < 0.
In *<TESTDATA>/inputs/overflow.sol:12*
```
balances[msg.sender] -= _value
```
## Integer Overflow
- Type: Warning
- Contract: Over
- Function name: `sendeth(address,uint256)`
- PC address: 725
### Description
A possible integer overflow exists in the function sendeth(address,uint256).
Addition will result in a lower value
In *<TESTDATA>/inputs/overflow.sol:13*
```
balances[_to] += _value
```
## Integer Underflow
- Type: Warning
- Contract: Over
- Function name: `sendeth(address,uint256)`
- PC address: 567
### Description
A possible integer underflow exists in the function sendeth(address,uint256).
The subtraction may result in a value < 0.
In *<TESTDATA>/inputs/overflow.sol:11*
```
balances[msg.sender] - _value
```

@ -0,0 +1,42 @@
==== Integer Underflow ====
Type: Warning
Contract: Over
Function name: sendeth(address,uint256)
PC address: 649
A possible integer underflow exists in the function sendeth(address,uint256).
The subtraction may result in a value < 0.
--------------------
In file: <TESTDATA>/inputs/overflow.sol:12
balances[msg.sender] -= _value
--------------------
==== Integer Overflow ====
Type: Warning
Contract: Over
Function name: sendeth(address,uint256)
PC address: 725
A possible integer overflow exists in the function sendeth(address,uint256).
Addition will result in a lower value
--------------------
In file: <TESTDATA>/inputs/overflow.sol:13
balances[_to] += _value
--------------------
==== Integer Underflow ====
Type: Warning
Contract: Over
Function name: sendeth(address,uint256)
PC address: 567
A possible integer underflow exists in the function sendeth(address,uint256).
The subtraction may result in a value < 0.
--------------------
In file: <TESTDATA>/inputs/overflow.sol:11
balances[msg.sender] - _value
--------------------
Loading…
Cancel
Save