Merge pull request #1340 from ConsenSys/modules_usability

Modules selection usability overhaul

mythril/analysis/module/base.py

@@ -42,7 +42,7 @@ class DetectionModule(ABC):
     - post_hooks: A list of instructions to hook the laser vm for (post execution of the instruction)
     """
 
-    name = "Detection Module Name"
+    name = "Detection Module Name / Title"
     swc_id = "SWC-000"
     description = "Detection module description"
     entry_point = EntryPoint.CALLBACK  # type: EntryPoint

mythril/analysis/module/loader.py

@@ -3,23 +3,27 @@ from mythril.support.support_utils import Singleton
 
 from mythril.analysis.module.modules.arbitrary_jump import ArbitraryJump
 from mythril.analysis.module.modules.arbitrary_write import ArbitraryStorage
-from mythril.analysis.module.modules.delegatecall import DelegateCallModule
+from mythril.analysis.module.modules.delegatecall import ArbitraryDelegateCall
 from mythril.analysis.module.modules.dependence_on_predictable_vars import (
-    PredictableDependenceModule,
+    PredictableVariables,
 )
-from mythril.analysis.module.modules.deprecated_ops import DeprecatedOperationsModule
+from mythril.analysis.module.modules.deprecated_ops import DeprecatedOperations
 from mythril.analysis.module.modules.ether_thief import EtherThief
-from mythril.analysis.module.modules.exceptions import ReachableExceptionsModule
+from mythril.analysis.module.modules.exceptions import Exceptions
 from mythril.analysis.module.modules.external_calls import ExternalCalls
-from mythril.analysis.module.modules.integer import IntegerOverflowUnderflowModule
-from mythril.analysis.module.modules.multiple_sends import MultipleSendsModule
-from mythril.analysis.module.modules.state_change_external_calls import StateChange
-from mythril.analysis.module.modules.suicide import SuicideModule
-from mythril.analysis.module.modules.unchecked_retval import UncheckedRetvalModule
+from mythril.analysis.module.modules.integer import IntegerArithmetics
+from mythril.analysis.module.modules.multiple_sends import MultipleSends
+from mythril.analysis.module.modules.state_change_external_calls import (
+    StateChangeAfterCall,
+)
+from mythril.analysis.module.modules.suicide import AccidentallyKillable
+from mythril.analysis.module.modules.unchecked_retval import UncheckedRetval
 from mythril.analysis.module.modules.user_assertions import UserAssertions
 
 from mythril.analysis.module.base import EntryPoint
 
+from mythril.exceptions import DetectorNotFoundError
+
 from typing import Optional, List
 
 
@@ -53,11 +57,28 @@ class ModuleLoader(object, metaclass=Singleton):
         :param white_list: If specified: only return whitelisted detection modules
         :return: The selected detection modules
         """
+
         result = self._modules[:]
+
+        if white_list:
+
+            # Sanity check
+
+            available_names = [type(module).__name__ for module in result]
+
+            for name in white_list:
+                if name not in available_names:
+                    raise DetectorNotFoundError(
+                        "Invalid detection module: {}".format(name)
+                    )
+
+            result = [
+                module for module in result if type(module).__name__ in white_list
+            ]
+
         if entry_point:
             result = [module for module in result if module.entry_point == entry_point]
-        if white_list:
-            result = [module for module in result if module.name in white_list]
+
         return result
 
     def _register_mythril_modules(self):
@@ -65,17 +86,17 @@ class ModuleLoader(object, metaclass=Singleton):
             [
                 ArbitraryJump(),
                 ArbitraryStorage(),
-                DelegateCallModule(),
-                PredictableDependenceModule(),
-                DeprecatedOperationsModule(),
+                ArbitraryDelegateCall(),
+                PredictableVariables(),
+                DeprecatedOperations(),
                 EtherThief(),
-                ReachableExceptionsModule(),
+                Exceptions(),
                 ExternalCalls(),
-                IntegerOverflowUnderflowModule(),
-                MultipleSendsModule(),
-                StateChange(),
-                SuicideModule(),
-                UncheckedRetvalModule(),
+                IntegerArithmetics(),
+                MultipleSends(),
+                StateChangeAfterCall(),
+                AccidentallyKillable(),
+                UncheckedRetval(),
                 UserAssertions(),
             ]
         )

mythril/analysis/module/modules/arbitrary_jump.py

@@ -9,14 +9,14 @@ log = logging.getLogger(__name__)
 
 DESCRIPTION = """
 
-Search for any writes to an arbitrary storage slot
+Search for jumps to arbitrary locations in the bytecode
 """
 
 
 class ArbitraryJump(DetectionModule):
     """This module searches for JUMPs to an arbitrary instruction."""
 
-    name = "Jump to an arbitrary line"
+    name = "Jump to an arbitrary bytecode location"
     swc_id = ARBITRARY_JUMP
     description = DESCRIPTION
     entry_point = EntryPoint.CALLBACK

mythril/analysis/module/modules/arbitrary_write.py

@@ -21,7 +21,7 @@ Search for any writes to an arbitrary storage slot
 class ArbitraryStorage(DetectionModule):
     """This module searches for a feasible write to an arbitrary storage slot."""
 
-    name = "Arbitrary Storage Write"
+    name = "Write to an arbitrary storage location"
     swc_id = WRITE_TO_ARBITRARY_STORAGE
     description = DESCRIPTION
     entry_point = EntryPoint.CALLBACK

mythril/analysis/module/modules/delegatecall.py

@@ -19,10 +19,10 @@ from mythril.laser.smt import symbol_factory, UGT
 log = logging.getLogger(__name__)
 
 
-class DelegateCallModule(DetectionModule):
+class ArbitraryDelegateCall(DetectionModule):
     """This module detects calldata being forwarded using DELEGATECALL."""
 
-    name = "DELEGATECALL Usage in Fallback Function"
+    name = "Delegatecall to a user-specified address"
     swc_id = DELEGATECALL_TO_UNTRUSTED_CONTRACT
     description = (
         "Check for invocations of delegatecall(msg.data) in the fallback function."
@@ -100,4 +100,4 @@ class DelegateCallModule(DetectionModule):
             return []
 
 
-detector = DelegateCallModule()
+detector = ArbitraryDelegateCall()

mythril/analysis/module/modules/dependence_on_predictable_vars.py

@@ -45,11 +45,11 @@ class OldBlockNumberUsedAnnotation(StateAnnotation):
         pass
 
 
-class PredictableDependenceModule(DetectionModule):
+class PredictableVariables(DetectionModule):
     """This module detects whether control flow decisions are made using predictable
     parameters."""
 
-    name = "Dependence of Predictable Variables"
+    name = "Control flow depends on a predictable environment variable"
     swc_id = "{} {}".format(TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS)
     description = (
         "Check whether important control flow decisions are influenced by block.coinbase,"
@@ -227,4 +227,4 @@ class PredictableDependenceModule(DetectionModule):
         return issues
 
 
-detector = PredictableDependenceModule()
+detector = PredictableVariables()

mythril/analysis/module/modules/deprecated_ops.py

@@ -15,10 +15,10 @@ Check for usage of deprecated opcodes
 """
 
 
-class DeprecatedOperationsModule(DetectionModule):
+class DeprecatedOperations(DetectionModule):
     """This module checks for the usage of deprecated op codes."""
 
-    name = "Deprecated Operations"
+    name = "Usage of deprecated instructions"
     swc_id = DEPRECATED_FUNCTIONS_USAGE
     description = DESCRIPTION
     entry_point = EntryPoint.CALLBACK
@@ -87,4 +87,4 @@ class DeprecatedOperationsModule(DetectionModule):
         return [potential_issue]
 
 
-detector = DeprecatedOperationsModule()
+detector = DeprecatedOperations()

mythril/analysis/module/modules/ether_thief.py

@@ -36,7 +36,7 @@ class EtherThief(DetectionModule):
     """This module search for cases where Ether can be withdrawn to a user-
     specified address."""
 
-    name = "Ether Thief"
+    name = "Attacker can profitably withdraw Ether from the contract account"
     swc_id = UNPROTECTED_ETHER_WITHDRAWAL
     description = DESCRIPTION
     entry_point = EntryPoint.CALLBACK

mythril/analysis/module/modules/exceptions.py

@@ -11,10 +11,10 @@ from mythril.laser.ethereum.state.global_state import GlobalState
 log = logging.getLogger(__name__)
 
 
-class ReachableExceptionsModule(DetectionModule):
+class Exceptions(DetectionModule):
     """"""
 
-    name = "Reachable Exceptions"
+    name = "Exception or assertion violation"
     swc_id = ASSERT_VIOLATION
     description = "Checks whether any exception states are reachable."
     entry_point = EntryPoint.CALLBACK
@@ -76,4 +76,4 @@ class ReachableExceptionsModule(DetectionModule):
         return []
 
 
-detector = ReachableExceptionsModule()
+detector = Exceptions()

mythril/analysis/module/modules/external_calls.py

@@ -49,7 +49,7 @@ class ExternalCalls(DetectionModule):
     """This module searches for low level calls (e.g. call.value()) that
     forward all gas to the callee."""
 
-    name = "External calls"
+    name = "External call to another contract"
     swc_id = REENTRANCY
     description = DESCRIPTION
     entry_point = EntryPoint.CALLBACK

mythril/analysis/module/modules/integer.py

@@ -61,10 +61,10 @@ class OverUnderflowStateAnnotation(StateAnnotation):
         return new_annotation
 
 
-class IntegerOverflowUnderflowModule(DetectionModule):
+class IntegerArithmetics(DetectionModule):
     """This module searches for integer over- and underflows."""
 
-    name = "Integer Overflow and Underflow"
+    name = "Integer overflow or underflow"
     swc_id = INTEGER_OVERFLOW_AND_UNDERFLOW
     description = (
         "For every SUB instruction, check if there's a possible state "
@@ -337,7 +337,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
             self.issues.append(issue)
 
 
-detector = IntegerOverflowUnderflowModule()
+detector = IntegerArithmetics()
 
 
 def _get_address_from_state(state):

mythril/analysis/module/modules/multiple_sends.py

@@ -24,10 +24,10 @@ class MultipleSendsAnnotation(StateAnnotation):
         return result
 
 
-class MultipleSendsModule(DetectionModule):
+class MultipleSends(DetectionModule):
     """This module checks for multiple sends in a single transaction."""
 
-    name = "Multiple Sends"
+    name = "Multiple external calls in the same transaction"
     swc_id = MULTIPLE_SENDS
     description = "Check for multiple sends in a single transaction"
     entry_point = EntryPoint.CALLBACK
@@ -98,4 +98,4 @@ class MultipleSendsModule(DetectionModule):
         return []
 
 
-detector = MultipleSendsModule()
+detector = MultipleSends()

mythril/analysis/module/modules/state_change_external_calls.py

@@ -95,11 +95,11 @@ class StateChangeCallsAnnotation(StateAnnotation):
         )
 
 
-class StateChange(DetectionModule):
+class StateChangeAfterCall(DetectionModule):
     """This module searches for state change after low level calls (e.g. call.value()) that
     forward gas to the callee."""
 
-    name = "State Change After External calls"
+    name = "State change after an external call"
     swc_id = REENTRANCY
     description = DESCRIPTION
     entry_point = EntryPoint.CALLBACK
@@ -159,13 +159,13 @@ class StateChange(DetectionModule):
         # Record state changes following from a transfer of ether
         if op_code in CALL_LIST:
             value = global_state.mstate.stack[-3]  # type: BitVec
-            if StateChange._balance_change(value, global_state):
+            if StateChangeAfterCall._balance_change(value, global_state):
                 for annotation in annotations:
                     annotation.state_change_states.append(global_state)
 
         # Record external calls
         if op_code in CALL_LIST:
-            StateChange._add_external_call(global_state)
+            StateChangeAfterCall._add_external_call(global_state)
 
         # Check for vulnerabilities
         vulnerabilities = []
@@ -195,4 +195,4 @@ class StateChange(DetectionModule):
                 return False
 
 
-detector = StateChange()
+detector = StateChangeAfterCall()

mythril/analysis/module/modules/suicide.py

@@ -20,11 +20,11 @@ For kill-able contracts, also check whether it is possible to direct the contrac
 """
 
 
-class SuicideModule(DetectionModule):
+class AccidentallyKillable(DetectionModule):
     """This module checks if the contact can be 'accidentally' killed by
     anyone."""
 
-    name = "Unprotected Selfdestruct"
+    name = "Contract can be accidentally killed by anyone"
     swc_id = UNPROTECTED_SELFDESTRUCT
     description = DESCRIPTION
     entry_point = EntryPoint.CALLBACK
@@ -109,4 +109,4 @@ class SuicideModule(DetectionModule):
         return []
 
 
-detector = SuicideModule()
+detector = AccidentallyKillable()

mythril/analysis/module/modules/unchecked_retval.py

@@ -28,10 +28,10 @@ class UncheckedRetvalAnnotation(StateAnnotation):
         return result
 
 
-class UncheckedRetvalModule(DetectionModule):
+class UncheckedRetval(DetectionModule):
     """A detection module to test whether CALL return value is checked."""
 
-    name = "Unchecked Return Value"
+    name = "Return value of an external call is not checked"
     swc_id = UNCHECKED_RET_VAL
     description = (
         "Test whether CALL return value is checked. "
@@ -121,4 +121,4 @@ class UncheckedRetvalModule(DetectionModule):
         return []
 
 
-detector = UncheckedRetvalModule()
+detector = UncheckedRetval()

mythril/analysis/module/modules/user_assertions.py

@@ -28,7 +28,7 @@ assertion_failed_hash = (
 class UserAssertions(DetectionModule):
     """This module searches for user supplied exceptions: emit AssertionFailed("Error")."""
 
-    name = "User assertions"
+    name = "A user-defined assertion has been triggered"
     swc_id = ASSERT_VIOLATION
     description = DESCRIPTION
     entry_point = EntryPoint.CALLBACK

mythril/exceptions.py

@@ -39,3 +39,10 @@ class AddressNotFoundError(MythrilBaseException):
     found."""
 
     pass
+
+
+class DetectorNotFoundError(MythrilBaseException):
+    """A Mythril exception denoting attempted usage of a non-existant
+    detection module."""
+
+    pass

mythril/interfaces/cli.py

@@ -17,7 +17,11 @@ import traceback
 import mythril.support.signatures as sigs
 from argparse import ArgumentParser, Namespace, RawTextHelpFormatter
 from mythril import mythx
-from mythril.exceptions import AddressNotFoundError, CriticalError
+from mythril.exceptions import (
+    AddressNotFoundError,
+    DetectorNotFoundError,
+    CriticalError,
+)
 from mythril.laser.ethereum.transaction.symbolic import ACTORS
 from mythril.mythril import (
     MythrilAnalyzer,
@@ -25,6 +29,9 @@ from mythril.mythril import (
     MythrilConfig,
     MythrilLevelDB,
 )
+
+from mythril.analysis.module import ModuleLoader
+
 from mythril.__version__ import __version__ as VERSION
 
 ANALYZE_LIST = ("analyze", "a")
@@ -42,6 +49,7 @@ COMMAND_LIST = (
         "leveldb-search",
         "function-to-hash",
         "hash-to-address",
+        "list-detectors",
         "version",
         "truffle",
         "help",
@@ -225,6 +233,11 @@ def main() -> None:
     )
     create_pro_parser(pro_parser)
 
+    subparsers.add_parser(
+        "list-detectors",
+        parents=[output_parser],
+        help="Lists available detection modules",
+    )
     read_storage_parser = subparsers.add_parser(
         "read-storage",
         help="Retrieves storage slots from a given address through rpc",
@@ -735,9 +748,11 @@ def execute_command(
                     "markdown": report.as_markdown(),
                 }
                 print(outputs[args.outform])
-            except ModuleNotFoundError as e:
+            except DetectorNotFoundError as e:
+                exit_with_error(args.outform, format(e))
+            except CriticalError as e:
                 exit_with_error(
-                    args.outform, "Error loading analysis modules: " + format(e)
+                    args.outform, "Analysis error encountered: " + format(e)
                 )
 
     else:
@@ -778,6 +793,17 @@ def parse_args_and_execute(parser: ArgumentParser, args: Namespace) -> None:
             print("Mythril version {}".format(VERSION))
         sys.exit()
 
+    if args.command == "list-detectors":
+        modules = []
+        for module in ModuleLoader().get_detection_modules():
+            modules.append({"classname": type(module).__name__, "title": module.name})
+        if args.outform == "json":
+            print(json.dumps(modules))
+        else:
+            for module_data in modules:
+                print("{}: {}".format(module_data["classname"], module_data["title"]))
+        sys.exit()
+
     if args.command == "help":
         parser.print_help()
         sys.exit()

mythril/laser/ethereum/keccak_function_manager.py

@@ -141,7 +141,7 @@ class KeccakFunctionManager:
         )
         concrete_cond = symbol_factory.Bool(False)
         for key, keccak in self.concrete_hashes.items():
-            hash_eq = And(func(func_input) == keccak, key == func_input,)
+            hash_eq = And(func(func_input) == keccak, key == func_input)
             concrete_cond = Or(concrete_cond, hash_eq)
         return And(inv(func(func_input)) == func_input, Or(cond, concrete_cond))
 

mythril/mythril/mythril_analyzer.py

@@ -18,6 +18,7 @@ from mythril.analysis.report import Report, Issue
 from mythril.ethereum.evmcontract import EVMContract
 from mythril.laser.smt import SolverStatistics
 from mythril.support.start_time import StartTime
+from mythril.exceptions import DetectorNotFoundError
 
 log = logging.getLogger(__name__)
 
@@ -172,6 +173,9 @@ class MythrilAnalyzer:
                     custom_modules_directory=self.custom_modules_directory,
                 )
                 issues = fire_lasers(sym, modules)
+            except DetectorNotFoundError as e:
+                # Bubble up
+                raise e
             except KeyboardInterrupt:
                 log.critical("Keyboard Interrupt")
                 if self.iprof is not None: