https://github.com/trailofbits/manticore
Tip revision: f863048d6c431589f5274dad8bbe3a0311d41186 authored by feliam on 06 August 2018, 16:35:42 UTC
CC
CC
Tip revision: f863048
__main__.py
import sys
import logging
import argparse
from . import Manticore
from .utils import log
# XXX(yan): This would normally be __name__, but then logger output will be pre-
# pended by 'm.__main__: ', which is not very pleasing. hard-coding to 'main'
logger = logging.getLogger('manticore.main')
sys.setrecursionlimit(10000)
def parse_arguments():
def positive(value):
ivalue = int(value)
if ivalue <= 0:
raise argparse.ArgumentTypeError("Argument must be positive")
return ivalue
parser = argparse.ArgumentParser(description='Symbolic execution tool')
parser.add_argument('--assertions', type=str, default=None,
help=argparse.SUPPRESS)
parser.add_argument('--buffer', type=str,
help=argparse.SUPPRESS)
parser.add_argument('--context', type=str, default=None,
help=argparse.SUPPRESS)
parser.add_argument('--coverage', type=str, default=None,
help='where to write the coverage data')
parser.add_argument('--data', type=str, default='',
help='Initial concrete concrete_data for the input symbolic buffer')
# FIXME (theo) similarly to policy, add documentation here.
disas = ['capstone', 'binja-il']
parser.add_argument('--disasm', type=str, default='capstone', choices=disas,
help=argparse.SUPPRESS)
parser.add_argument('--env', type=str, nargs=1, default=[], action='append',
help='Add an environment variable. Use "+" for symbolic bytes. (VARNAME=++++)')
#TODO allow entry as an address
#parser.add_argument('--entry', type=str, default=None,
# help='address as entry point')
parser.add_argument('--entrysymbol', type=str, default=None,
help='symbol as entry point')
parser.add_argument('--file', type=str, default=[], action='append', dest='files',
help='Specify symbolic input file, \'+\' marks symbolic bytes')
parser.add_argument('--names', type=str, default=None,
help=argparse.SUPPRESS)
parser.add_argument('--offset', type=int, default=16,
help=argparse.SUPPRESS)
# FIXME (theo) Add some documentation on the different search policy options
parser.add_argument('--policy', type=str, default='random',
help=("Search policy. random|adhoc|uncovered|dicount"
"|icount|syscount|depth. (use + (max) or - (min)"
" to specify order. e.g. +random)"))
parser.add_argument('--profile', action='store_true',
help='Enable profiling mode.')
parser.add_argument('--procs', type=int, default=1,
help='Number of parallel processes to spawn')
parser.add_argument('argv', type=str, nargs='+',
help="Path to program, and arguments ('+' in arguments indicates symbolic byte).")
parser.add_argument('--timeout', type=int, default=0,
help='Timeout. Abort exploration aftr TIMEOUT seconds')
parser.add_argument('-v', action='count', default=1,
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_?????)"))
parser.add_argument('--version', action='version', version='Manticore 0.1.10',
help='Show program version information')
parser.add_argument('--txlimit', type=positive,
help='Maximum number of symbolic transactions to run (positive integer) (Ethereum only)')
parser.add_argument('--txnocoverage', action='store_true',
help='Do not use coverage as stopping criteria (Ethereum only)')
parser.add_argument('--txaccount', type=str, default="attacker",
help='Account used as caller in the symbolic transactions, either "attacker" or "owner" (Ethereum only)')
parser.add_argument('--contract', type=str,
help='Contract name to analyze in case of multiple ones (Ethereum only)')
parser.add_argument('--detect-overflow', action='store_true',
help='Enable integer overflow detection (Ethereum only)')
parser.add_argument('--detect-invalid', action='store_true',
help='Enable INVALID instruction detection (Ethereum only)')
parser.add_argument('--detect-uninitialized-memory', action='store_true',
help='Enable detection of uninitialized memory usage (Ethereum only)')
parser.add_argument('--detect-uninitialized-storage', action='store_true',
help='Enable detection of uninitialized storage usage (Ethereum only)')
parser.add_argument('--detect-reentrancy', action='store_true',
help='Enable detection of reentrancy bug (Ethereum only)')
parser.add_argument('--detect-unused-retval', action='store_true',
help='Enable detection of not used internal transaction return value')
parser.add_argument('--detect-all', action='store_true',
help='Enable all detector heuristics (Ethereum only)')
parser.add_argument('--avoid-constant', action='store_true',
help='Avoid exploring constant functions for human transactions (Ethereum only)')
parsed = parser.parse_args(sys.argv[1:])
if parsed.procs <= 0:
parsed.procs = 1
if parsed.policy.startswith('min'):
parsed.policy = '-' + parsed.policy[3:]
elif parsed.policy.startswith('max'):
parsed.policy = '+' + parsed.policy[3:]
return parsed
def ethereum_cli(args):
from .ethereum import ManticoreEVM, DetectInvalid, DetectIntegerOverflow, DetectUninitializedStorage, DetectUninitializedMemory, FilterFunctions, DetectReentrancy, DetectUnusedRetVal
log.init_logging()
m = ManticoreEVM(procs=args.procs)
if args.detect_all or args.detect_invalid:
m.register_detector(DetectInvalid())
if args.detect_all or args.detect_overflow:
m.register_detector(DetectIntegerOverflow())
if args.detect_all or args.detect_uninitialized_storage:
m.register_detector(DetectUninitializedStorage())
if args.detect_all or args.detect_uninitialized_memory:
m.register_detector(DetectUninitializedMemory())
if args.detect_all or args.detect_reentrancy:
m.register_detector(DetectReentrancy())
if args.detect_all or args.detect_unused_retval:
m.register_detector(DetectUnusedRetVal())
if args.avoid_constant:
# avoid all human level tx that has no effect on the storage
filter_nohuman_constants = FilterFunctions(regexp=r".*", depth='human', mutability='constant', include=False)
m.register_plugin(filter_nohuman_constants)
logger.info("Beginning analysis")
m.multi_tx_analysis(args.argv[0], contract_name=args.contract, tx_limit=args.txlimit, tx_use_coverage=not args.txnocoverage, tx_account=args.txaccount)
#TODO unregister all plugins
m.finalize()
def main():
from .manticore import InstructionCounter, Visited, Tracer, RecordSymbolicBranches
log.init_logging()
args = parse_arguments()
Manticore.verbosity(args.v)
# TODO(mark): Temporarily hack ethereum support into manticore cli
if args.argv[0].endswith('.sol'):
ethereum_cli(args)
return
env = {key: val for key, val in [env[0].split('=') for env in args.env]}
m = Manticore(args.argv[0], argv=args.argv[1:], env=env, entry_symbol=args.entrysymbol, workspace_url=args.workspace, policy=args.policy, disasm=args.disasm, concrete_start=args.data)
# Default plugins for now.. FIXME REMOVE!
m.register_plugin(InstructionCounter())
m.register_plugin(Visited())
m.register_plugin(Tracer())
m.register_plugin(RecordSymbolicBranches())
# Fixme(felipe) remove this, move to plugin
m.coverage_file = args.coverage
if args.names is not None:
m.apply_model_hooks(args.names)
if args.assertions:
m.load_assertions(args.assertions)
@m.init
def init(initial_state):
for file in args.files:
initial_state.platform.add_symbolic_file(file)
m.run(procs=args.procs, timeout=args.timeout, should_profile=args.profile)
if __name__ == '__main__':
main()