diff --git a/manticore/__main__.py b/manticore/__main__.py index 510082925..611487557 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -212,9 +212,7 @@ def positive(value): ) eth_flags.add_argument( - "--limit-loops", - action="store_true", - help="Avoid exploring constant functions for human transactions", + "--limit-loops", action="store_true", help="Limit loops depth", ) eth_flags.add_argument( diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py index 92abd8c06..f924008ce 100644 --- a/manticore/core/manticore.py +++ b/manticore/core/manticore.py @@ -23,7 +23,7 @@ from ..utils.helpers import PickleSerializer from ..utils.log import set_verbosity from ..utils.nointerrupt import WithKeyboardInterruptAs -from .workspace import Workspace +from .workspace import Workspace, Testcase from .worker import WorkerSingle, WorkerThread, WorkerProcess from multiprocessing.managers import SyncManager @@ -403,8 +403,7 @@ def goto_snapshot(self): in a snapshot """ if not self._snapshot: raise ManticoreError("No snapshot to go to") - for state_id in tuple(self._ready_states): - self._ready_states.remove(state_id) + self.clear_ready_states() for state_id in self._snapshot: self._ready_states.append(state_id) self._snapshot = None @@ -421,13 +420,23 @@ def clear_snapshot(self): @sync @at_not_running def clear_terminated_states(self): - """ Simply remove all states from terminated list """ + """ Remove all states from the terminated list """ terminated_states_ids = tuple(self._terminated_states) for state_id in terminated_states_ids: self._terminated_states.remove(state_id) self._remove(state_id) assert self.count_terminated_states() == 0 + @sync + @at_not_running + def clear_ready_states(self): + """ Remove all states from the ready list """ + ready_states_ids = tuple(self._ready_states) + for state_id in ready_states_ids: + self._ready_states.remove(state_id) + self._remove(state_id) + assert self.count_ready_states() == 0 + def __str__(self): return f"<{str(type(self))[8:-2]}| Alive States: {self.count_ready_states()}; Running States: {self.count_busy_states()} Terminated States: {self.count_terminated_states()} Killed States: {self.count_killed_states()} Started: {self._running.value} Killed: {self._killed.value}>" @@ -833,7 +842,7 @@ def count_terminated_states(self): """ Terminated states count """ return len(self._terminated_states) - def generate_testcase(self, state, message: str = "test", name: str = "test"): + def generate_testcase(self, state, message: str = "test", name: str = "test") -> Testcase: if message == "test" and hasattr(state, "_terminated_by") and state._terminated_by: message = str(state._terminated_by) testcase = self._output.testcase(prefix=name) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 9d512c61a..8c312d019 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -593,7 +593,7 @@ def get_value(self, constraints: ConstraintSet, *expressions): """ values = [] start = time.time() - with constraints as temp_cs: + with constraints.related_to(*expressions) as temp_cs: for expression in expressions: if not issymbolic(expression): values.append(expression) diff --git a/manticore/core/workspace.py b/manticore/core/workspace.py index 6041ba1ef..2160f2e16 100644 --- a/manticore/core/workspace.py +++ b/manticore/core/workspace.py @@ -44,7 +44,7 @@ def __exit__(self, *excinfo): consts.add("dir", default=".", description="Location of where to create workspace directories") -class WorkspaceTestcase: +class Testcase: """ A `WorkspaceTestCase` represents a test case input generated by Manticore. """ @@ -519,8 +519,8 @@ def __init__(self, desc=None): self._descriptor = desc self._store = Store.fromdescriptor(desc) - def testcase(self, prefix: str = "test") -> WorkspaceTestcase: - return WorkspaceTestcase(self, prefix) + def testcase(self, prefix: str = "test") -> Testcase: + return Testcase(self, prefix) @property def store(self): @@ -587,7 +587,7 @@ def _named_stream(self, name, binary=False, lock=False): yield s # Remove/move ... - def save_testcase(self, state: StateBase, testcase: WorkspaceTestcase, message: str = ""): + def save_testcase(self, state: StateBase, testcase: Testcase, message: str = ""): """ Save the environment from `state` to storage. Return a state id describing it, which should be an int or a string. diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 32a0d78a5..1ef66a3f8 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -13,7 +13,8 @@ from crytic_compile import CryticCompile, InvalidCompilation, is_supported -from ..core.manticore import ManticoreBase +from ..core.manticore import ManticoreBase, Testcase, ManticoreError + from ..core.smtlib import ( ConstraintSet, Array, @@ -1536,10 +1537,6 @@ def current_location(self, state): def generate_testcase(self, state, message="", only_if=None, name="user"): """ - Generate a testcase to the workspace for the given program state. The details of what - a testcase is depends on the type of Platform the state is, but involves serializing the state, - and generating an input (concretizing symbolic variables) to trigger this state. - The only_if parameter should be a symbolic expression. If this argument is provided, and the expression *can be true* in this state, a testcase is generated such that the expression will be true in the state. If it *is impossible* for the expression to be true in the state, a testcase is not generated. @@ -1552,29 +1549,38 @@ def generate_testcase(self, state, message="", only_if=None, name="user"): m.generate_testcase(state, 'balance CAN be 0', only_if=balance == 0) # testcase generated with an input that will violate invariant (make balance == 0) + """ + try: + with state as temp_state: + if only_if is not None: + temp_state.constrain(only_if) + return self._generate_testcase_ex(temp_state, message, name=name) + except ManticoreError: + return None + + def _generate_testcase_ex(self, state, message="", name="user"): + """ + Generate a testcase in the outputspace for the given program state. + An exception is raised if the state is unsound or unfeasible + + On return you get a Testcase containing all the informations about the state. + A Testcase is a collection of files living at the OutputSpace. + Registered plugins and other parts of Manticore add files to the Testcase. + User can add more streams to is like this: + + testcase = m.generate_testcase_ex(state) + with testcase.open_stream("txt") as descf: + descf.write("This testcase is interesting!") :param manticore.core.state.State state: :param str message: longer description of the testcase condition - :param manticore.core.smtlib.Bool only_if: only if this expr can be true, generate testcase. if is None, generate testcase unconditionally. - :param str name: short string used as the prefix for the workspace key (e.g. filename prefix for testcase files) - :return: If a testcase was generated + :param str name: short string used as the prefix for the outputspace key (e.g. filename prefix for testcase files) + :return: a Testcase :rtype: bool """ - """ - Create a serialized description of a given state. - :param state: The state to generate information about - :param message: Accompanying message - """ + # Refuse to generate a testcase from an unsound state if not self.fix_unsound_symbolication(state): - return False - - if only_if is not None: - with state as temp_state: - temp_state.constrain(only_if) - if temp_state.is_feasible(): - return self.generate_testcase(temp_state, message, only_if=None, name=name) - else: - return False + raise ManticoreError("Trying to generate a testcase out of an unsound state path") blockchain = state.platform @@ -1584,8 +1590,6 @@ def generate_testcase(self, state, message="", only_if=None, name="user"): testcase = super().generate_testcase( state, message + f"({len(blockchain.human_transactions)} txs)", name=name ) - # TODO(mark): Refactor ManticoreOutput to let the platform be more in control - # so this function can be fully ported to EVMWorld.generate_workspace_files. local_findings = set() for detector in self.detectors.values(): @@ -1865,8 +1869,8 @@ def ready_sound_states(self): This tries to solve any symbolic imprecision added by unsound_symbolication and then iterates over the resultant set. - This is the recommended to iterate over resultant steas after an exploration - that included unsound symbolication + This is the recommended way to iterate over the resultant states after + an exploration that included unsound symbolication """ self.fix_unsound_all() diff --git a/manticore/ethereum/verifier.py b/manticore/ethereum/verifier.py new file mode 100644 index 000000000..702fd0bb6 --- /dev/null +++ b/manticore/ethereum/verifier.py @@ -0,0 +1,487 @@ +""" +$python manticore-verifier.py property.sol TestToken +""" +import os +import re +import sys +import argparse +import logging +import pkg_resources +from itertools import chain +from manticore.ethereum import ManticoreEVM +from manticore.ethereum.detectors import DetectIntegerOverflow +from manticore.ethereum.plugins import FilterFunctions, VerboseTrace, KeepOnlyIfStorageChanges +from manticore.core.smtlib.operators import OR, NOT, AND +from manticore.ethereum.abi import ABI +from manticore.utils.log import set_verbosity +from prettytable import PrettyTable +from manticore.utils import config +from manticore.utils.nointerrupt import WithKeyboardInterruptAs + + +def constrain_to_known_func_ids(state): + world = state.platform + tx = world.human_transactions[-1] + md = state.manticore.get_metadata(tx.address) + + N = 0 + is_normal = False + func_id = tx.data[:4] + for func_hsh in md.function_selectors: + N += 1 + is_normal = OR(func_hsh == func_id, is_normal) + is_fallback = NOT(is_normal) + is_known_func_id = is_normal + + chosen_fallback_func_is = None + if state.can_be_true(is_fallback): + with state as temp_state: + temp_state.constraint(is_fallback) + chosen_fallback_func_id = bytes(state.solve_one(tx.data[:4])) + is_known_func_id = OR(is_known_func_id, chosen_fallback_func_id == func_id) + N += 1 + state.constrain(is_known_func_id) + return N + + +def manticore_verifier( + source_code, + contract_name, + maxfail=None, + maxt=3, + maxcov=100, + deployer=None, + senders=None, + psender=None, + propre=r"crytic_.*", + compile_args=None, + outputspace_url=None, + timeout=100, +): + """ Verify solidity properties + The results are dumped to stdout and to the workspace folder. + + $manticore-verifier property.sol --contract TestToken --smt.solver yices --maxt 4 + # Owner account: 0xf3c67ffb8ab4cdd4d3243ad247d0641cd24af939 + # Contract account: 0x6f4b51ac2eb017600e9263085cfa06f831132c72 + # Sender_0 account: 0x97528a0c7c6592772231fd581e5b42125c1a2ff4 + # PSender account: 0x97528a0c7c6592772231fd581e5b42125c1a2ff4 + # Found 2 properties: crytic_test_must_revert, crytic_test_balance + # Exploration will stop when some of the following happens: + # * 4 human transaction sent + # * Code coverage is greater than 100% meassured on target contract + # * No more coverage was gained in the last transaction + # * At least 2 different properties where found to be breakable. (1 for fail fast) + # * 240 seconds pass + # Starting exploration... + Transactions done: 0. States: 1, RT Coverage: 0.0%, Failing properties: 0/2 + Transactions done: 1. States: 2, RT Coverage: 55.43%, Failing properties: 0/2 + Transactions done: 2. States: 8, RT Coverage: 80.48%, Failing properties: 1/2 + Transactions done: 3. States: 30, RT Coverage: 80.48%, Failing properties: 1/2 + No coverage progress. Stopping exploration. + Coverage obtained 80.48%. (RT + prop) + +-------------------------+------------+ + | Property Named | Status | + +-------------------------+------------+ + | crytic_test_balance | failed (0) | + | crytic_test_must_revert | passed | + +-------------------------+------------+ + Checkout testcases here:./mcore_6jdil7nh + + :param maxfail: stop after maxfail properties are failing. All if None + :param maxcov: Stop after maxcov % coverage is obtained in the main contract + :param maxt: Max transaction count to explore + :param deployer: (optional) address of account used to deploy the contract + :param senders: (optional) a list of calles addresses for the exploration + :param psender: (optional) address from where the property is tested + :param source_code: A filename or source code + :param contract_name: The target contract name defined in the source code + :param propre: A regular expression for selecting properties + :param outputspace_url: where to put the extended result + :param timeout: timeout in seconds + :return: + """ + # Termination condition + # Exploration will stop when some of the following happens: + # * MAXTX human transaction sent + # * Code coverage is greater than MAXCOV meassured on target contract + # * No more coverage was gained in the last transaction + # * At least MAXFAIL different properties where found to be breakable. (1 for fail fast) + + # Max transaction count to explore + MAXTX = maxt + # Max coverage % to get + MAXCOV = maxcov + # Max different properties fails + MAXFAIL = maxfail + + config.get_group("smt").timeout = 120 + config.get_group("smt").memory = 16384 + config.get_group("evm").ignore_balance = True + config.get_group("evm").oog = "ignore" + + print("# Welcome to manticore-verifier") + # Main manticore manager object + m = ManticoreEVM() + # avoid all human level tx that are marked as constant (have no effect on the storage) + filter_out_human_constants = FilterFunctions( + regexp=r".*", depth="human", mutability="constant", include=False + ) + m.register_plugin(filter_out_human_constants) + filter_out_human_constants.disable() + + # Avoid automatically exploring property + filter_no_crytic = FilterFunctions(regexp=propre, include=False) + m.register_plugin(filter_no_crytic) + filter_no_crytic.disable() + + # Only explore properties (at human level) + filter_only_crytic = FilterFunctions(regexp=propre, depth="human", fallback=False, include=True) + m.register_plugin(filter_only_crytic) + filter_only_crytic.disable() + + # And now make the contract account to analyze + + # User accounts. Transactions trying to break the property are send from one + # of this + senders = (None,) if senders is None else senders + + user_accounts = [] + for n, address_i in enumerate(senders): + user_accounts.append( + m.create_account(balance=10 ** 10, address=address_i, name=f"sender_{n}") + ) + # the address used for deployment + owner_account = m.create_account(balance=10 ** 10, address=deployer, name="deployer") + # the target contract account + contract_account = m.solidity_create_contract( + source_code, + owner=owner_account, + contract_name=contract_name, + compile_args=compile_args, + name="contract_account", + ) + # the address used for checking porperties + checker_account = m.create_account(balance=10 ** 10, address=psender, name="psender") + + print(f"# Owner account: 0x{int(owner_account):x}") + print(f"# Contract account: 0x{int(contract_account):x}") + for n, user_account in enumerate(user_accounts): + print(f"# Sender_{n} account: 0x{int(checker_account):x}") + print(f"# PSender account: 0x{int(checker_account):x}") + + properties = {} + md = m.get_metadata(contract_account) + for func_hsh in md.function_selectors: + func_name = md.get_abi(func_hsh)["name"] + if re.match(propre, func_name): + properties[func_name] = [] + + print(f"# Found {len(properties)} properties: {', '.join(properties.keys())}") + if not properties: + print("I am sorry I had to run the init bytecode for this.\n" "Good Bye.") + return + MAXFAIL = len(properties) if MAXFAIL is None else MAXFAIL + tx_num = 0 # transactions count + current_coverage = None # obtained coverge % + new_coverage = 0.0 + + print( + f"""# Exploration will stop when some of the following happens: +# * {MAXTX} human transaction sent +# * Code coverage is greater than {MAXCOV}% meassured on target contract +# * No more coverage was gained in the last transaction +# * At least {MAXFAIL} different properties where found to be breakable. (1 for fail fast) +# * {timeout} seconds pass""" + ) + print("# Starting exploration...") + print( + f"Transactions done: {tx_num}. States: {m.count_ready_states()}, RT Coverage: {0.00}%, " + f"Failing properties: 0/{len(properties)}" + ) + with m.kill_timeout(timeout=timeout): + while True: + # check if we found a way to break more than MAXFAIL properties + broken_properties = sum(int(len(x) != 0) for x in properties.values()) + if broken_properties >= MAXFAIL: + print( + f"Found {broken_properties}/{len(properties)} failing properties. Stopping exploration." + ) + break + + # check if we sent more than MAXTX transaction + if tx_num >= MAXTX: + print("Max numbr of transactions reached({tx_num})") + break + tx_num += 1 + + # check if we got enough coverage + new_coverage = m.global_coverage(contract_account) + if new_coverage >= MAXCOV: + print( + "Current coverage({new_coverage}%) is greater than max allowed({MAXCOV}%).Stopping exploration." + ) + break + + # check if we have made coverage progress in the last transaction + if current_coverage == new_coverage: + print(f"No coverage progress. Stopping exploration.") + break + current_coverage = new_coverage + + # check if timeout was requested + if m.is_killed(): + print("Cancelled or timeout.") + break + + # Explore all methods but the "crytic_" properties + # Note: you may be tempted to get all valid function ids/hashes from the + # metadata and to constrain the first 4 bytes of the calldata here. + # This wont work because we also want to prevent the contract to call + # crytic added methods as internal transactions + filter_no_crytic.enable() # filter out crytic_porperties + filter_out_human_constants.enable() # Exclude constant methods + filter_only_crytic.disable() # Exclude all methods that are not property checks + + symbolic_data = m.make_symbolic_buffer(320) + symbolic_value = m.make_symbolic_value() + caller_account = m.make_symbolic_value(160) + args = tuple((caller_account == address_i for address_i in user_accounts)) + + m.constrain(OR(*args, False)) + m.transaction( + caller=caller_account, + address=contract_account, + value=symbolic_value, + data=symbolic_data, + ) + + m.clear_terminated_states() # no interest in reverted states + m.take_snapshot() # make a copy of all ready states + print( + f"Transactions done: {tx_num}. States: {m.count_ready_states()}, " + f"RT Coverage: {m.global_coverage(contract_account):3.2f}%, " + f"Failing properties: {broken_properties}/{len(properties)}" + ) + + # And now explore all properties (and only the properties) + filter_no_crytic.disable() # Allow crytic_porperties + filter_out_human_constants.disable() # Allow them to be marked as constants + filter_only_crytic.enable() # Exclude all methods that are not property checks + symbolic_data = m.make_symbolic_buffer(4) + m.transaction( + caller=checker_account, address=contract_account, value=0, data=symbolic_data + ) + + for state in m.all_states: + world = state.platform + tx = world.human_transactions[-1] + md = m.get_metadata(tx.address) + """ + A is _broken_ if: + * is normal property + * RETURN False + OR: + * property name ends witth 'revert' + * does not REVERT + Property is considered to _pass_ otherwise + """ + N = constrain_to_known_func_ids(state) + for func_id in map(bytes, state.solve_n(tx.data[:4], nsolves=N)): + func_name = md.get_abi(func_id)["name"] + if not func_name.endswith("revert"): + # Property does not ends in "revert" + # It must RETURN a 1 + if tx.return_value == 1: + # TODO: test when property STOPs + return_data = ABI.deserialize("bool", tx.return_data) + testcase = m.generate_testcase( + state, + f"property {md.get_func_name(func_id)} is broken", + only_if=AND(tx.data[:4] == func_id, return_data == 0), + ) + if testcase: + properties[func_name].append(testcase.num) + else: + # property name ends in "revert" so it MUST revert + if tx.result != "REVERT": + testcase = m.generate_testcase( + state, + f"Some property is broken did not reverted.(MUST REVERTED)", + only_if=tx.data[:4] == func_id, + ) + if testcase: + properties[func_name].append(testcase.num) + + m.clear_terminated_states() # no interest in reverted states for now! + m.goto_snapshot() + + m.clear_terminated_states() + m.clear_ready_states() + m.clear_snapshot() + + if m.is_killed(): + print("Exploration ended by CTRL+C or timeout") + + print(f"Coverage obtained {new_coverage:3.2f}%. (RT + prop)") + + x = PrettyTable() + x.field_names = ["Property Named", "Status"] + for name, testcases in sorted(properties.items()): + result = "passed" + if testcases: + result = f"failed ({testcases[0]})" + x.add_row((name, result)) + print(x) + + m.clear_ready_states() + + workspace = os.path.abspath(m.workspace)[len(os.getcwd()) + 1 :] + print(f"Checkout testcases here:./{workspace}") + + +def main(): + from crytic_compile import is_supported, cryticparser + + parser = argparse.ArgumentParser( + description="Solidity property verifier", + prog="manticore_verifier", + # formatter_class=argparse.ArgumentDefaultsHelpFormatter, + ) + + # Add crytic compile arguments + # See https://github.com/crytic/crytic-compile/wiki/Configuration + cryticparser.init(parser) + + parser.add_argument( + "source_code", type=str, nargs="*", default=[], help="Contract source code", + ) + parser.add_argument( + "-v", action="count", default=0, help="Specify verbosity level from -v to -vvvv" + ) + + parser.add_argument( + "--workspace", + type=str, + default=None, + help=("A folder name for temporaries and results." "(default mcore_?????)"), + ) + + current_version = pkg_resources.get_distribution("manticore").version + parser.add_argument( + "--version", + action="version", + version=f"Manticore {current_version}", + help="Show program version information", + ) + parser.add_argument( + "--propconfig", type=str, help="Solidity property accounts config file (.yml)", + ) + eth_flags = parser.add_argument_group("Ethereum flags") + + eth_flags.add_argument( + "--quick-mode", + action="store_true", + help="Configure Manticore for quick exploration. Disable gas, generate testcase only for alive states, " + "do not explore constant functions. Disable all detectors.", + ) + eth_flags.add_argument( + "--contract_name", type=str, help="The target contract name defined in the source code" + ) + eth_flags.add_argument( + "--maxfail", type=int, help="stop after maxfail properties are failing. All if None" + ) + eth_flags.add_argument( + "--maxcov", + type=int, + default=100, + help=" Stop after maxcov %% coverage is obtained in the main contract", + ) + eth_flags.add_argument("--maxt", type=int, default=3, help="Max transaction count to explore") + eth_flags.add_argument( + "--deployer", type=str, help="(optional) address of account used to deploy the contract" + ) + eth_flags.add_argument( + "--senders", + type=str, + help="(optional) a comma separated list of sender addresses. The properties are going to be tested sending transactions from these addresses.", + ) + eth_flags.add_argument( + "--psender", type=str, help="(optional) address from where the property is tested" + ) + eth_flags.add_argument( + "--propre", type=str, help="A regular expression for selecting properties" + ) + eth_flags.add_argument( + "--timeout", default=240, type=int, help="Exploration timeout in seconds" + ) + eth_flags.add_argument("--outputspace_url", type=str, help="where to put the extended result") + + config_flags = parser.add_argument_group("Constants") + config.add_config_vars_to_argparse(config_flags) + + parsed = parser.parse_args(sys.argv[1:]) + config.process_config_values(parser, parsed) + + if not parsed.source_code: + print(parser.format_usage() + "error: You need to provide a contract source code.") + sys.exit(1) + args = parsed + set_verbosity(args.v) + logger = logging.getLogger("manticore.main") + + # read yaml config file + deployer = None + senders = None + psenders = None + if args.propconfig: + """ + deployer: "0x41414141414141414141" #who deploys the contract + sender: ["0x51515151515151515151", "0x52525252525252525252"] #who calls the transactions (potentially can be multiple users) + psender: "0x616161616161616161" #who calls the property + """ + import yaml + + with open(args.propconfig) as f: + c = yaml.safe_load(f) + deployer = c.get("deployer") + if deployer is not None: + deployer = int(deployer, 0) + + senders = c.get("sender") + if senders is not None: + senders = [int(sender, 0) for sender in senders] + + psender = c.get("psender") + if psender is not None: + psender = int(psender, 0) + + # override with commandline args + deployer = None + if args.deployer is not None: + deployer = int(args.deployer, 0) + + senders = None + if args.senders is not None: + senders = [int(sender, 0) for sender in args.senders.split(",")] + + psender = None + if args.psender is not None: + psender = int(args.psender, 0) + + source_code = args.source_code[0] + contract_name = args.contract_name + maxfail = args.maxfail + maxt = args.maxt + maxcov = args.maxcov + return manticore_verifier( + source_code, + contract_name, + maxfail=maxfail, + maxt=maxt, + maxcov=100, + senders=senders, + deployer=deployer, + psender=psender, + timeout=args.timeout, + ) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 435c6d83e..f65c1cac5 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -102,6 +102,10 @@ def globalfakesha3(data): default=-1, description="Max calldata size to explore in each CALLDATACOPY. Iff size in a calldata related instruction are symbolic it will be constrained to be less than this constant. -1 means free(only use when gas is being tracked)", ) +consts.add( + "ignore_balance", default=False, description="Do not try to solve symbolic balances", +) + # Auxiliary constants and functions TT256 = 2 ** 256 @@ -251,6 +255,8 @@ def dump(self, stream, state, mevm, conc_tx=None): stream.write("Gas used: %d %s\n" % (conc_tx.gas, flagged(issymbolic(self.gas)))) tx_data = conc_tx.data + if len(tx_data) > 80: + tx_data = tx_data.rstrip(conc_tx.data[-3:-1]) stream.write( "Data: 0x{} {}\n".format( @@ -262,9 +268,9 @@ def dump(self, stream, state, mevm, conc_tx=None): return_data = conc_tx.return_data stream.write( - "Return_data: 0x{} ({}) {}\n".format( + "Return_data: 0x{} {} {}\n".format( binascii.hexlify(return_data).decode(), - printable_bytes(return_data), + f"({printable_bytes(return_data)})" if conc_tx.sort != "CREATE" else "", flagged(issymbolic(self.return_data)), ) ) @@ -743,7 +749,7 @@ def __init__( # This is a very cornered corner case in which code is actually symbolic # We should simply not allow to jump to unconstrained(*) symbolic code. # (*) bytecode that could take more than a single value - self._check_jumpdest = False + self._need_check_jumpdest = False self._valid_jumpdests = set() # Compile the list of valid jumpdests via linear dissassembly @@ -876,7 +882,7 @@ def __getstate__(self): state["_published_pre_instruction_events"] = self._published_pre_instruction_events state["_used_calldata_size"] = self._used_calldata_size state["_valid_jumpdests"] = self._valid_jumpdests - state["_check_jumpdest"] = self._check_jumpdest + state["_need_check_jumpdest"] = self._need_check_jumpdest state["_return_data"] = self._return_data state["evmfork"] = self.evmfork state["_refund"] = self._refund @@ -905,7 +911,7 @@ def __setstate__(self, state): self.suicides = state["suicides"] self._used_calldata_size = state["_used_calldata_size"] self._valid_jumpdests = state["_valid_jumpdests"] - self._check_jumpdest = state["_check_jumpdest"] + self._need_check_jumpdest = state["_need_check_jumpdest"] self._return_data = state["_return_data"] self.evmfork = state["evmfork"] self._refund = state["_refund"] @@ -1213,23 +1219,23 @@ def _set_check_jmpdest(self, flag=True): Note that at this point `flag` can be the conditional from a JUMPI instruction hence potentially a symbolic value. """ - self._check_jumpdest = flag + self._need_check_jumpdest = flag def _check_jmpdest(self): """ If the previous instruction was a JUMP/JUMPI and the conditional was True, this checks that the current instruction must be a JUMPDEST. - Here, if symbolic, the conditional `self._check_jumpdest` would be + Here, if symbolic, the conditional `self._need_check_jumpdest` would be already constrained to a single concrete value. """ # If pc is already pointing to a JUMPDEST thre is no need to check. pc = self.pc.value if isinstance(self.pc, Constant) else self.pc if pc in self._valid_jumpdests: - self._check_jumpdest = False + self._need_check_jumpdest = False return - should_check_jumpdest = simplify(self._check_jumpdest) + should_check_jumpdest = simplify(self._need_check_jumpdest) if isinstance(should_check_jumpdest, Constant): should_check_jumpdest = should_check_jumpdest.value elif issymbolic(should_check_jumpdest): @@ -1242,7 +1248,7 @@ def _check_jmpdest(self): # If it can be solved only to False just set it False. If it can be solved # only to True, process it and also set it to False - self._check_jumpdest = False + self._need_check_jumpdest = False if should_check_jumpdest: if pc not in self._valid_jumpdests: @@ -3371,21 +3377,24 @@ def dump(self, stream, state, mevm, message): stream.write("\n") # Accounts summary + assert state.can_be_true(True) is_something_symbolic = False stream.write("%d accounts.\n" % len(blockchain.accounts)) for account_address in blockchain.accounts: is_account_address_symbolic = issymbolic(account_address) - account_address = state.solve_one(account_address) + account_address = state.solve_one(account_address, constrain=True) stream.write("* %s::\n" % mevm.account_name(account_address)) stream.write( "Address: 0x%x %s\n" % (account_address, flagged(is_account_address_symbolic)) ) balance = blockchain.get_balance(account_address) - is_balance_symbolic = issymbolic(balance) - is_something_symbolic = is_something_symbolic or is_balance_symbolic - balance = state.solve_one(balance, constrain=True) - stream.write("Balance: %d %s\n" % (balance, flagged(is_balance_symbolic))) + + if not consts.ignore_balance: + is_balance_symbolic = issymbolic(balance) + is_something_symbolic = is_something_symbolic or is_balance_symbolic + balance = state.solve_one(balance, constrain=True) + stream.write("Balance: %d %s\n" % (balance, flagged(is_balance_symbolic))) storage = blockchain.get_storage(account_address) concrete_indexes = set() @@ -3394,7 +3403,7 @@ def dump(self, stream, state, mevm, message): for index in concrete_indexes: stream.write( - f"storage[{index:x}] = {state.solve_one(storage[index], constrain=True):x}" + f"storage[{index:x}] = {state.solve_one(storage[index], constrain=True):x}\n" ) storage = blockchain.get_storage(account_address) stream.write("Storage: %s\n" % translate_to_smtlib(storage, use_bindings=False)) @@ -3420,8 +3429,8 @@ def dump(self, stream, state, mevm, message): stream.write( "storage[%x] = %x %s\n" % ( - state.solve_one(i), - state.solve_one(value), + state.solve_one(i, constrain=True), + state.solve_one(value, constrain=True), flagged(is_storage_symbolic), ) ) diff --git a/manticore/utils/config.py b/manticore/utils/config.py index bd43bd80d..d9f7b4faa 100644 --- a/manticore/utils/config.py +++ b/manticore/utils/config.py @@ -319,7 +319,8 @@ def process_config_values(parser: argparse.ArgumentParser, args: argparse.Namesp :param args: The value that parser.parse_args returned """ # First, load a local config file, if passed or look for one in pwd if it wasn't. - load_overrides(args.config) + if hasattr(args, "config"): + load_overrides(args.config) # Get a list of defined config vals. If these are passed on the command line, # update them in their correct group, not in the cli group diff --git a/scripts/run_tests.sh b/scripts/run_tests.sh index ccef31929..97b71452f 100755 --- a/scripts/run_tests.sh +++ b/scripts/run_tests.sh @@ -100,8 +100,8 @@ run_truffle_tests(){ # Truffle smoke test. We test if manticore is able to generate states # from a truffle project. count=$(find output/ -name '*tx' -type f | wc -l) - if [ "$count" -ne 26 ]; then - echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 26" + if [ "$count" -lt 25 ]; then + echo "Truffle test failed" `ls output/*tx -l | wc -l` "< 25" return 1 fi echo "Truffle test succeded" diff --git a/setup.py b/setup.py index d40169394..8690299ee 100644 --- a/setup.py +++ b/setup.py @@ -65,6 +65,11 @@ def rtd_dependent_deps(): ] + rtd_dependent_deps(), extras_require=extra_require, - entry_points={"console_scripts": ["manticore = manticore.__main__:main"]}, + entry_points={ + "console_scripts": [ + "manticore = manticore.__main__:main", + "manticore-verifier = manticore.ethereum.verifier:main", + ] + }, classifiers=["License :: OSI Approved :: GNU Affero General Public License v3"], ) diff --git a/tests/ethereum/contracts/prop_verifier.sol b/tests/ethereum/contracts/prop_verifier.sol new file mode 100644 index 000000000..f45bf1746 --- /dev/null +++ b/tests/ethereum/contracts/prop_verifier.sol @@ -0,0 +1,48 @@ +contract Ownership{ + address owner = msg.sender; + function Owner() public{ + owner = msg.sender; + } + modifier isOwner(){ + require(owner == msg.sender); + _; + } +} +contract Pausable is Ownership{ + bool is_paused; + modifier ifNotPaused(){ + require(!is_paused); + _; + } + function paused() isOwner public{ + is_paused = true; + } + function resume() isOwner public{ + is_paused = false; + } +} +contract Token is Pausable{ + mapping(address => uint) public balances; + function transfer(address to, uint value) ifNotPaused public{ + balances[msg.sender] -= value; + balances[to] += value; + } +} + +contract TestToken is Token { + constructor() public{ + balances[msg.sender] = 10000; + } + // the properties + function crytic_test_balance() view public returns(bool){ + return balances[msg.sender] <= 10000; + } + function crytic_test_must_revert() view public returns(bool){ + require(false); + } + function crytic_failing_test_must_revert() view public returns(bool){ + require(true); + } + + +} diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index 998aadd8f..c09331a76 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -1,5 +1,7 @@ import binascii import unittest +import subprocess +import pkg_resources from contextlib import contextmanager from pathlib import Path @@ -27,12 +29,17 @@ ABI, EthereumError, EVMContract, + verifier, ) from manticore.ethereum.plugins import FilterFunctions from manticore.ethereum.solidity import SolidityMetadata from manticore.platforms import evm from manticore.platforms.evm import EVMWorld, ConcretizeArgument, concretized_args, Return, Stop from manticore.utils.deprecated import ManticoreDeprecationWarning +from manticore.utils import config +import io +import contextlib + solver = Z3Solver.instance() @@ -62,6 +69,33 @@ def test_int_ovf(self): self.assertIn("Unsigned integer overflow at MUL instruction", all_findings) +class EthVerifierIntegrationTest(unittest.TestCase): + def test_propverif(self): + smtcfg = config.get_group("smt") + smtcfg.solver = smtcfg.solver.yices + with smtcfg.temp_vals(): + smtcfg.solver = smtcfg.solver.yices + + filename = os.path.join(THIS_DIR, "contracts/prop_verifier.sol") + f = io.StringIO() + with contextlib.redirect_stdout(f): + verifier.manticore_verifier(filename, "TestToken") + output = f.getvalue() + self.assertIsNotNone( + re.compile( + r".*crytic_test_balance\s*\|\s*failed\s*\([0-9a-f]+\).*", re.DOTALL + ).match(output) + ) + self.assertIsNotNone( + re.compile(r".*crytic_test_must_revert\s*\|\s*passed.*", re.DOTALL).match(output) + ) + + def test_propverif_external(self) -> None: + cli_version = subprocess.check_output(("manticore-verifier", "--version")).decode("utf-8") + py_version = f"Manticore {pkg_resources.get_distribution('manticore').version}\n" + self.assertEqual(cli_version, py_version) + + class EthAbiTests(unittest.TestCase): _multiprocess_can_split = True @@ -93,7 +127,7 @@ def test_parse_tx(self): } } """ - user_account = m.create_account(balance=1000000, name="user_account") + user_account = m.create_account(balance=10 ** 10, name="user_account") contract_account = m.solidity_create_contract( source_code, owner=user_account, name="contract_account", gas=36225 ) @@ -684,7 +718,7 @@ def test_function_name_collision(self): def test_check_jumpdest_symbolic_pc(self): """ In Manticore 0.2.4 (up to 6804661) when run with DetectIntegerOverflow, - the EVM.pc is tainted and so it becomes a Constant and so a check in EVM._check_jumpdest: + the EVM.pc is tainted and so it becomes a Constant and so a check in EVM._need_check_jumpdest: self.pc in self._valid_jumpdests failed (because we checked if the object is in a list of integers...). @@ -993,20 +1027,16 @@ class TestPlugin(Plugin): """ def did_evm_execute_instruction_callback(self, state, instruction, arguments, result): - try: - world = state.platform - if world.current_transaction.sort == "CREATE": - name = "init" - else: - name = "rt" - - # collect all end instructions based on whether they are in init or rt - if instruction.is_endtx: - with self.locked_context(name) as d: - d.append(instruction.pc) - except Exception as e: - print(e) - raise + world = state.platform + if world.current_transaction.sort == "CREATE": + name = "init" + else: + name = "rt" + + # collect all end instructions based on whether they are in init or rt + if instruction.is_endtx: + with self.locked_context(name) as d: + d.append(instruction.pc) mevm = self.mevm p = TestPlugin() diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py index c377ddd9e..3050b900f 100644 --- a/tests/other/test_smtlibv2.py +++ b/tests/other/test_smtlibv2.py @@ -688,6 +688,15 @@ def test_constant_folding_udiv(self): self.assertItemsEqual(z.taint, ("important", "stuff")) self.assertEqual(z.value, 0x7FFFFFFF) + def test_simplify_OR(self): + cs = ConstraintSet() + bf = BoolConstant(False) + bt = BoolConstant(True) + var = cs.new_bool() + cs.add(simplify(Operators.OR(var, var)) == var) + cs.add(simplify(Operators.OR(var, bt)) == bt) + self.assertTrue(self.solver.check(cs)) + def testBasicReplace(self): """ Add """ a = BitVecConstant(32, 100)