mirror of https://github.com/ConsenSys/mythril
Merge branch 'joshuata/templating' of git://github.com/joshuata/mythril
commit
9adcf06914
@ -1,279 +1,162 @@ |
|||||||
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 |
||||||
|
import z3 |
||||||
default_style = ''' |
|
||||||
<style type="text/css"> |
default_opts = { |
||||||
#mynetwork { |
'autoResize': True, |
||||||
background-color: #232625; |
'height': '100%', |
||||||
} |
'width': '100%', |
||||||
|
'manipulation': False, |
||||||
body { |
'layout': { |
||||||
background-color: #232625; |
'improvedLayout': True, |
||||||
color: #ffffff; |
'hierarchical': { |
||||||
font-size: 10px; |
'enabled': True, |
||||||
} |
'levelSeparation': 450, |
||||||
</style> |
'nodeSpacing': 200, |
||||||
''' |
'treeSpacing': 100, |
||||||
|
'blockShifting': True, |
||||||
default_opts = ''' |
'edgeMinimization': True, |
||||||
var options = { |
'parentCentralization': False, |
||||||
autoResize: true, |
'direction': 'LR', |
||||||
height: '100%', |
'sortMethod': 'directed' |
||||||
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:{ |
'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; |
|
||||||
} |
default_colors = [ |
||||||
|
{'border': '#26996f', 'background': '#2f7e5b', 'highlight': {'border': '#26996f', 'background': '#28a16f'}}, |
||||||
clickedNode.isExpanded = !clickedNode.isExpanded; |
{'border': '#9e42b3', 'background': '#842899', 'highlight': {'border': '#9e42b3', 'background': '#933da6'}}, |
||||||
|
{'border': '#b82323', 'background': '#991d1d', 'highlight': {'border': '#b82323', 'background': '#a61f1f'}}, |
||||||
nodesSet.update(clickedNode); |
{'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'}}, |
||||||
</script> |
{'border': '#b82323', 'background': '#991d1d', 'highlight': {'border': '#b82323', 'background': '#a61f1f'}}, |
||||||
</body> |
{'border': '#4753bf', 'background': '#3b46a1', 'highlight': {'border': '#4753bf', 'background': '#424db3'}}, |
||||||
</html> |
|
||||||
''' |
|
||||||
|
|
||||||
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] |
||||||
|
instructions = [state.get_current_instruction() for state in node.states] |
||||||
code = node.get_cfg_dict()['code'] |
code_split = [] |
||||||
code = re.sub("([0-9a-f]{8})[0-9a-f]+", lambda m: m.group(1) + "(...)", code) |
for instruction in instructions: |
||||||
|
if instruction['opcode'].startswith("PUSH"): |
||||||
if NodeFlags.FUNC_ENTRY in node.flags: |
code_split.append(f"{instruction['address']} {instruction['opcode']} {instruction['argument']}") |
||||||
code = re.sub("JUMPDEST", node.function_name, code) |
elif instruction['opcode'].startswith("JUMPDEST"): |
||||||
|
code_split.append(f"{instruction['address']} {instruction['opcode']} {node.function_name}") |
||||||
code_split = code.split("\\n") |
else: |
||||||
|
code_split.append(f"{instruction['address']} {instruction['opcode']}") |
||||||
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( |
||||||
color = color_map[node.get_cfg_dict()['contract_name']] |
code_split[:6]) + "\n(click to expand +)" |
||||||
|
|
||||||
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_map[node.get_cfg_dict()['contract_name']], |
||||||
|
'size': 150, |
||||||
|
'fullLabel': '\n'.join(code_split), |
||||||
|
'label': truncated_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: |
||||||
|
|
||||||
try: |
try: |
||||||
label = str(simplify(edge.condition)).replace("\n", "") |
label = str(z3.simplify(edge.condition)).replace("\n", "") |
||||||
except Z3Exception: |
except z3.Z3Exception: |
||||||
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(r'([^_])([\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, title="Mythril / Ethereum LASER Symbolic VM", physics=False, phrackify=False): |
||||||
''' |
env = Environment(loader=PackageLoader('mythril.analysis'), autoescape=select_autoescape(['html', 'xml'])) |
||||||
This is some of the the ugliest code in the whole project. |
template = env.get_template('graph.html') |
||||||
At some point someone needs to write a templating system. |
|
||||||
''' |
|
||||||
|
|
||||||
color_map = {} |
graph_opts = default_opts |
||||||
|
accounts = statespace.accounts |
||||||
|
|
||||||
if phrackify: |
if phrackify: |
||||||
|
color_map = {accounts[k].contract_name: phrack_color for k in accounts} |
||||||
for k in statespace.accounts: |
graph_opts.update(phrack_opts) |
||||||
color_map[statespace.accounts[k].contract_name] = "{border: '#000000', background: '#ffffff', highlight: {border: '#000000', background: '#ffffff'}}" |
|
||||||
|
|
||||||
html = graph_html.replace("[STYLE]", phrack_style).replace("[OPTS]", phrack_opts) |
|
||||||
|
|
||||||
else: |
else: |
||||||
|
color_map = {accounts[k].contract_name: default_colors[i % len(default_colors)] for i, k in enumerate(accounts)} |
||||||
|
|
||||||
i = 0 |
graph_opts['physics']['enabled'] = physics |
||||||
|
|
||||||
for k in statespace.accounts: |
|
||||||
color_map[statespace.accounts[k].contract_name] = colors[i] |
|
||||||
i += 1 |
|
||||||
|
|
||||||
html = graph_html.replace("[STYLE]", default_style).replace("[OPTS]", default_opts) |
|
||||||
|
|
||||||
html = html.replace("[JS]", serialize(statespace, color_map)).replace("[ENABLE_PHYSICS]", str(physics).lower()) |
|
||||||
|
|
||||||
return html |
return template.render(title=title, |
||||||
|
nodes=extract_nodes(statespace, color_map), |
||||||
|
edges=extract_edges(statespace), |
||||||
|
phrackify=phrackify, |
||||||
|
opts=graph_opts |
||||||
|
) |
||||||
|
@ -0,0 +1,68 @@ |
|||||||
|
<html> |
||||||
|
<head> |
||||||
|
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/vis/4.21.0/vis.min.css" integrity="sha256-iq5ygGJ7021Pi7H5S+QAUXCPUfaBzfqeplbg/KlEssg=" crossorigin="anonymous" /> |
||||||
|
<script src="https://cdnjs.cloudflare.com/ajax/libs/vis/4.21.0/vis.min.js" integrity="sha256-JuQeAGbk9rG/EoRMixuy5X8syzICcvB0dj3KindZkY0=" crossorigin="anonymous"></script> |
||||||
|
|
||||||
|
{% if not phrackify %} |
||||||
|
<style type="text/css"> |
||||||
|
#mynetwork { |
||||||
|
background-color: #232625; |
||||||
|
} |
||||||
|
body { |
||||||
|
background-color: #232625; |
||||||
|
color: #ffffff; |
||||||
|
font-size: 10px; |
||||||
|
} |
||||||
|
</style> |
||||||
|
{% else %} |
||||||
|
<style type="text/css"> |
||||||
|
#mynetwork { |
||||||
|
background-color: #ffffff; |
||||||
|
} |
||||||
|
body { |
||||||
|
background-color: #ffffff; |
||||||
|
color: #000000; |
||||||
|
font-size: 10px; |
||||||
|
font-family: "courier new"; |
||||||
|
} |
||||||
|
</style> |
||||||
|
{% endif %} |
||||||
|
|
||||||
|
<script> |
||||||
|
var options = {{opts | tojson}}; |
||||||
|
var nodes = {{nodes | tojson}}; |
||||||
|
var edges = {{edges | tojson}}; |
||||||
|
</script> |
||||||
|
</head> |
||||||
|
<body> |
||||||
|
<p>{{ title }}</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> |
Loading…
Reference in new issue