Improvements. Now hooking fewer functions, and instead making on big array symbolic. This will make it easier to run the inputs concretely (by eventually filling in the array with the concrete bytes), and will also make possible fuzzer integration (where the fuzzer mutates the bytes of the array) possible.
This commit is contained in:
Peter Goodman
+71
-48
@@ -14,8 +14,18 @@
|
||||
# limitations under the License.
|
||||
|
||||
import angr
|
||||
import logging
|
||||
import sys
|
||||
|
||||
L = logging.getLogger("mctest")
|
||||
L.setLevel(logging.INFO)
|
||||
|
||||
def hook_function(project, name, cls):
|
||||
"""Hook the function `name` with the SimProcedure `cls`."""
|
||||
project.hook(project.kb.labels.lookup(name),
|
||||
cls(project=project))
|
||||
|
||||
|
||||
def read_c_string(state, ea):
|
||||
"""Read a concrete NUL-terminated string from `ea`."""
|
||||
assert isinstance(ea, (int, long))
|
||||
@@ -31,67 +41,87 @@ def read_c_string(state, ea):
|
||||
return "".join(chars)
|
||||
|
||||
|
||||
def read_uint64_t(state, ea):
|
||||
def read_uintptr_t(state, ea):
|
||||
"""Read a uint64_t value from memory."""
|
||||
return state.solver.eval(state.mem[ea].uint64_t.resolved,
|
||||
cast_to=int)
|
||||
return state.solver.eval(state.mem[ea].uintptr_t.resolved, cast_to=int)
|
||||
|
||||
|
||||
def read_uint32_t(state, ea):
|
||||
"""Read a uint64_t value from memory."""
|
||||
return state.solver.eval(state.mem[ea].uint32_t.resolved, cast_to=int)
|
||||
|
||||
|
||||
def find_test_cases(project, state):
|
||||
"""Find the test case descriptors."""
|
||||
obj = project.loader.main_object
|
||||
tests = []
|
||||
addr_size_bytes = state.arch.bits // 8
|
||||
for sec in obj.sections:
|
||||
if sec.name != ".mctest_entrypoints":
|
||||
continue
|
||||
|
||||
for ea in xrange(sec.vaddr, sec.vaddr + sec.memsize, 32):
|
||||
test_func_ea = read_uint64_t(state, ea + 0)
|
||||
test_name_ea = read_uint64_t(state, ea + 8)
|
||||
file_name_ea = read_uint64_t(state, ea + 16)
|
||||
file_line_num = read_uint64_t(state, ea + 24)
|
||||
test_func_ea = read_uintptr_t(state, ea + 0 * addr_size_bytes)
|
||||
test_name_ea = read_uintptr_t(state, ea + 1 * addr_size_bytes)
|
||||
file_name_ea = read_uintptr_t(state, ea + 2 * addr_size_bytes)
|
||||
file_line_num = read_uint32_t(state, ea + 3 * addr_size_bytes)
|
||||
|
||||
if not test_func_ea or \
|
||||
not test_name_ea or \
|
||||
not file_name_ea or \
|
||||
not file_line_num: # `__LINE__` in C always starts at `1` ;-)
|
||||
continue
|
||||
|
||||
test_name = read_c_string(state, test_name_ea)
|
||||
file_name = read_c_string(state, file_name_ea)
|
||||
|
||||
L.info("Test case {} at {:x} is at {}:{}".format(
|
||||
test_name, test_func_ea, file_name, file_line_num))
|
||||
tests.append((test_func_ea, test_name, file_name, file_line_num))
|
||||
|
||||
return tests
|
||||
|
||||
|
||||
def hook_symbolic_int_func(project, state, name, num_bits):
|
||||
"""Hook a McTest function and make it return a symbolic integer."""
|
||||
class Function(angr.SimProcedure):
|
||||
def run(self):
|
||||
return self.state.solver.BVS("", num_bits)
|
||||
|
||||
func_name = "McTest_{}".format(name)
|
||||
ea = project.kb.labels.lookup(func_name)
|
||||
project.hook(ea, Function(project=project))
|
||||
def make_symbolic_input(project, state):
|
||||
"""Fill in the input data array with symbolic data."""
|
||||
obj = project.loader.main_object
|
||||
for sec in obj.sections:
|
||||
if sec.name == ".mctest_input_data":
|
||||
data = state.se.Unconstrained('MCTEST_INPUT', sec.memsize * 8)
|
||||
state.memory.store(sec.vaddr, data)
|
||||
return data
|
||||
|
||||
|
||||
def hook_predicate_int_func(project, state, name, num_bits):
|
||||
"""Hook a McTest function that checks whether or not its integer argument
|
||||
is symbolic."""
|
||||
class Function(angr.SimProcedure):
|
||||
class Hook(angr.SimProcedure):
|
||||
def run(self, arg):
|
||||
return int(self.state.se.symbolic(arg))
|
||||
|
||||
func_name = "McTest_IsSymbolic{}".format(name)
|
||||
ea = project.kb.labels.lookup(func_name)
|
||||
project.hook(ea, Function(project=project))
|
||||
hook_function(project, "McTest_IsSymbolic{}".format(name), Hook)
|
||||
|
||||
|
||||
class Assume(angr.SimProcedure):
|
||||
"""Implements McTest_Assume, which injects a constraint."""
|
||||
"""Implements _McTest_CanAssume, which tries to inject a constraint."""
|
||||
def run(self, arg):
|
||||
if self.state.se.symbolic(arg):
|
||||
constraint = arg != 0
|
||||
eval_res = self.state.se.eval(constraint)
|
||||
if eval_res:
|
||||
self.state.add_constraints(constraint)
|
||||
ret = eval_res
|
||||
else:
|
||||
ret = self.state.se.eval(arg) != 0
|
||||
return int(ret)
|
||||
constraint = arg != 0
|
||||
self.state.solver.add(constraint)
|
||||
if not self.state.solver.satisfiable():
|
||||
L.error("Failed to assert assumption {}".format(constraint))
|
||||
self.exit(2)
|
||||
|
||||
|
||||
class Pass(angr.SimProcedure):
|
||||
"""Implements McTest_Pass, which notifies us of a passing test."""
|
||||
def run(self):
|
||||
L.info("Passed test case")
|
||||
self.exit(0)
|
||||
|
||||
|
||||
class Fail(angr.SimProcedure):
|
||||
"""Implements McTest_Fail, which notifies us of a passing test."""
|
||||
def run(self):
|
||||
L.error("Failed test case")
|
||||
self.exit(1)
|
||||
|
||||
|
||||
def main():
|
||||
@@ -103,7 +133,8 @@ def main():
|
||||
sys.argv[1],
|
||||
use_sim_procedures=True,
|
||||
translation_cache=True,
|
||||
support_selfmodifying_code=False)
|
||||
support_selfmodifying_code=False,
|
||||
auto_load_libs=False)
|
||||
|
||||
entry_state = project.factory.entry_state()
|
||||
addr_size_bits = entry_state.arch.bits
|
||||
@@ -119,23 +150,16 @@ def main():
|
||||
concrete_manager.explore(find=ea_of_main)
|
||||
main_state = concrete_manager.found[0]
|
||||
|
||||
#concrete_manager.move(from_stash='found', to_stash='deadended')
|
||||
|
||||
# Hook functions that should now return symbolic values.
|
||||
hook_symbolic_int_func(project, main_state, 'Bool', 1)
|
||||
hook_symbolic_int_func(project, main_state, 'Size', addr_size_bits)
|
||||
hook_symbolic_int_func(project, main_state, 'UInt64', 64)
|
||||
hook_symbolic_int_func(project, main_state, 'UInt', 32)
|
||||
# Introduce symbolic input that the tested code will use.
|
||||
symbolic_input = make_symbolic_input(project, main_state)
|
||||
|
||||
# Hook predicate functions that should return 1 or 0 depending on whether
|
||||
# or not their argument is symbolic.
|
||||
hook_predicate_int_func(project, main_state, 'UInt', 32)
|
||||
|
||||
# Hook the assume function.
|
||||
project.hook(project.kb.labels.lookup('McTest_Assume'),
|
||||
Assume(project=project))
|
||||
|
||||
ea_of_done = project.kb.labels.lookup('McTest_DoneTestCase')
|
||||
hook_function(project, '_McTest_Assume', Assume)
|
||||
hook_function(project, 'McTest_Pass', Pass)
|
||||
hook_function(project, 'McTest_Fail', Fail)
|
||||
|
||||
# For each test, create a simulation manager whose initial state calls into
|
||||
# the test case function, and returns to `McTest_DoneTestCase`.
|
||||
@@ -143,8 +167,7 @@ def main():
|
||||
for entry_ea, test_name, file_name, line_num in tests:
|
||||
test_state = project.factory.call_state(
|
||||
entry_ea,
|
||||
base_state=main_state,
|
||||
ret_addr=ea_of_done)
|
||||
base_state=main_state)
|
||||
|
||||
# NOTE(pag): Enabling Veritesting seems to miss some cases where the
|
||||
# tests fail.
|
||||
@@ -152,13 +175,13 @@ def main():
|
||||
project=project,
|
||||
active_states=[test_state])
|
||||
|
||||
L.info("Running test case {}".format(test_name))
|
||||
test_manager.run()
|
||||
|
||||
for state in test_manager.deadended:
|
||||
last_event = state.history.events[-1]
|
||||
if 'terminate' == last_event.type:
|
||||
code = last_event.objects['exit_code']._model_concrete.value
|
||||
print "{} in {}:{} terminated with {}".format(test_name, file_name, line_num, code)
|
||||
|
||||
return 0
|
||||
|
||||
|
||||
Reference in New Issue
Block a user