|
|
@ -1,217 +1,96 @@ |
|
|
|
from z3 import Z3Exception, simplify |
|
|
|
|
|
|
|
from laser.ethereum.svm import NodeFlags |
|
|
|
|
|
|
|
import re |
|
|
|
import re |
|
|
|
|
|
|
|
|
|
|
|
default_title = '<p>Mythril / Ethereum LASER Symbolic VM</p>' |
|
|
|
from jinja2 import Environment, PackageLoader, select_autoescape |
|
|
|
|
|
|
|
from laser.ethereum.svm import NodeFlags |
|
|
|
default_style = ''' |
|
|
|
from z3 import Z3Exception, simplify |
|
|
|
<style type="text/css"> |
|
|
|
|
|
|
|
#mynetwork { |
|
|
|
|
|
|
|
background-color: #232625; |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
body { |
|
|
|
|
|
|
|
background-color: #232625; |
|
|
|
|
|
|
|
color: #ffffff; |
|
|
|
|
|
|
|
font-size: 10px; |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
</style> |
|
|
|
|
|
|
|
''' |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
default_opts = ''' |
|
|
|
default_opts = { |
|
|
|
var options = { |
|
|
|
'autoResize': True, |
|
|
|
autoResize: true, |
|
|
|
'height': '100%', |
|
|
|
height: '100%', |
|
|
|
'width': '100%', |
|
|
|
width: '100%', |
|
|
|
'manipulation': False, |
|
|
|
manipulation: false, |
|
|
|
'height': '90%', |
|
|
|
height: '90%', |
|
|
|
'layout': { |
|
|
|
layout: { |
|
|
|
'improvedLayout': True, |
|
|
|
randomSeed: undefined, |
|
|
|
'hierarchical': { |
|
|
|
improvedLayout:true, |
|
|
|
'enabled': True, |
|
|
|
hierarchical: { |
|
|
|
'levelSeparation': 450, |
|
|
|
enabled:true, |
|
|
|
'nodeSpacing': 200, |
|
|
|
levelSeparation: 450, |
|
|
|
'treeSpacing': 100, |
|
|
|
nodeSpacing: 200, |
|
|
|
'blockShifting': True, |
|
|
|
treeSpacing: 100, |
|
|
|
'edgeMinimization': True, |
|
|
|
blockShifting: true, |
|
|
|
'parentCentralization': False, |
|
|
|
edgeMinimization: true, |
|
|
|
'direction': 'LR', |
|
|
|
parentCentralization: false, |
|
|
|
'sortMethod': 'directed' |
|
|
|
direction: 'LR', // UD, DU, LR, RL |
|
|
|
|
|
|
|
sortMethod: 'directed' // hubsize, directed |
|
|
|
|
|
|
|
} |
|
|
|
} |
|
|
|
}, |
|
|
|
}, |
|
|
|
nodes:{ |
|
|
|
'nodes': { |
|
|
|
borderWidth: 1, |
|
|
|
'color': '#000000', |
|
|
|
borderWidthSelected: 2, |
|
|
|
'borderWidth': 1, |
|
|
|
chosen: true, |
|
|
|
'borderWidthSelected': 2, |
|
|
|
shape: 'box', |
|
|
|
'chosen': True, |
|
|
|
font: { |
|
|
|
'shape': 'box', |
|
|
|
align: 'left', |
|
|
|
'font': {'align': 'left', 'color': '#FFFFFF'}, |
|
|
|
color: '#FFFFFF', |
|
|
|
}, |
|
|
|
}, |
|
|
|
'edges': { |
|
|
|
}, |
|
|
|
'font': { |
|
|
|
edges:{ |
|
|
|
'color': '#FFFFFF', |
|
|
|
font: { |
|
|
|
'face': 'arial', |
|
|
|
color: '#ffffff', |
|
|
|
'background': 'none', |
|
|
|
size: 12, // px |
|
|
|
'strokeWidth': 0, |
|
|
|
face: 'arial', |
|
|
|
'strokeColor': '#ffffff', |
|
|
|
background: 'none', |
|
|
|
'align': 'horizontal', |
|
|
|
strokeWidth: 0, // px |
|
|
|
'multi': False, |
|
|
|
strokeColor: '#ffffff', |
|
|
|
'vadjust': 0, |
|
|
|
align: 'horizontal', |
|
|
|
|
|
|
|
multi: false, |
|
|
|
|
|
|
|
vadjust: 0, |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
}, |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
physics:{ |
|
|
|
|
|
|
|
enabled: [ENABLE_PHYSICS], |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
''' |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
phrack_style = ''' |
|
|
|
|
|
|
|
<style type="text/css"> |
|
|
|
|
|
|
|
#mynetwork { |
|
|
|
|
|
|
|
background-color: #ffffff; |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
body { |
|
|
|
|
|
|
|
background-color: #ffffff; |
|
|
|
|
|
|
|
color: #000000; |
|
|
|
|
|
|
|
font-size: 10px; |
|
|
|
|
|
|
|
font-family: "courier new"; |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
</style> |
|
|
|
|
|
|
|
''' |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
phrack_opts = ''' |
|
|
|
|
|
|
|
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:{ |
|
|
|
'physics': {'enabled': False} |
|
|
|
color: '#000000', |
|
|
|
} |
|
|
|
borderWidth: 1, |
|
|
|
|
|
|
|
borderWidthSelected: 1, |
|
|
|
phrack_opts = { |
|
|
|
shapeProperties: { |
|
|
|
'nodes': { |
|
|
|
borderDashes: false, // only for borders |
|
|
|
'color': '#000000', |
|
|
|
borderRadius: 0, // only for box shape |
|
|
|
'borderWidth': 1, |
|
|
|
}, |
|
|
|
'borderWidthSelected': 1, |
|
|
|
chosen: true, |
|
|
|
'shapeProperties': { |
|
|
|
shape: 'box', |
|
|
|
'borderDashes': False, |
|
|
|
font: { |
|
|
|
'borderRadius': 0, |
|
|
|
face: 'courier new', |
|
|
|
|
|
|
|
align: 'left', |
|
|
|
|
|
|
|
color: '#000000', |
|
|
|
|
|
|
|
}, |
|
|
|
}, |
|
|
|
}, |
|
|
|
'chosen': True, |
|
|
|
edges:{ |
|
|
|
'shape': 'box', |
|
|
|
font: { |
|
|
|
'font': {'face': 'courier new', 'align': 'left', 'color': '#000000'}, |
|
|
|
color: '#000000', |
|
|
|
}, |
|
|
|
face: 'courier new', |
|
|
|
'edges': { |
|
|
|
background: 'none', |
|
|
|
'font': { |
|
|
|
strokeWidth: 0, // px |
|
|
|
'color': '#000000', |
|
|
|
strokeColor: '#ffffff', |
|
|
|
'face': 'courier new', |
|
|
|
align: 'horizontal', |
|
|
|
'background': 'none', |
|
|
|
multi: false, |
|
|
|
'strokeWidth': 0, |
|
|
|
vadjust: 0, |
|
|
|
'strokeColor': '#ffffff', |
|
|
|
|
|
|
|
'align': 'horizontal', |
|
|
|
|
|
|
|
'multi': False, |
|
|
|
|
|
|
|
'vadjust': 0, |
|
|
|
} |
|
|
|
} |
|
|
|
}, |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
physics:{ |
|
|
|
|
|
|
|
enabled: [ENABLE_PHYSICS], |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
''' |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
graph_html = '''<html> |
|
|
|
|
|
|
|
<head> |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
[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> |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
[OPTS] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
[JS] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
</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; |
|
|
|
|
|
|
|
|
|
|
|
default_colors = [ |
|
|
|
nodesSet.update(clickedNode); |
|
|
|
{'border': '#26996f', 'background': '#2f7e5b', 'highlight': {'border': '#26996f', 'background': '#28a16f'}}, |
|
|
|
} |
|
|
|
{'border': '#9e42b3', 'background': '#842899', 'highlight': {'border': '#9e42b3', 'background': '#933da6'}}, |
|
|
|
}); |
|
|
|
{'border': '#b82323', 'background': '#991d1d', 'highlight': {'border': '#b82323', 'background': '#a61f1f'}}, |
|
|
|
</script> |
|
|
|
{'border': '#4753bf', 'background': '#3b46a1', 'highlight': {'border': '#4753bf', 'background': '#424db3'}}, |
|
|
|
</body> |
|
|
|
{'border': '#26996f', 'background': '#2f7e5b', 'highlight': {'border': '#26996f', 'background': '#28a16f'}}, |
|
|
|
</html> |
|
|
|
{'border': '#9e42b3', 'background': '#842899', 'highlight': {'border': '#9e42b3', 'background': '#933da6'}}, |
|
|
|
''' |
|
|
|
{'border': '#b82323', 'background': '#991d1d', 'highlight': {'border': '#b82323', 'background': '#a61f1f'}}, |
|
|
|
|
|
|
|
{'border': '#4753bf', 'background': '#3b46a1', 'highlight': {'border': '#4753bf', 'background': '#424db3'}}, |
|
|
|
colors = [ |
|
|
|
|
|
|
|
"{border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}", |
|
|
|
|
|
|
|
"{border: '#9e42b3', background: '#842899', highlight: {border: '#9e42b3', background: '#933da6'}}", |
|
|
|
|
|
|
|
"{border: '#b82323', background: '#991d1d', highlight: {border: '#b82323', background: '#a61f1f'}}", |
|
|
|
|
|
|
|
"{border: '#4753bf', background: '#3b46a1', highlight: {border: '#4753bf', background: '#424db3'}}", |
|
|
|
|
|
|
|
"{border: '#26996f', background: '#2f7e5b', highlight: {border: '#26996f', background: '#28a16f'}}", |
|
|
|
|
|
|
|
"{border: '#9e42b3', background: '#842899', highlight: {border: '#9e42b3', background: '#933da6'}}", |
|
|
|
|
|
|
|
"{border: '#b82323', background: '#991d1d', highlight: {border: '#b82323', background: '#a61f1f'}}", |
|
|
|
|
|
|
|
"{border: '#4753bf', background: '#3b46a1', highlight: {border: '#4753bf', background: '#424db3'}}", |
|
|
|
|
|
|
|
] |
|
|
|
] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
phrack_color = {'border': '#000000', 'background': '#ffffff', |
|
|
|
|
|
|
|
'highlight': {'border': '#000000', 'background': '#ffffff'}} |
|
|
|
|
|
|
|
|
|
|
|
def serialize(statespace, color_map): |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def extract_nodes(statespace, color_map): |
|
|
|
nodes = [] |
|
|
|
nodes = [] |
|
|
|
edges = [] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
for node_key in statespace.nodes: |
|
|
|
for node_key in statespace.nodes: |
|
|
|
|
|
|
|
|
|
|
|
node = statespace.nodes[node_key] |
|
|
|
node = statespace.nodes[node_key] |
|
|
@ -223,16 +102,31 @@ def serialize(statespace, color_map): |
|
|
|
code = re.sub("JUMPDEST", node.function_name, code) |
|
|
|
code = re.sub("JUMPDEST", node.function_name, code) |
|
|
|
|
|
|
|
|
|
|
|
code_split = code.split("\\n") |
|
|
|
code_split = code.split("\\n") |
|
|
|
|
|
|
|
code_split = [x for x in code_split if x] |
|
|
|
|
|
|
|
full_code = '\n'.join(code_split) |
|
|
|
|
|
|
|
|
|
|
|
truncated_code = code if (len(code_split) < 7) else "\\n".join(code_split[:6]) + "\\n(click to expand +)" |
|
|
|
truncated_code = '\n'.join(code_split) if (len(code_split) < 7) else '\n'.join(code_split[:6]) + "\n(click to expand +)" |
|
|
|
|
|
|
|
|
|
|
|
color = color_map[node.get_cfg_dict()['contract_name']] |
|
|
|
color = color_map[node.get_cfg_dict()['contract_name']] |
|
|
|
|
|
|
|
|
|
|
|
nodes.append("{id: '" + str(node_key) + "', color: " + color + ", size: 150, 'label': '" + truncated_code + "', 'fullLabel': '" + code + "', 'truncLabel': '" + truncated_code + "', 'isExpanded': false}") |
|
|
|
nodes.append({ |
|
|
|
|
|
|
|
'id': str(node_key), |
|
|
|
|
|
|
|
'color': color, |
|
|
|
|
|
|
|
'size': 150, |
|
|
|
|
|
|
|
'label': truncated_code, |
|
|
|
|
|
|
|
'fullLabel': full_code, |
|
|
|
|
|
|
|
'truncLabel': truncated_code, |
|
|
|
|
|
|
|
'isExpanded': False |
|
|
|
|
|
|
|
}) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
return nodes |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def extract_edges(statespace): |
|
|
|
|
|
|
|
edges = [] |
|
|
|
for edge in statespace.edges: |
|
|
|
for edge in statespace.edges: |
|
|
|
|
|
|
|
|
|
|
|
if (edge.condition is None): |
|
|
|
if edge.condition is None: |
|
|
|
label = "" |
|
|
|
label = "" |
|
|
|
else: |
|
|
|
else: |
|
|
|
|
|
|
|
|
|
|
@ -242,38 +136,52 @@ def serialize(statespace, color_map): |
|
|
|
label = str(edge.condition).replace("\n", "") |
|
|
|
label = str(edge.condition).replace("\n", "") |
|
|
|
|
|
|
|
|
|
|
|
label = re.sub("([^_])([\d]{2}\d+)", lambda m: m.group(1) + hex(int(m.group(2))), label) |
|
|
|
label = re.sub("([^_])([\d]{2}\d+)", lambda m: m.group(1) + hex(int(m.group(2))), label) |
|
|
|
code = re.sub("([0-9a-f]{8})[0-9a-f]+", lambda m: m.group(1) + "(...)", code) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
edges.append("{from: '" + str(edge.as_dict()['from']) + "', to: '" + str(edge.as_dict()['to']) + "', 'arrows': 'to', 'label': '" + label + "', 'smooth': {'type': 'cubicBezier'}}") |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
return "var nodes = [\n" + ",\n".join(nodes) + "\n];\nvar edges = [\n" + ",\n".join(edges) + "\n];" |
|
|
|
edges.append({ |
|
|
|
|
|
|
|
'from': str(edge.as_dict()['from']), |
|
|
|
|
|
|
|
'to': str(edge.as_dict()['to']), |
|
|
|
|
|
|
|
'arrows': 'to', |
|
|
|
|
|
|
|
'label': label, |
|
|
|
|
|
|
|
'smooth': {'type': 'cubicBezier'} |
|
|
|
|
|
|
|
}) |
|
|
|
|
|
|
|
return edges |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def generate_graph(statespace, physics=False, phrackify=False): |
|
|
|
def generate_graph(statespace, physics=False, phrackify=False, opts=None): |
|
|
|
''' |
|
|
|
''' |
|
|
|
This is some of the the ugliest code in the whole project. |
|
|
|
This is some of the the ugliest code in the whole project. |
|
|
|
At some point someone needs to write a templating system. |
|
|
|
At some point someone needs to write a templating system. |
|
|
|
''' |
|
|
|
''' |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
if opts is None: |
|
|
|
|
|
|
|
opts = {} |
|
|
|
|
|
|
|
env = Environment( |
|
|
|
|
|
|
|
loader=PackageLoader('mythril.analysis'), |
|
|
|
|
|
|
|
autoescape=select_autoescape(['html', 'xml']) |
|
|
|
|
|
|
|
) |
|
|
|
|
|
|
|
template = env.get_template('graph.html') |
|
|
|
|
|
|
|
|
|
|
|
color_map = {} |
|
|
|
color_map = {} |
|
|
|
|
|
|
|
graph_opts = default_opts |
|
|
|
|
|
|
|
|
|
|
|
if phrackify: |
|
|
|
if phrackify: |
|
|
|
|
|
|
|
graph_opts.update(phrack_opts) |
|
|
|
for k in statespace.accounts: |
|
|
|
for k in statespace.accounts: |
|
|
|
color_map[statespace.accounts[k].contract_name] = "{border: '#000000', background: '#ffffff', highlight: {border: '#000000', background: '#ffffff'}}" |
|
|
|
color_map[statespace.accounts[k].contract_name] = phrack_color |
|
|
|
|
|
|
|
|
|
|
|
html = graph_html.replace("[STYLE]", phrack_style).replace("[OPTS]", phrack_opts) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
else: |
|
|
|
else: |
|
|
|
|
|
|
|
|
|
|
|
i = 0 |
|
|
|
i = 0 |
|
|
|
|
|
|
|
|
|
|
|
for k in statespace.accounts: |
|
|
|
for k in statespace.accounts: |
|
|
|
color_map[statespace.accounts[k].contract_name] = colors[i] |
|
|
|
color_map[statespace.accounts[k].contract_name] = default_colors[i] |
|
|
|
i += 1 |
|
|
|
i += 1 |
|
|
|
|
|
|
|
|
|
|
|
html = graph_html.replace("[STYLE]", default_style).replace("[OPTS]", default_opts) |
|
|
|
graph_opts.update(opts) |
|
|
|
|
|
|
|
graph_opts['physics']['enabled'] = physics |
|
|
|
|
|
|
|
|
|
|
|
html = html.replace("[JS]", serialize(statespace, color_map)).replace("[ENABLE_PHYSICS]", str(physics).lower()) |
|
|
|
nodes = extract_nodes(statespace, color_map) |
|
|
|
|
|
|
|
|
|
|
|
return html |
|
|
|
return template.render(title="Mythril / Ethereum LASER Symbolic VM", |
|
|
|
|
|
|
|
nodes=extract_nodes(statespace, color_map), |
|
|
|
|
|
|
|
edges=extract_edges(statespace), |
|
|
|
|
|
|
|
phrackify=phrackify, |
|
|
|
|
|
|
|
opts=graph_opts |
|
|
|
|
|
|
|
) |
|
|
|