8591bff45f
* WIP New Policy class * WIP pubsub * Update Signal tests * EVM support - Wip * EVM support - dependencies fixed * EVM support - fix decree merge * fix decode instrucion event * Fix small bugs in evm opcodes (too many arguments + wrong LOG name) (#380) Fix wrong call parameters + typo * Fix Create/Call * Fix depth * Default fixed point in arithmetic simplifier * small fixes from github comments * Fix event decode_instruction signature * wip wip * Auto tests for evm * New EVM tests * Ran 9556 FAILED (failures=166, errors=8, skipped=62) * Fix some arithmetic instructions * Ran 9556 FAILED (failures=136, errors=8, skipped=62) * More instructions - Optimizing symbolic memory * Added gas to opcodes description - FIX DELEGATECALL POPS * Add wip wallet example * The tests * Solidity constructors need argument after bytecode * Simple integer overflow working * Good merge * Good good merge * WIP manticore refactor * Fix default old-style initial state * context now working * Fix context serialization * Fix test models. Can not set a state constraints * typo * A few typos (constraints setter) and use of public properties in internal methods * Fix init wallet example * State __init__ needs to initialize platform constraints * Internal methods use internal properties * Better attack modeling * Better example layout * Storage backup on CALL is now faster .. and correct * Add LOG support * Minimal SE test * Added examples * Send ether bugfix * EVM: Fix wrong balance destination on CALL + decrease caller balance on CREATE * New balance management * Trying to maintain known hashes * Known hash concretization policy * CALLDATA max size bugfix * Minimal SE example * Remove evm tests * add -> enqueue * @m.init * Fix workspace url * Some test skipped * Ad Fixme to platform specific stuff in State * add -> enqueue * Enqueue created state * Fix m.init Use a messy hack to adhere to the spec (callback func receive 1 state argument) * Add _coverage_file ivar to Manticore * Fix symbolic files * remove extra enqueue * Fixing __main__ * comments * Fix visitors oddity * setup merged * remove duplicates and add pysha3 * Remove EVMTests import * Refactor platform specific code out of ManticoreOutput (#505) * Initial moving work * Clean * Make linux.generate_workspace_files work * Fix * clean * Add test * Test workspace for platform files * Skip EVM cpu pretty print * Remove bad import * Fix coverage.py for testing * Clean comment * Comment hack * Print evm cpu * pretty print evm world instead of platform * delet old scripts/examples * delet old tests * Remove z3 install script * Array.max_size can be None, include check for that * Rm unused _symbolic_files add_symbolic_files was moved to linux, so this is not needed * Rm unused args * Import evm * Rm dup function * Rm stray prints * Add docs for new classmethod apis * minimal * minimal example * fix minimal * Fair symbolic SHA3 handling * Simple mapping example * coverage example * fix tests * fix minimal * Some eko fixes * New SETH * integer_overflow refactored * Fixing the examples * init_bytecode -> init ' * Concrete reentrancy exampole * concrete reentrancy selfdestruct * Update minimal.py * It's a new Minimal * Integer overflow example * New minimal * minimal fix * Examples last minute fixes * Remove debug print * add plugin.py * Fixing event subscription * remove temp params * Remove param * Update uncovered will_exec callback prototype * Clean up debug output * Automatically generated intruction tests * Uninplemented instruction test removed * Unused concretization policy removed * Fixes enabling default bplugins * solc from PATH * Removed unused import * Logger name updated
268 lines
8.9 KiB
Python
268 lines
8.9 KiB
Python
import unittest
|
|
from manticore.utils.event import Eventful
|
|
from manticore.platforms import linux
|
|
from manticore.core.state import State
|
|
from manticore.core.smtlib import BitVecVariable, ConstraintSet
|
|
|
|
class _CallbackExecuted(Exception):
|
|
pass
|
|
|
|
|
|
class FakeMemory(object):
|
|
def __init__(self):
|
|
self._constraints = None
|
|
|
|
@property
|
|
def constraints(self):
|
|
return self._constraints
|
|
|
|
@constraints.setter
|
|
def constraints(self, constraints):
|
|
self._constraints = constraints
|
|
|
|
class FakeCpu(object):
|
|
def __init__(self):
|
|
self._memory = FakeMemory()
|
|
|
|
@property
|
|
def memory(self):
|
|
return self._memory
|
|
|
|
class FakePlatform(Eventful):
|
|
def __init__(self):
|
|
super(FakePlatform, self).__init__()
|
|
self._constraints = None
|
|
self.procs = [FakeCpu()]
|
|
|
|
|
|
|
|
def __getstate__(self):
|
|
state = super(FakePlatform, self).__getstate__()
|
|
state['cons'] = self._constraints
|
|
state['procs'] = self.procs
|
|
return state
|
|
def __setstate__(self, state):
|
|
super(FakePlatform, self).__setstate__(state)
|
|
self._constraints = state['cons']
|
|
self.procs = state['procs']
|
|
|
|
|
|
@property
|
|
def current(self):
|
|
return self.procs[0]
|
|
|
|
@property
|
|
def constraints(self):
|
|
return self._constraints
|
|
|
|
@constraints.setter
|
|
def constraints(self, constraints):
|
|
self._constraints = constraints
|
|
for proc in self.procs:
|
|
proc.memory.constraints = constraints
|
|
|
|
|
|
|
|
class StateTest(unittest.TestCase):
|
|
_multiprocess_can_split_ = True
|
|
def setUp(self):
|
|
l = linux.Linux('/bin/ls')
|
|
self.state = State(ConstraintSet(), l)
|
|
|
|
def test_solve_one(self):
|
|
val = 42
|
|
expr = BitVecVariable(32, 'tmp')
|
|
self.state.constrain(expr == val)
|
|
solved = self.state.solve_one(expr)
|
|
self.assertEqual(solved, val)
|
|
|
|
def test_solve_n(self):
|
|
expr = BitVecVariable(32, 'tmp')
|
|
self.state.constrain(expr > 4)
|
|
self.state.constrain(expr < 7)
|
|
solved = self.state.solve_n(expr, 2)
|
|
self.assertEqual(solved, [5,6])
|
|
|
|
def test_solve_n2(self):
|
|
expr = BitVecVariable(32, 'tmp')
|
|
self.state.constrain(expr > 4)
|
|
self.state.constrain(expr < 100)
|
|
solved = self.state.solve_n(expr, 5)
|
|
self.assertEqual(len(solved), 5)
|
|
|
|
def test_policy_one(self):
|
|
expr = BitVecVariable(32, 'tmp')
|
|
self.state.constrain(expr > 0)
|
|
self.state.constrain(expr < 100)
|
|
solved = self.state.concretize(expr, 'ONE')
|
|
self.assertEqual(len(solved), 1)
|
|
self.assertIn(solved[0], xrange(100))
|
|
|
|
def test_state(self):
|
|
constraints = ConstraintSet()
|
|
initial_state = State(constraints, FakePlatform())
|
|
|
|
arr = initial_state.symbolicate_buffer('+'*100, label='SYMBA')
|
|
initial_state.constrain(arr[0] > 0x41)
|
|
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
|
|
with initial_state as new_state:
|
|
|
|
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
|
|
self.assertTrue(len(new_state.constraints.declarations) == 1 )
|
|
arrb = new_state.symbolicate_buffer('+'*100, label='SYMBB')
|
|
|
|
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
|
|
self.assertTrue(len(new_state.constraints.declarations) == 1 )
|
|
|
|
new_state.constrain(arrb[0] > 0x42)
|
|
|
|
|
|
self.assertTrue(len(new_state.constraints.declarations) == 2 )
|
|
|
|
|
|
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
|
|
|
|
def test_new_symbolic_buffer(self):
|
|
length = 64
|
|
expr = self.state.new_symbolic_buffer(length)
|
|
self.assertEqual(len(expr), length)
|
|
|
|
def test_new_symbolic_value(self):
|
|
length = 64
|
|
expr = self.state.new_symbolic_value(length)
|
|
self.assertEqual(expr.size, length)
|
|
|
|
def test_new_bad_symbolic_value(self):
|
|
length = 62
|
|
with self.assertRaises(Exception):
|
|
expr = self.state.new_symbolic_value(length)
|
|
|
|
def test_tainted_symbolic_buffer(self):
|
|
taint = ('TEST_TAINT', )
|
|
expr = self.state.new_symbolic_buffer(64, taint=taint)
|
|
self.assertEqual(expr.taint, frozenset(taint))
|
|
|
|
def test_tainted_symbolic_value(self):
|
|
taint = ('TEST_TAINT', )
|
|
expr = self.state.new_symbolic_value(64, taint=taint)
|
|
self.assertEqual(expr.taint, frozenset(taint))
|
|
|
|
def testContextSerialization(self):
|
|
import cPickle as pickle
|
|
initial_file = ''
|
|
new_file = ''
|
|
new_new_file = ''
|
|
constraints = ConstraintSet()
|
|
initial_state = State(constraints, FakePlatform())
|
|
initial_state.context['step'] = 10
|
|
initial_file = pickle.dumps(initial_state)
|
|
with initial_state as new_state:
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 10)
|
|
|
|
new_state.context['step'] = 20
|
|
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
new_file = pickle.dumps(new_state)
|
|
|
|
with new_state as new_new_state:
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
self.assertEqual( new_new_state.context['step'], 20)
|
|
|
|
new_new_state.context['step'] += 10
|
|
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
self.assertEqual( new_new_state.context['step'], 30)
|
|
|
|
new_new_file = pickle.dumps(new_new_state)
|
|
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
self.assertEqual( new_new_state.context['step'], 30)
|
|
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
|
|
del initial_state
|
|
del new_state
|
|
del new_new_state
|
|
|
|
|
|
|
|
initial_state = pickle.loads(initial_file)
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
new_state = pickle.loads(new_file)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
new_new_state = pickle.loads(new_new_file)
|
|
self.assertEqual( new_new_state.context['step'], 30)
|
|
|
|
|
|
def _test_state_gen_helper(self, name, msg):
|
|
self.assertEqual(name, 'statename')
|
|
self.assertEqual(msg, 'statemsg')
|
|
raise _CallbackExecuted
|
|
|
|
def testContextSerialization(self):
|
|
import cPickle as pickle
|
|
initial_file = ''
|
|
new_file = ''
|
|
new_new_file = ''
|
|
constraints = ConstraintSet()
|
|
initial_state = State(constraints, FakePlatform())
|
|
initial_state.context['step'] = 10
|
|
initial_file = pickle.dumps(initial_state)
|
|
with initial_state as new_state:
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 10)
|
|
|
|
new_state.context['step'] = 20
|
|
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
new_file = pickle.dumps(new_state)
|
|
|
|
with new_state as new_new_state:
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
self.assertEqual( new_new_state.context['step'], 20)
|
|
|
|
new_new_state.context['step'] += 10
|
|
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
self.assertEqual( new_new_state.context['step'], 30)
|
|
|
|
new_new_file = pickle.dumps(new_new_state)
|
|
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
self.assertEqual( new_new_state.context['step'], 30)
|
|
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
|
|
del initial_state
|
|
del new_state
|
|
del new_new_state
|
|
|
|
|
|
|
|
initial_state = pickle.loads(initial_file)
|
|
self.assertEqual( initial_state.context['step'], 10)
|
|
new_state = pickle.loads(new_file)
|
|
self.assertEqual( new_state.context['step'], 20)
|
|
new_new_state = pickle.loads(new_new_file)
|
|
self.assertEqual( new_new_state.context['step'], 30)
|
|
|
|
def test_state_gen(self):
|
|
self.state.subscribe('will_generate_testcase', self._test_state_gen_helper)
|
|
with self.assertRaises(_CallbackExecuted):
|
|
self.state.generate_testcase('statename', 'statemsg')
|