Merge branch 'bounded_loops' of github.com:ConsenSys/mythril into bounded_loops

pull/1060/head
Bernhard Mueller 6 years ago
commit 3eb9ebbcd9
  1. 6
      .circleci/config.yml
  2. 6
      docs/source/about.rst
  3. 2
      docs/source/analysis-modules.rst
  4. 20
      docs/source/conf.py
  5. 2
      docs/source/create-module.rst
  6. 2
      docs/source/index.rst
  7. 22
      docs/source/module-list.rst
  8. 2
      docs/source/security-analysis.rst
  9. 2
      mythril/__version__.py
  10. 10
      mythril/analysis/modules/suicide.py

@ -89,10 +89,10 @@ jobs:
working_directory: /home working_directory: /home
steps: steps:
- checkout: - checkout:
path: /home/mythril-classic path: /home/mythril
- run: - run:
name: Builds `mythril-classic` name: Builds `mythril`
command: cd mythril-classic && python3 setup.py install command: cd mythril && python3 setup.py install
- run: - run:
name: Installs other MythX components name: Installs other MythX components
command: | command: |

@ -1,6 +1,6 @@
What is Mythril Classic? What is Mythril?
======================== ========================
Mythril Classic is a security analysis tool for Ethereum smart contracts. It was `introduced at HITBSecConf 2018 <https://github.com/b-mueller/smashing-smart-contracts/blob/master/smashing-smart-contracts-1of1.pdf>`_. Mythril is a security analysis tool for Ethereum smart contracts. It was `introduced at HITBSecConf 2018 <https://github.com/b-mueller/smashing-smart-contracts/blob/master/smashing-smart-contracts-1of1.pdf>`_.
Mythril Classic detects a range of security issues, including integer underflows, owner-overwrite-to-Ether-withdrawal, and others. Note that Mythril is targeted at finding common vulnerabilities, and is not able to discover issues in the business logic of an application. Furthermore, Mythril and symbolic executors are generally unsound, as they are often unable to explore all possible states of a program. Mythril detects a range of security issues, including integer underflows, owner-overwrite-to-Ether-withdrawal, and others. Note that Mythril is targeted at finding common vulnerabilities, and is not able to discover issues in the business logic of an application. Furthermore, Mythril and symbolic executors are generally unsound, as they are often unable to explore all possible states of a program.

@ -1,7 +1,7 @@
Analysis Modules Analysis Modules
================ ================
Mythril Classic's detection capabilities are written in modules in the `/analysis/modules <https://github.com/ConsenSys/mythril-classic/tree/master/mythril/analysis/modules>`_ directory. Mythril's detection capabilities are written in modules in the `/analysis/modules <https://github.com/ConsenSys/mythril/tree/master/mythril/analysis/modules>`_ directory.
.. toctree:: .. toctree::

@ -108,7 +108,7 @@ html_static_path = ["_static"]
# -- Options for HTMLHelp output --------------------------------------------- # -- Options for HTMLHelp output ---------------------------------------------
# Output file base name for HTML help builder. # Output file base name for HTML help builder.
htmlhelp_basename = "MythrilClassicdoc" htmlhelp_basename = "Mythrildoc"
# -- Options for LaTeX output ------------------------------------------------ # -- Options for LaTeX output ------------------------------------------------
@ -132,13 +132,7 @@ latex_elements = {
# (source start file, target name, title, # (source start file, target name, title,
# author, documentclass [howto, manual, or own class]). # author, documentclass [howto, manual, or own class]).
latex_documents = [ latex_documents = [
( (master_doc, "Mythril.tex", "Mythril Documentation", "Bernhard Mueller", "manual")
master_doc,
"MythrilClassic.tex",
"Mythril Classic Documentation",
"Bernhard Mueller",
"manual",
)
] ]
@ -146,9 +140,7 @@ latex_documents = [
# One entry per manual page. List of tuples # One entry per manual page. List of tuples
# (source start file, name, description, authors, manual section). # (source start file, name, description, authors, manual section).
man_pages = [ man_pages = [(master_doc, "mythril", "Mythril Documentation", [author], 1)]
(master_doc, "mythrilclassic", "Mythril Classic Documentation", [author], 1)
]
# -- Options for Texinfo output ---------------------------------------------- # -- Options for Texinfo output ----------------------------------------------
@ -159,10 +151,10 @@ man_pages = [
texinfo_documents = [ texinfo_documents = [
( (
master_doc, master_doc,
"MythrilClassic", "Mythril",
"Mythril Classic Documentation", "Mythril Documentation",
author, author,
"MythrilClassic", "Mythril",
"One line description of project.", "One line description of project.",
"Miscellaneous", "Miscellaneous",
) )

@ -1,4 +1,4 @@
Creating a Module Creating a Module
================= =================
Create a module in the :code:`analysis/modules` directory, and create an instance of a class that inherits :code:`DetectionModule` named :code:`detector`. Take a look at the `suicide module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/suicide.py>`_ as an example. Create a module in the :code:`analysis/modules` directory, and create an instance of a class that inherits :code:`DetectionModule` named :code:`detector`. Take a look at the `suicide module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/suicide.py>`_ as an example.

@ -1,4 +1,4 @@
Welcome to Mythril Classic's documentation! Welcome to Mythril's documentation!
=========================================== ===========================================
.. toctree:: .. toctree::

@ -5,65 +5,65 @@ Modules
Delegate Call To Untrusted Contract Delegate Call To Untrusted Contract
*********************************** ***********************************
The `delegatecall module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/delegatecall.py>`_ detects `SWC-112 (DELEGATECALL to Untrusted Callee) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-112>`_. The `delegatecall module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/delegatecall.py>`_ detects `SWC-112 (DELEGATECALL to Untrusted Callee) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-112>`_.
*********************************** ***********************************
Dependence on Predictable Variables Dependence on Predictable Variables
*********************************** ***********************************
The `predictable variables module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/dependence_on_predictable_vars.py>`_ detects `SWC-120 (Weak Randomness) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-120>`_ and `SWC-116 (Timestamp Dependence) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-116>`_. The `predictable variables module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/dependence_on_predictable_vars.py>`_ detects `SWC-120 (Weak Randomness) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-120>`_ and `SWC-116 (Timestamp Dependence) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-116>`_.
****************** ******************
Deprecated Opcodes Deprecated Opcodes
****************** ******************
The `deprecated opcodes module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/deprecated_ops.py>`_ detects `SWC-111 (Use of Deprecated Functions) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-111>`_. The `deprecated opcodes module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/deprecated_ops.py>`_ detects `SWC-111 (Use of Deprecated Functions) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-111>`_.
*********** ***********
Ether Thief Ether Thief
*********** ***********
The `Ether Thief module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/ether_thief.py>`_ detects `SWC-105 (Unprotected Ether Withdrawal) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-105>`_. The `Ether Thief module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/ether_thief.py>`_ detects `SWC-105 (Unprotected Ether Withdrawal) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-105>`_.
********** **********
Exceptions Exceptions
********** **********
The `exceptions module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/exceptions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_. The `exceptions module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/exceptions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_.
************** **************
External Calls External Calls
************** **************
The `external calls module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/external_calls.py>`_ warns about `SWC-117 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting calls to external contracts. The `external calls module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/external_calls.py>`_ warns about `SWC-117 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting calls to external contracts.
******* *******
Integer Integer
******* *******
The `integer module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/integer.py>`_ detects `SWC-101 (Integer Overflow and Underflow) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-101>`_. The `integer module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/integer.py>`_ detects `SWC-101 (Integer Overflow and Underflow) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-101>`_.
************** **************
Multiple Sends Multiple Sends
************** **************
The `multiple sends module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/multiple_sends.py>`_ detects `SWC-113 (Denial of Service with Failed Call) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-113>`_ by checking for multiple calls or sends in a single transaction. The `multiple sends module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/multiple_sends.py>`_ detects `SWC-113 (Denial of Service with Failed Call) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-113>`_ by checking for multiple calls or sends in a single transaction.
******* *******
Suicide Suicide
******* *******
The `suicide module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/suicide.py>`_ detects `SWC-106 (Unprotected SELFDESTRUCT) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-106>`_. The `suicide module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/suicide.py>`_ detects `SWC-106 (Unprotected SELFDESTRUCT) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-106>`_.
**************************** ****************************
State Change External Calls State Change External Calls
**************************** ****************************
The `state change external calls module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/state_change_external_calls.py>`_ detects `SWC-107 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting state change after calls to an external contract. The `state change external calls module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/state_change_external_calls.py>`_ detects `SWC-107 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting state change after calls to an external contract.
**************** ****************
Unchecked Retval Unchecked Retval
**************** ****************
The `unchecked retval module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_. The `unchecked retval module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_.

@ -1,7 +1,7 @@
Security Analysis Security Analysis
================= =================
Run :code:`myth -x` with one of the input options described below will run the analysis modules in the `/analysis/modules <https://github.com/ConsenSys/mythril-classic/tree/master/mythril/analysis/modules>`_ directory. Run :code:`myth -x` with one of the input options described below will run the analysis modules in the `/analysis/modules <https://github.com/ConsenSys/mythril/tree/master/mythril/analysis/modules>`_ directory.
*********************** ***********************
Analyzing Solidity Code Analyzing Solidity Code

@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
as for importing into Python. as for importing into Python.
""" """
__version__ = "v0.20.8" __version__ = "v0.20.9"

@ -4,6 +4,7 @@ from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT
from mythril.exceptions import UnsatError from mythril.exceptions import UnsatError
from mythril.analysis.modules.base import DetectionModule from mythril.analysis.modules.base import DetectionModule
from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
import logging import logging
import json import json
@ -57,13 +58,16 @@ class SuicideModule(DetectionModule):
) )
description_head = "The contract can be killed by anyone." description_head = "The contract can be killed by anyone."
caller = state.current_transaction.caller
try: try:
try: try:
transaction_sequence = solver.get_transaction_sequence( transaction_sequence = solver.get_transaction_sequence(
state, state,
state.mstate.constraints state.mstate.constraints
+ [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF], + [
to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF,
caller == ATTACKER_ADDRESS,
],
) )
description_tail = ( description_tail = (
"Anyone can kill this contract and withdraw its balance to an arbitrary " "Anyone can kill this contract and withdraw its balance to an arbitrary "
@ -71,7 +75,7 @@ class SuicideModule(DetectionModule):
) )
except UnsatError: except UnsatError:
transaction_sequence = solver.get_transaction_sequence( transaction_sequence = solver.get_transaction_sequence(
state, state.mstate.constraints state, state.mstate.constraints + [caller == ATTACKER_ADDRESS]
) )
description_tail = "Arbitrary senders can kill this contract." description_tail = "Arbitrary senders can kill this contract."

Loading…
Cancel
Save