search

trailofbits / deepstate

A unit test-like interface for fuzzing and symbolic execution
Apache License 2.0
814 stars 99 forks source link

Tests examples fail with "SimSegfaultException" on docker #359

Closed rocky01 closed 2 years ago

rocky01 commented 4 years ago

I try to learn how to write tests based on symbolic execution but I stuck on examples. All examples finish with exception "SimSegfaultException".

Environment:

$ lsb_release -a
LSB Version:    1.4
Distributor ID: Arch
Description:    Arch Linux
Release:        rolling
Codename:       n/a
$ uname -a
Linux XXX 5.7.12-arch1-1 #1 SMP PREEMPT Fri, 31 Jul 2020 17:38:22 +0000 x86_64 GNU/Linux
$ docker --version
Docker version 19.03.12-ce, build 48a66213fe

Steps to reproduce

$ docker build -t deepstate-base -f docker/base/Dockerfile docker/base
$ docker build -t deepstate --build-arg make_j=6 -f ./docker/Dockerfile .
$ docker run -it deepstate bash
user@a17bc44fd259:~/deepstate$ cd build/examples
user@a17bc44fd259:~/deepstate/build/examples$ deepstate-angr ./Runlen

Expected Result

Finish without exception.

Actual Result

user@c0fbeddcfdb3:~/deepstate/build/examples$ deepstate-angr ./Runlen
INFO:deepstate:Setting log level from DEEPSTATE_LOG: 2
INFO:deepstate.core.base:Setting log level from --min_log_level: 2
Traceback (most recent call last):
  File "/usr/local/bin/deepstate-angr", line 33, in <module>
    sys.exit(load_entry_point('deepstate==0.1', 'console_scripts', 'deepstate-angr')())
  File "/usr/local/lib/python3.6/dist-packages/deepstate-0.1-py3.6.egg/deepstate/executors/symex/angr.py", line 514, in main
    return main_unit_test(args, project)
  File "/usr/local/lib/python3.6/dist-packages/deepstate-0.1-py3.6.egg/deepstate/executors/symex/angr.py", line 434, in main_unit_test
    angr.options.STRICT_PAGE_ACCESS})
  File "/home/user/.local/lib/python3.6/site-packages/angr/factory.py", line 99, in entry_state
    return self.project.simos.state_entry(**kwargs)
  File "/home/user/.local/lib/python3.6/site-packages/angr/simos/linux.py", line 321, in state_entry
    state.mem[sym.rebased_addr].long = val
  File "/home/user/.local/lib/python3.6/site-packages/angr/state_plugins/view.py", line 213, in __setattr__
    return self.__getattr__(k).store(v)
  File "/home/user/.local/lib/python3.6/site-packages/angr/state_plugins/view.py", line 269, in store
    return self._type.store(self.state, self._addr, value)
  File "/home/user/.local/lib/python3.6/site-packages/angr/sim_type.py", line 241, in store
    state.memory.store(addr, value, endness=store_endness)
  File "/home/user/.local/lib/python3.6/site-packages/angr/storage/memory.py", line 572, in store
    self._store(request) #will use state_plugins/symbolic_memory.py
  File "/home/user/.local/lib/python3.6/site-packages/angr/state_plugins/symbolic_memory.py", line 819, in _store
    self._insert_memory_object(store_item['value'], store_item['addr'], store_item['size'])
  File "/home/user/.local/lib/python3.6/site-packages/angr/state_plugins/symbolic_memory.py", line 836, in _insert_memory_object
    self.mem.store_memory_object(mo)
  File "/home/user/.local/lib/python3.6/site-packages/angr/storage/paged_memory.py", line 783, in store_memory_object
    self._apply_object_to_page(p, mo, overwrite=overwrite)
  File "/home/user/.local/lib/python3.6/site-packages/angr/storage/paged_memory.py", line 761, in _apply_object_to_page
    raise SimSegfaultError(mo.base, 'non-writable')
angr.errors.SimSegfaultException: 0x4faa50 (non-writable)
agroce commented 4 years ago

I'll build latest docker (though on mac, not arch linux, probably) and see if this is arch/your setup specific, or can be reproduced, sometime this week.

agroce commented 4 years ago

Ok, took me a while to build latest, but I get this too, with exception build doesn't exist, I have to cd to build_deepstate:

user@153562b20972:~/deepstate$ cd build_deepstate
user@153562b20972:~/deepstate/build_deepstate$ cd examples
user@153562b20972:~/deepstate/build_deepstate/examples$ deepstate-angr ./Runlen 
INFO:deepstate:Setting log level from DEEPSTATE_LOG: 2
INFO:deepstate.core.base:Setting log level from --min_log_level: 2
Traceback (most recent call last):
  File "/usr/local/bin/deepstate-angr", line 11, in <module>
    load_entry_point('deepstate==0.1', 'console_scripts', 'deepstate-angr')()
  File "/usr/local/lib/python3.6/dist-packages/deepstate-0.1-py3.6.egg/deepstate/executors/symex/angr.py", line 514, in main
    return main_unit_test(args, project)
  File "/usr/local/lib/python3.6/dist-packages/deepstate-0.1-py3.6.egg/deepstate/executors/symex/angr.py", line 434, in main_unit_test
    angr.options.STRICT_PAGE_ACCESS})
  File "/home/user/.local/lib/python3.6/site-packages/angr/factory.py", line 99, in entry_state
    return self.project.simos.state_entry(**kwargs)
  File "/home/user/.local/lib/python3.6/site-packages/angr/simos/linux.py", line 319, in state_entry
    state.mem[sym.rebased_addr].long = val
  File "/home/user/.local/lib/python3.6/site-packages/angr/state_plugins/view.py", line 213, in __setattr__
    return self.__getattr__(k).store(v)
  File "/home/user/.local/lib/python3.6/site-packages/angr/state_plugins/view.py", line 269, in store
    return self._type.store(self.state, self._addr, value)
  File "/home/user/.local/lib/python3.6/site-packages/angr/sim_type.py", line 188, in store
    state.memory.store(addr, value, endness=store_endness)
  File "/home/user/.local/lib/python3.6/site-packages/angr/storage/memory.py", line 572, in store
    self._store(request) #will use state_plugins/symbolic_memory.py
  File "/home/user/.local/lib/python3.6/site-packages/angr/state_plugins/symbolic_memory.py", line 819, in _store
    self._insert_memory_object(store_item['value'], store_item['addr'], store_item['size'])
  File "/home/user/.local/lib/python3.6/site-packages/angr/state_plugins/symbolic_memory.py", line 836, in _insert_memory_object
    self.mem.store_memory_object(mo)
  File "/home/user/.local/lib/python3.6/site-packages/angr/storage/paged_memory.py", line 783, in store_memory_object
    self._apply_object_to_page(p, mo, overwrite=overwrite)
  File "/home/user/.local/lib/python3.6/site-packages/angr/storage/paged_memory.py", line 761, in _apply_object_to_page
    raise SimSegfaultError(mo.base, 'non-writable')
angr.errors.SimSegfaultException: 0x704a90 (non-writable)
agroce commented 4 years ago 
~/deepstate/build_deepstate/examples$ deepstate-manticore ./Runlen
INFO:deepstate:Setting log level from DEEPSTATE_LOG: 2
INFO:deepstate.core.base:Setting log level from --min_log_level: 2
2020-08-20 18:47:20,253: [31] m.n.manticore:INFO: Loading program ./Runlen
2020-08-20 18:47:22,649: [31] m.n.manticore:INFO: Loading program ./Runlen
WARNING:deepstate.core.symex:Argument `--output_test_dir` not given, will not save test cases.
WARNING:deepstate.core.symex:Argument `--output_test_dir` not given, will not save test cases.
2020-08-20 18:47:27,864: [31] m.c.worker:ERROR: Exception in state 0: SolverException('Error in smtlib: (error "line 3 column 44: invalid parameter, unknown module \'tactic\'")\n',)
Traceback (most recent call last):
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/worker.py", line 121, in run
    current_state.execute()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/native/state.py", line 46, in execute
    result = self._platform.execute()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/platforms/linux.py", line 2760, in execute
    self.current.execute()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/native/cpu/abstractcpu.py", line 980, in execute
    self._publish("will_execute_instruction", self._last_pc, insn)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/utils/event.py", line 146, in _publish
    self._publish_impl(_name, *args, **kwargs)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/utils/event.py", line 163, in _publish_impl
    sink._publish_impl(_name, *args, **kwargs)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/utils/event.py", line 163, in _publish_impl
    sink._publish_impl(_name, *args, **kwargs)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/utils/event.py", line 161, in _publish_impl
    sink._publish_impl(_name, self, *args, **kwargs)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/utils/event.py", line 154, in _publish_impl
    callback(robj(), *args, **kwargs)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/native/manticore.py", line 266, in _hook_callback
    cb(state)
  File "/usr/local/lib/python3.6/dist-packages/deepstate-0.1-py3.6.egg/deepstate/executors/symex/manticore.py", line 264, in <lambda>
    return lambda state: state.invoke_model(func)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/native/state.py", line 98, in invoke_model
    self._platform.invoke_model(model, prefix_args=(self,))
  File "/home/user/.local/lib/python3.6/site-packages/manticore/platforms/platform.py", line 55, in invoke_model
    self._function_abi.invoke(model, prefix_args)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/native/cpu/abstractcpu.py", line 370, in invoke
    result = model(*arguments)
  File "/usr/local/lib/python3.6/dist-packages/deepstate-0.1-py3.6.egg/deepstate/executors/symex/manticore.py", line 169, in hook_Assume
    DeepManticore(state).api_assume(arg, expr_ea, file_ea, line)
  File "/usr/local/lib/python3.6/dist-packages/deepstate-0.1-py3.6.egg/deepstate/core/symex.py", line 439, in api_assume
    if not self.add_constraint(constraint):
  File "/usr/local/lib/python3.6/dist-packages/deepstate-0.1-py3.6.egg/deepstate/executors/symex/manticore.py", line 141, in add_constraint
    return self.state.is_feasible()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/state.py", line 324, in is_feasible
    return self.can_be_true(True)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/state.py", line 328, in can_be_true
    return self._solver.can_be_true(self._constraints, expr)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/state.py", line 311, in _solver
    return Z3Solver.instance()  # solver
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 65, in instance
    cls.__singleton_instances[(pid, tid)] = cls()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 180, in __init__
    self.version = self._solver_version()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 209, in _solver_version
    self._received_version = self._recv()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 335, in _recv
    raise SolverException(f"Error in smtlib: {bufl[0]}")
manticore.core.smtlib.solver.SolverException: Error in smtlib: (error "line 3 column 44: invalid parameter, unknown module 'tactic'")

2020-08-20 18:47:28,009: [31] m.c.worker:ERROR: Exception in state 0: SolverException('Error in smtlib: (error "line 3 column 44: invalid parameter, unknown module \'tactic\'")\n',)
Traceback (most recent call last):
  File "/home/user/.local/lib/python3.6/site-packages/manticore/native/state.py", line 46, in execute
    result = self._platform.execute()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/platforms/linux.py", line 2760, in execute
    self.current.execute()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/native/cpu/abstractcpu.py", line 971, in execute
    raise ConcretizeRegister(self, "PC", policy="ALL")
manticore.native.cpu.abstractcpu.ConcretizeRegister: (<manticore.native.cpu.x86.AMD64Cpu object at 0x7f85d6458c18>, 'PC')

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/worker.py", line 121, in run
    current_state.execute()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/native/state.py", line 60, in execute
    raise Concretize(str(e), expression=expression, setstate=setstate, policy=e.policy)
manticore.core.state.Concretize

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/worker.py", line 142, in run
    m._fork(current_state, exc.expression, exc.policy, exc.setstate)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/manticore.py", line 412, in _fork
    solutions = state.concretize(expression, policy)
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/state.py", line 301, in concretize
    vals = self._solver.get_all_values(
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/state.py", line 311, in _solver
    return Z3Solver.instance()  # solver
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 65, in instance
    cls.__singleton_instances[(pid, tid)] = cls()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 180, in __init__
    self.version = self._solver_version()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 209, in _solver_version
    self._received_version = self._recv()
  File "/home/user/.local/lib/python3.6/site-packages/manticore/core/smtlib/solver.py", line 335, in _recv
    raise SolverException(f"Error in smtlib: {bufl[0]}")
manticore.core.smtlib.solver.SolverException: Error in smtlib: (error "line 3 column 44: invalid parameter, unknown module 'tactic'")

fails with manticore, too, though maybe for different reasons...

agroce commented 4 years ago

Same results with, e.g., ./IntegerArithmetic as well, so it's not just Runlen

agroce commented 4 years ago

@rocky01 thanks for pointing this out, it seems to be a serious issue with symbolic execution. @pgoodman @ggrieco-tob any ideas?

agroce commented 4 years ago

Running non-symbolic, things seem fine (AFL fuzzing looks ok, brute-force fuzzer on these exact executables seems fine

agroce commented 4 years ago

To my non-expert eyes, these look pretty different. Manticore seems to be a mismatch with smtlib call parameters, and I'm wondering if the fact we install Manticore in Docker via: git+git://github.com/trailofbits/manticore.git is involved. Maybe that's an out of date Manticore for other packages we're getting through the angr installation.

OTOH, angr looks like it's just doing something very bad with memory, in the simulated run later? I think these might should be separate issues.

agroce commented 4 years ago

@feliam says we can maybe fix the Manticore issue (and speed up Manticore symex a lot) by switching to yikes:

#install yices
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2

consts = config.get_group("smt")
consts.solver=SolverType.yice
#consts.yices_bin="/usr/bin/yices-smt2"

I'll probably do this soonish, but if someone else wants to try first, go ahead, I have classes to teach for a bit...

agroce commented 4 years ago

Ok, the Manticore issue, which seems separate is fixed. I believe manticore should work for you now, @rocky01 -- I will talk to angr folks about what is going there, when I get a chance (busy with classes, so it may take a little time). But symex via manticore will (A) work and (B) probably be faster than it used to be, thanks to solver change