diff --git a/manticore/__init__.py b/manticore/__init__.py index f200a0221..4cae29336 100644 --- a/manticore/__init__.py +++ b/manticore/__init__.py @@ -6,7 +6,7 @@ from .utils import config, log from .utils.log import set_verbosity -from .utils.helpers import issymbolic, istainted +from .core.smtlib import issymbolic, istainted from .ethereum.manticore import ManticoreEVM __all__ = [issymbolic.__name__, istainted.__name__, ManticoreEVM.__name__, set_verbosity.__name__] diff --git a/manticore/core/plugin.py b/manticore/core/plugin.py index bf88a3749..b49269bfe 100644 --- a/manticore/core/plugin.py +++ b/manticore/core/plugin.py @@ -4,7 +4,7 @@ import pstats import threading -from ..utils.helpers import issymbolic +from .smtlib import issymbolic logger = logging.getLogger(__name__) diff --git a/manticore/core/smtlib/__init__.py b/manticore/core/smtlib/__init__.py index 10fd8a37e..0128c94f6 100644 --- a/manticore/core/smtlib/__init__.py +++ b/manticore/core/smtlib/__init__.py @@ -1,4 +1,4 @@ -from .expression import Expression, Bool, BitVec, Array, BitVecConstant # noqa +from .expression import Expression, Bool, BitVec, Array, BitVecConstant, issymbolic # noqa from .constraints import ConstraintSet # noqa from .solver import * # noqa from . import operators as Operators # noqa diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py index 3311d5951..99e709de6 100644 --- a/manticore/core/smtlib/expression.py +++ b/manticore/core/smtlib/expression.py @@ -1,6 +1,9 @@ from functools import reduce import uuid +import re +import copy + class Expression: """ Abstract taintable Expression. """ @@ -24,6 +27,78 @@ def taint(self): return self._taint +def issymbolic(value): + """ + Helper to determine whether an object is symbolic (e.g checking + if data read from memory is symbolic) + + :param object value: object to check + :return: whether `value` is symbolic + :rtype: bool + """ + return isinstance(value, Expression) + + +def istainted(arg, taint=None): + """ + Helper to determine whether an object if tainted. + :param arg: a value or Expression + :param taint: a regular expression matching a taint value (eg. 'IMPORTANT.*'). If None, this function checks for any taint value. + """ + + if not issymbolic(arg): + return False + if taint is None: + return len(arg.taint) != 0 + for arg_taint in arg.taint: + m = re.match(taint, arg_taint, re.DOTALL | re.IGNORECASE) + if m: + return True + return False + + +def get_taints(arg, taint=None): + """ + Helper to list an object taints. + :param arg: a value or Expression + :param taint: a regular expression matching a taint value (eg. 'IMPORTANT.*'). If None, this function checks for any taint value. + """ + + if not issymbolic(arg): + return + for arg_taint in arg.taint: + if taint is not None: + m = re.match(taint, arg_taint, re.DOTALL | re.IGNORECASE) + if m: + yield arg_taint + else: + yield arg_taint + return + + +def taint_with(arg, taint, value_bits=256, index_bits=256): + """ + Helper to taint a value. + :param arg: a value or Expression + :param taint: a regular expression matching a taint value (eg. 'IMPORTANT.*'). If None, this function checks for any taint value. + """ + + tainted_fset = frozenset((taint,)) + + if not issymbolic(arg): + if isinstance(arg, int): + arg = BitVecConstant(value_bits, arg) + arg._taint = tainted_fset + else: + raise ValueError("type not supported") + + else: + arg = copy.copy(arg) + arg._taint |= tainted_fset + + return arg + + class Variable(Expression): def __init__(self, name, *args, **kwargs): if self.__class__ is Variable: diff --git a/manticore/core/smtlib/operators.py b/manticore/core/smtlib/operators.py index 61ec8bb46..5be8f7984 100644 --- a/manticore/core/smtlib/operators.py +++ b/manticore/core/smtlib/operators.py @@ -10,7 +10,7 @@ BoolConstant, BoolITE, ) -from ...utils.helpers import issymbolic +from . import issymbolic import math diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index a666de991..f12894466 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -26,7 +26,7 @@ from .visitors import * from ...exceptions import Z3NotFoundError, SolverError, SolverUnknown, TooManySolutions from ...utils import config -from ...utils.helpers import issymbolic +from . import issymbolic logger = logging.getLogger(__name__) consts = config.get_group("smt") diff --git a/manticore/core/state.py b/manticore/core/state.py index c2e1c6ce8..186cf63c1 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -1,8 +1,7 @@ import copy import logging -from .smtlib import solver, Bool -from ..utils.helpers import issymbolic +from .smtlib import solver, Bool, issymbolic from ..utils.event import Eventful logger = logging.getLogger(__name__) diff --git a/manticore/ethereum/abi.py b/manticore/ethereum/abi.py index 15b5903ef..161d4dd3b 100644 --- a/manticore/ethereum/abi.py +++ b/manticore/ethereum/abi.py @@ -5,8 +5,7 @@ import sha3 from . import abitypes -from ..utils.helpers import issymbolic -from ..core.smtlib import Array, Operators, BitVec, ArrayVariable, ArrayProxy +from ..core.smtlib import Array, Operators, BitVec, ArrayVariable, ArrayProxy, issymbolic from ..exceptions import EthereumError logger = logging.getLogger(__name__) diff --git a/manticore/ethereum/detectors.py b/manticore/ethereum/detectors.py index b79642d6b..1fc4cdaf3 100644 --- a/manticore/ethereum/detectors.py +++ b/manticore/ethereum/detectors.py @@ -3,8 +3,15 @@ import logging from contextlib import contextmanager -from ..core.smtlib import Operators, Constant, simplify -from ..utils.helpers import istainted, issymbolic, taint_with, get_taints +from ..core.smtlib import ( + Operators, + Constant, + simplify, + istainted, + issymbolic, + get_taints, + taint_with, +) from ..core.plugin import Plugin diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 4ff0c7f2f..9628fe69f 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -25,6 +25,7 @@ BoolConstant, BoolOperation, Expression, + issymbolic, ) from ..core.state import TerminateState, AbandonState from .account import EVMContract, EVMAccount, ABI @@ -34,7 +35,7 @@ from ..exceptions import EthereumError, DependencyError, NoAliveStates from ..platforms import evm from ..utils import config, log -from ..utils.helpers import PickleSerializer, issymbolic +from ..utils.helpers import PickleSerializer logger = logging.getLogger(__name__) diff --git a/manticore/native/cpu/abstractcpu.py b/manticore/native/cpu/abstractcpu.py index 2ea4c43cd..1e425b69f 100644 --- a/manticore/native/cpu/abstractcpu.py +++ b/manticore/native/cpu/abstractcpu.py @@ -11,13 +11,12 @@ from .disasm import init_disassembler from ..memory import ConcretizeMemory, InvalidMemoryAccess, FileMap, AnonMap from ..memory import LazySMemory -from ...core.smtlib import Expression, BitVec, Operators, Constant +from ...core.smtlib import Expression, BitVec, Operators, Constant, issymbolic from ...core.smtlib import visitors from ...core.smtlib.solver import Z3Solver from ...utils.emulate import ConcreteUnicornEmulator from ...utils.event import Eventful from ...utils.fallback_emulator import UnicornEmulator -from ...utils.helpers import issymbolic from capstone import CS_ARCH_ARM64, CS_ARCH_X86, CS_ARCH_ARM from capstone.arm64 import ARM64_REG_ENDING diff --git a/manticore/native/cpu/arm.py b/manticore/native/cpu/arm.py index cffd11419..4bd52fcdc 100644 --- a/manticore/native/cpu/arm.py +++ b/manticore/native/cpu/arm.py @@ -8,8 +8,7 @@ from .abstractcpu import instruction as abstract_instruction from .bitwise import * from .register import Register -from ...core.smtlib import Operators, BitVecConstant -from ...utils.helpers import issymbolic +from ...core.smtlib import Operators, BitVecConstant, issymbolic logger = logging.getLogger(__name__) diff --git a/manticore/native/cpu/x86.py b/manticore/native/cpu/x86.py index 127cb2be1..14d6b91a1 100644 --- a/manticore/native/cpu/x86.py +++ b/manticore/native/cpu/x86.py @@ -19,9 +19,8 @@ ) -from ...core.smtlib import Operators, BitVec, Bool, BitVecConstant, operator, visitors +from ...core.smtlib import Operators, BitVec, Bool, BitVecConstant, operator, visitors, issymbolic from ..memory import ConcretizeMemory -from ...utils.helpers import issymbolic from functools import reduce logger = logging.getLogger(__name__) diff --git a/manticore/native/manticore.py b/manticore/native/manticore.py index 74363ef4a..1cc2dbf94 100644 --- a/manticore/native/manticore.py +++ b/manticore/native/manticore.py @@ -12,9 +12,8 @@ from .state import State from ..core.manticore import ManticoreBase from ..core.smtlib import ConstraintSet -from ..core.smtlib.solver import Z3Solver +from ..core.smtlib.solver import Z3Solver, issymbolic from ..utils import log, config -from ..utils.helpers import issymbolic logger = logging.getLogger(__name__) diff --git a/manticore/native/memory.py b/manticore/native/memory.py index c09f78bb2..a4c4d0ac8 100644 --- a/manticore/native/memory.py +++ b/manticore/native/memory.py @@ -9,9 +9,10 @@ BitVec, BitVecConstant, expression, + issymbolic, ) from ..native.mappings import mmap, munmap -from ..utils.helpers import issymbolic, interval_intersection +from ..utils.helpers import interval_intersection import functools import logging diff --git a/manticore/native/models.py b/manticore/native/models.py index ddaec1b5a..56d7ebd64 100644 --- a/manticore/native/models.py +++ b/manticore/native/models.py @@ -3,7 +3,7 @@ """ from .cpu.abstractcpu import ConcretizeArgument -from ..utils.helpers import issymbolic +from ..core.smtlib import issymbolic from ..core.smtlib.solver import Z3Solver from ..core.smtlib.operators import ITEBV, ZEXTEND diff --git a/manticore/platforms/decree.py b/manticore/platforms/decree.py index b74a2f3d5..6fb8633f1 100644 --- a/manticore/platforms/decree.py +++ b/manticore/platforms/decree.py @@ -6,7 +6,6 @@ from ..native.memory import SMemory32, Memory32 from ..core.smtlib import * from ..core.state import TerminateState -from ..utils.helpers import issymbolic from ..binary import CGCElf from ..platforms.platform import Platform import logging diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 0c6a04db6..9ec84fa20 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -6,7 +6,6 @@ import inspect from functools import wraps from typing import List, Set, Tuple, Union -from ..utils.helpers import issymbolic, get_taints, taint_with, istainted from ..platforms.platform import * from ..core.smtlib import ( Z3Solver, @@ -21,6 +20,10 @@ translate_to_smtlib, to_constant, simplify, + issymbolic, + get_taints, + istainted, + taint_with, ) from ..core.state import Concretize, TerminateState from ..utils.event import Eventful diff --git a/manticore/platforms/linux.py b/manticore/platforms/linux.py index 7c3b141e6..f88cc1aaa 100644 --- a/manticore/platforms/linux.py +++ b/manticore/platforms/linux.py @@ -21,14 +21,13 @@ from . import linux_syscalls from .linux_syscall_stubs import SyscallStubs from ..core.state import TerminateState -from ..core.smtlib import ConstraintSet, Operators, Expression +from ..core.smtlib import ConstraintSet, Operators, Expression, issymbolic from ..core.smtlib.solver import Z3Solver from ..exceptions import SolverError from ..native.cpu.abstractcpu import Syscall, ConcretizeArgument, Interruption from ..native.cpu.cpufactory import CpuFactory from ..native.memory import SMemory32, SMemory64, Memory32, Memory64, LazySMemory32, LazySMemory64 from ..platforms.platform import Platform, SyscallNotImplemented, unimplemented -from ..utils.helpers import issymbolic logger = logging.getLogger(__name__) diff --git a/manticore/utils/emulate.py b/manticore/utils/emulate.py index b74d68321..41cf918e6 100644 --- a/manticore/utils/emulate.py +++ b/manticore/utils/emulate.py @@ -10,8 +10,7 @@ from unicorn.arm_const import * from unicorn.x86_const import * -from .helpers import issymbolic -from ..core.smtlib import Operators, solver +from ..core.smtlib import Operators, solver, issymbolic from ..native.memory import MemoryException logger = logging.getLogger(__name__) diff --git a/manticore/utils/fallback_emulator.py b/manticore/utils/fallback_emulator.py index 22ab3b97a..237059a87 100644 --- a/manticore/utils/fallback_emulator.py +++ b/manticore/utils/fallback_emulator.py @@ -2,7 +2,7 @@ from ..native.memory import MemoryException -from .helpers import issymbolic +from ..core.smtlib import issymbolic ###################################################################### # Abstract classes for capstone/unicorn based cpus diff --git a/manticore/utils/helpers.py b/manticore/utils/helpers.py index 21af30fc5..288ef2ebe 100644 --- a/manticore/utils/helpers.py +++ b/manticore/utils/helpers.py @@ -3,88 +3,10 @@ import sys from collections import OrderedDict -import copy -import re - logger = logging.getLogger(__name__) -def issymbolic(value): - """ - Helper to determine whether an object is symbolic (e.g checking - if data read from memory is symbolic) - - :param object value: object to check - :return: whether `value` is symbolic - :rtype: bool - """ - from ..core.smtlib import Expression # prevent circular imports - - return isinstance(value, Expression) - - -def istainted(arg, taint=None): - """ - Helper to determine whether an object if tainted. - :param arg: a value or Expression - :param taint: a regular expression matching a taint value (eg. 'IMPORTANT.*'). If None, this function checks for any taint value. - """ - - if not issymbolic(arg): - return False - if taint is None: - return len(arg.taint) != 0 - for arg_taint in arg.taint: - m = re.match(taint, arg_taint, re.DOTALL | re.IGNORECASE) - if m: - return True - return False - - -def get_taints(arg, taint=None): - """ - Helper to list an object taints. - :param arg: a value or Expression - :param taint: a regular expression matching a taint value (eg. 'IMPORTANT.*'). If None, this function checks for any taint value. - """ - - if not issymbolic(arg): - return - for arg_taint in arg.taint: - if taint is not None: - m = re.match(taint, arg_taint, re.DOTALL | re.IGNORECASE) - if m: - yield arg_taint - else: - yield arg_taint - return - - -def taint_with(arg, taint, value_bits=256, index_bits=256): - """ - Helper to taint a value. - :param arg: a value or Expression - :param taint: a regular expression matching a taint value (eg. 'IMPORTANT.*'). If None, this function checks for any taint value. - """ - from ..core.smtlib import BitVecConstant # prevent circular imports - - tainted_fset = frozenset((taint,)) - - if not issymbolic(arg): - if isinstance(arg, int): - arg = BitVecConstant(value_bits, arg) - arg._taint = tainted_fset - else: - raise ValueError("type not supported") - - else: - arg = copy.copy(arg) - arg._taint |= tainted_fset - - return arg - - def interval_intersection(min1, max1, min2, max2): """ Given two intervals, (min1, max1) and (min2, max2) return their intersecting interval, diff --git a/tests/native/test_lazy_memory.py b/tests/native/test_lazy_memory.py index c53bf800b..9d4d6d291 100644 --- a/tests/native/test_lazy_memory.py +++ b/tests/native/test_lazy_memory.py @@ -10,8 +10,7 @@ import sys from manticore.native.memory import * -from manticore.utils.helpers import issymbolic -from manticore.core.smtlib import Z3Solver, Operators +from manticore.core.smtlib import Z3Solver, Operators, issymbolic from manticore.core.smtlib.expression import * from manticore.core.smtlib.visitors import *