DeforaNetworks/manticore
3
0
Fork 0
Code Releases Activity

Add --tx flag to control symbolic tx (#667)

Browse Source 
* Add --tx argument that must be a positive int

* Add simple tx_count mode

* Help updates

* Add None default arg

* Implement as upper bound, rather than absolute tx num

* rename to positive
This commit is contained in:
Mark Mossberg 2017-12-22 18:11:14 -05:00 committed by GitHub
parent 2e578acf9d
commit 6499c0e281
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 24 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
manticore/__main__.py
View File

@ -13,8 +13,12 @@ sys.setrecursionlimit(10000)
def parse_arguments():
###########################################################################
# parse arguments
def positive(value):
ivalue = int(value)
if ivalue <= 0:
raise argparse.ArgumentTypeError("Argument must be positive")
return ivalue
parser = argparse.ArgumentParser(description='Dynamic binary analysis tool')
parser.add_argument('--assertions', type=str, default=None,
help=argparse.SUPPRESS)
@ -58,6 +62,9 @@ def parse_arguments():
"(default mcore_?????)"))
parser.add_argument('--version', action='version', version='Manticore 0.1.5',
help='Show program version information')
parser.add_argument('--txlimit', type=positive,
help='Maximum number of symbolic transactions to run (positive integer) (Ethereum only)')
parsed = parser.parse_args(sys.argv[1:])
if parsed.procs <= 0:
@ -84,7 +91,7 @@ def ethereum_cli(args):
logger.info("Beginning analysis")
m.multi_tx_analysis(args.argv[0])
m.multi_tx_analysis(args.argv[0], args.txlimit)
def main():
log.init_logging()

22
manticore/ethereum.py
View File

@ -841,7 +841,7 @@ class ManticoreEVM(Manticore):
return status
def multi_tx_analysis(self, solidity_filename):
def multi_tx_analysis(self, solidity_filename, tx_limit=None):
with open(solidity_filename) as f:
source_code = f.read()
@ -849,18 +849,24 @@ class ManticoreEVM(Manticore):
contract_account = self.solidity_create_contract(source_code, owner=user_account)
attacker_account = self.create_account(balance=1000)
def run_symbolic_tx():
symbolic_data = self.make_symbolic_buffer(320)
symbolic_value = self.make_symbolic_value()
self.transaction(caller=attacker_account,
address=contract_account,
data=symbolic_data,
value=symbolic_value )
prev_coverage = 0
current_coverage = 0
while current_coverage < 100:
run_symbolic_tx()
symbolic_data = self.make_symbolic_buffer(320)
symbolic_value = self.make_symbolic_value()
self.transaction(caller=attacker_account,
address=contract_account,
data=symbolic_data,
value=symbolic_value )
if tx_limit is not None:
tx_limit -= 1
if tx_limit == 0:
break
prev_coverage = current_coverage
current_coverage = self.global_coverage(contract_account)