diff --git a/.github/ISSUE_TEMPLATE.md b/.github/ISSUE_TEMPLATE/bug_report.md similarity index 75% rename from .github/ISSUE_TEMPLATE.md rename to .github/ISSUE_TEMPLATE/bug_report.md index bac3dc61e..9a8c3787f 100644 --- a/.github/ISSUE_TEMPLATE.md +++ b/.github/ISSUE_TEMPLATE/bug_report.md @@ -1,5 +1,14 @@ -### OS / Environment - +--- +name: Bug report +about: Create a report to help us improve Manticore +title: '' +labels: bug +assignees: '' + +--- + +### Summary of the problem + ### Manticore version @@ -7,14 +16,12 @@ ### Python version +### OS / Environment + ### Dependencies - -### Summary of the problem - - ### Step to reproduce the behavior @@ -27,4 +34,3 @@ ### Any relevant logs - diff --git a/.github/ISSUE_TEMPLATE/config.yml b/.github/ISSUE_TEMPLATE/config.yml new file mode 100644 index 000000000..74ffdedfb --- /dev/null +++ b/.github/ISSUE_TEMPLATE/config.yml @@ -0,0 +1,14 @@ +blank_issues_enabled: false +contact_links: + - name: Bug Report + url: https://github.com/trailofbits/manticore/issues/new?labels=bug&template=bug_report.md + about: Report a bug in Manticore + - name: Feature Request + url: https://github.com/trailofbits/manticore/issues/new?labels=idea&template=feature_request.md + about: Request a new feature in Manticore + - name: Ask a Question + url: https://github.com/trailofbits/manticore/discussions/new + about: Ask for help or clarification from the developers + - name: Join our Slack + url: https://empirehacking.slack.com/archives/C3PTWK7UM + about: Engage with other users of Manticore \ No newline at end of file diff --git a/.github/ISSUE_TEMPLATE/feature_request.md b/.github/ISSUE_TEMPLATE/feature_request.md new file mode 100644 index 000000000..cdabf56a8 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/feature_request.md @@ -0,0 +1,20 @@ +--- +name: Feature request +about: Suggest a new feature for Manticore +title: '' +labels: idea +assignees: '' + +--- + +**Is your feature request related to a problem? Please describe.** +A clear and concise description of what the problem is. Ex. I'm always frustrated when [...] + +**Describe the solution you'd like** +A clear and concise description of what you want to happen. + +**Describe alternatives you've considered** +A clear and concise description of any alternative solutions or features you've considered. + +**Additional context** +Add any other context or screenshots about the feature request here. \ No newline at end of file diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 4e54d0e97..b7ec75670 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -18,10 +18,14 @@ instead. ## Questions -Questions can be submitted to the issue tracker, but you may get a faster +Questions can be submitted to the [discussion page](https://github.com/trailofbits/manticore/discussions), but you may get a faster response if you ask in our [chat room](https://empireslacking.herokuapp.com/) (in the #manticore channel). +## Legal +For legal reasons, we require contributors to sign our [Contributor License Agreement](https://cla-assistant.io/trailofbits/manticore). +This will be automatically checked as part of our CI. + ## Code Manticore uses the pull request contribution model. Please make an account on diff --git a/README.md b/README.md index 92c48d42a..3f95e1ca3 100644 --- a/README.md +++ b/README.md @@ -15,47 +15,110 @@ Manticore is a symbolic execution tool for analysis of smart contracts and binaries. -> Note: Beginning with version 0.2.0, Python 3.6+ is required. - ## Features -- **Input Generation**: Manticore automatically generates inputs that trigger unique code paths -- **Error Discovery**: Manticore discovers bugs and produces inputs required to trigger them -- **Execution Tracing**: Manticore records an instruction-level trace of execution for each generated input +- **Program Exploration**: Manticore can execute a program with symbolic inputs and explore all the possible states it can reach +- **Input Generation**: Manticore can automatically produce concrete inputs that result in a given program state +- **Error Discovery**: Manticore can detect crashes and other failure cases in binaries and smart contracts +- **Instrumentation**: Manticore provides fine-grained control of state exploration via event callbacks and instruction hooks - **Programmatic Interface**: Manticore exposes programmatic access to its analysis engine via a Python API Manticore can analyze the following types of programs: - Ethereum smart contracts (EVM bytecode) -- Linux ELF binaries (x86, x86_64 and ARMv7) +- Linux ELF binaries (x86, x86_64, aarch64, and ARMv7) +- WASM Modules + +## Installation + +> Note: We recommend installing Manticore in a [virtual environment](https://packaging.python.org/guides/installing-using-pip-and-virtual-environments/#installing-virtualenv) + to prevent conflicts with other projects or packages + +Option 1: Installing from PyPI: + +```bash +pip install manticore +``` + +Option 2: Installing from PyPI, with extra dependencies needed to execute native binaries: + +```bash +pip install "manticore[native]" +``` + +Option 3: Installing from the `master` branch: + +```bash +git clone https://github.com/trailofbits/manticore.git +cd manticore +pip install -e ".[native]" +``` + +Option 4: Install via Docker: + +```bash +docker pull trailofbits/manticore +``` + +Once installed, the `manticore` CLI tool and Python API will be available. + +For a development installation, see our [wiki](https://github.com/trailofbits/manticore/wiki/Hacking-on-Manticore). ## Usage ### CLI -Manticore has a command line interface which can be used to easily symbolically execute a supported program or smart contract. Analysis results will be placed into a new directory beginning with `mcore_`. +Manticore has a command line interface which can perform a basic symbolic analysis of a binary or smart contract. +Analysis results will be placed into a workspace directory beginning with `mcore_`. For information about the workspace, see the [wiki](https://github.com/trailofbits/manticore/wiki/What's-in-the-workspace%3F). -Use the CLI to explore possible states in Ethereum smart contracts. Manticore includes _detectors_ that flag potentially vulnerable code in discovered states; output from them will be written to stdout and the results directory. +#### EVM Solidity smart contracts must have a `.sol` extension for analysis by Manticore. See a [demo](https://asciinema.org/a/154012). - +
+ Click to expand: + ```bash -$ manticore ./path/to/contract.sol # runs, and creates a mcore_* directory with analysis results +$ manticore examples/evm/umd_example.sol + [9921] m.main:INFO: Registered plugins: DetectUninitializedMemory, DetectReentrancySimple, DetectExternalCallAndLeak, ... + [9921] m.e.manticore:INFO: Starting symbolic create contract + [9921] m.e.manticore:INFO: Starting symbolic transaction: 0 + [9921] m.e.manticore:INFO: 4 alive states, 6 terminated states + [9921] m.e.manticore:INFO: Starting symbolic transaction: 1 + [9921] m.e.manticore:INFO: 16 alive states, 22 terminated states +[13761] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs) +[13754] m.c.manticore:INFO: Generated testcase No. 1 - STOP(3 txs) +... +[13743] m.c.manticore:INFO: Generated testcase No. 36 - THROW(3 txs) +[13740] m.c.manticore:INFO: Generated testcase No. 37 - THROW(3 txs) +[9921] m.c.manticore:INFO: Results in ~/manticore/mcore_gsncmlgx ``` +
-The command line can also be used to simply explore a Linux binary: +#### Native +
+ Click to expand: + ```bash -$ manticore ./path/to/binary # runs, and creates a mcore_* directory with analysis results -$ manticore ./path/to/binary ab cd # use concrete strings "ab", "cd" as program arguments -$ manticore ./path/to/binary ++ ++ # use two symbolic strings of length two as program arguments +$ manticore examples/linux/basic +[9507] m.n.manticore:INFO: Loading program examples/linux/basic +[9507] m.c.manticore:INFO: Generated testcase No. 0 - Program finished with exit status: 0 +[9507] m.c.manticore:INFO: Generated testcase No. 1 - Program finished with exit status: 0 +[9507] m.c.manticore:INFO: Results in ~/manticore/mcore_7u7hgfay +[9507] m.n.manticore:INFO: Total time: 2.8029580116271973 ``` +
-### API -Manticore has a Python programming interface which can be used to implement custom analyses. +### API -For Ethereum smart contracts, it can be used for detailed verification of arbitrary contract properties. Set starting conditions, execute symbolic transactions, then review discovered states to ensure invariants for your contract hold. +Manticore provides a Python programming interface which can be used to implement powerful custom analyses. +#### EVM +For Ethereum smart contracts, the API can be used for detailed verification of arbitrary contract properties. Users can set the starting conditions, +execute symbolic transactions, then review discovered states to ensure invariants for a contract hold. +
+ Click to expand: + ```python from manticore.ethereum import ManticoreEVM contract_src=""" @@ -81,19 +144,22 @@ for state in m.ready_states: print("can value be 1? {}".format(state.can_be_true(value == 1))) print("can value be 200? {}".format(state.can_be_true(value == 200))) ``` +
-It is also possible to use the API to create custom analysis tools for Linux binaries. - +#### Native +It is also possible to use the API to create custom analysis tools for Linux binaries. Tailoring the initial state helps avoid state explosion +problems that commonly occur when using the CLI. +
+ Click to expand: + ```python # example Manticore script from manticore.native import Manticore -hook_pc = 0x400ca0 +m = Manticore.linux('./example') -m = Manticore.linux('./path/to/binary') - -@m.hook(hook_pc) +@m.hook(0x400ca0) def hook(state): cpu = state.cpu print('eax', cpu.EAX) @@ -103,9 +169,15 @@ def hook(state): m.run() ``` +
+ -Manticore can also evaluate WebAssembly functions over symbolic inputs. +#### WASM +Manticore can also evaluate WebAssembly functions over symbolic inputs for property validation or general analysis. +
+ Click to expand: + ```python from manticore.wasm import ManticoreWASM @@ -129,147 +201,48 @@ m.collatz(arg_gen) for idx, val_list in enumerate(m.collect_returns()): print("State", idx, "::", val_list[0]) ``` +
## Requirements +* Manticore requires Python 3.6 or greater +* Manticore officially supports the latest LTS version of Ubuntu provided by Github Actions + * Manticore has experimental support for EVM and WASM (but not native Linux binaries) on MacOS +* We recommend running with increased stack size. This can be done by running `ulimit -s 100000` or by passing `--ulimit stack=100000000:100000000` to `docker run` -* Manticore is supported on Linux and requires **Python 3.6+**. -* Ubuntu 18.04 is strongly recommended. +### Compiling Smart Contracts * Ethereum smart contract analysis requires the [`solc`](https://github.com/ethereum/solidity) program in your `$PATH`. -* Increased stack size is recommended; this can be done by `ulimit -s 100000` or by passing `--ulimit stack=100000000:100000000` to `docker run` if docker is used. - -## Quickstart - -Install and try Manticore in a few shell commands: - -```bash -# Install system dependencies -sudo apt-get update && sudo apt-get install python3 python3-dev python3-pip -y - -# Install Manticore and its dependencies -sudo pip3 install manticore[native] - -# Download the examples -git clone https://github.com/trailofbits/manticore.git && cd manticore/examples/linux - -# Build the examples -make - -# Use the Manticore CLI -manticore basic -cat mcore_*/*0.stdin | ./basic -cat mcore_*/*1.stdin | ./basic - -# Use the Manticore API -cd ../script -python3 count_instructions.py ../linux/helloworld -``` - -You can also use Docker to quickly install and try Manticore: - -```bash -# Run container with a shared examples/ directory -# Note that `--rm` will make the container be deleted if you exit it -# (if you want to persist data from the container, use docker volumes) -# (we need to increase maximum stack size, so we use ulimit for that) -$ docker run --rm -it --ulimit stack=100000000:100000000 trailofbits/manticore bash - -# Change to examples directory -manticore@8d456f662d0f:~$ cd manticore/examples/linux/ - -# Build the examples -manticore@8d456f662d0f:~/manticore/examples/linux$ make - -# Use the Manticore CLI -manticore@8d456f662d0f:~/manticore/examples/linux$ manticore basic - - -manticore@8d456f662d0f:~/manticore/examples/linux$ cat mcore_*/*0.stdin | ./basic -manticore@8d456f662d0f:~/manticore/examples/linux$ cat mcore_*/*1.stdin | ./basic - -# Use the Manticore API -manticore@8d456f662d0f:~/manticore/examples/linux$ cd ../script -manticore@8d456f662d0f:~/manticore/examples/script$ python3 count_instructions.py ../linux/helloworld -``` - -## Installation - - -> NOTE: For native binary analysis, Manticore requires additional dependencies that are not installed by default. To -install these also, substitute `manticore[native]` for `manticore` in any `pip` command. - - -Option 1: Perform a user install (requires `~/.local/bin` in your `PATH`). - -```bash -echo "PATH=\$PATH:~/.local/bin" >> ~/.profile -source ~/.profile -pip3 install --user manticore -``` - -Option 2: Use a virtual environment (requires [virtualenvwrapper](https://virtualenvwrapper.readthedocs.io/en/latest/) or [similar](https://virtualenv.pypa.io/en/stable/)). - -```bash -sudo pip3 install virtualenvwrapper -echo "source /usr/local/bin/virtualenvwrapper.sh" >> ~/.profile -source ~/.profile -mkvirtualenv manticore -sudo ./manticore/bin/pip3 install manticore -``` - -Option 3: Perform a system install. - -```bash -sudo pip3 install manticore -``` - -Option 4: Install via Docker. - -```bash -docker pull trailofbits/manticore -``` - -Once installed, the `manticore` CLI tool and Python API will be available. - -For installing a development version of Manticore, see our [wiki](https://github.com/trailofbits/manticore/wiki/Hacking-on-Manticore). - -If you use Mac OS X you may need to install dependencies manually: - -```bash -brew install capstone -export MACOS_UNIVERSAL=no && pip install capstone - -brew install unicorn -UNICORN_QEMU_FLAGS="--python=`whereis python`" pip install unicorn -``` - -### Solidity Versions -Note that we're still in the process of implementing full support for the EVM Constantinople instruction semantics, so certain opcodes may not be supported. -You may want to consider using a version of `solc` that's less likely to generate these opcodes (eg pre-0.5.0). +* Manticore uses [crytic-compile](https://github.com/crytic/crytic-compile) to build smart contracts. If you're having compilation issues, consider running +`crytic-compile` on your code directly to make it easier to identify any issues. +* We're still in the process of implementing full support for the EVM Istanbul instruction semantics, so certain opcodes may not be supported. +In a pinch, you can try compiling with Solidity 0.4.x to avoid generating those instructions. ## Getting Help Feel free to stop by our #manticore slack channel in [Empire Hacking](https://empireslacking.herokuapp.com/) for help using or extending Manticore. - Documentation is available in several places: - * The [wiki](https://github.com/trailofbits/manticore/wiki) contains some - basic information about getting started with Manticore and contributing + * The [wiki](https://github.com/trailofbits/manticore/wiki) contains information about getting started with Manticore and contributing + + * The [API reference](http://manticore.readthedocs.io/en/latest/) has more thorough and in-depth documentation on our API + + * The [examples](examples) directory has some small examples that showcase API features - * The [examples](examples) directory has some very minimal examples that - showcase API features + * The [manticore-examples](https://github.com/trailofbits/manticore-examples) repository has some more involved examples, including some real CTF problems - * The [API reference](http://manticore.readthedocs.io/en/latest/) has more - thorough and in-depth documentation on our API +If you'd like to file a bug report or feature request, please use our [issues](https://github.com/trailofbits/manticore/issues/choose) page. - * The [manticore-examples](https://github.com/trailofbits/manticore-examples) - repository has some more involved examples, for instance solving real CTF problems +For questions and clarifications, please visit the [discussion](https://github.com/trailofbits/manticore/discussions) page. ## License Manticore is licensed and distributed under the AGPLv3 license. [Contact us](mailto:opensource@trailofbits.com) if you're looking for an exception to the terms. -## Publication +## Publications - [Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts](https://arxiv.org/abs/1907.03890), Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, Artem Dinaburg - ASE 19 If you are using Manticore on an academic work, consider applying to the [Crytic $10k Research Prize](https://blog.trailofbits.com/2019/11/13/announcing-the-crytic-10k-research-prize/). + +## Demo Video from ASE 2019 +[![Brief Manticore demo video](https://img.youtube.com/vi/o6pmBJZpKAc/1.jpg)](https://youtu.be/o6pmBJZpKAc) + diff --git a/examples/README.md b/examples/README.md new file mode 100644 index 000000000..e5be467e1 --- /dev/null +++ b/examples/README.md @@ -0,0 +1,56 @@ +# Manticore Examples + +## Quickstart + +Install and try Manticore in a few shell commands: + +```bash +# (Recommended) Create a virtual environment for Manticore +virtualenv -p `which python3` mcenv +source mcenv/bin/activate + +# Install Manticore and its dependencies +pip install manticore[native] + +# Download the examples +git clone https://github.com/trailofbits/manticore.git && cd manticore/examples/linux + +# Build the examples +make + +# Use the Manticore CLI +manticore basic +cat mcore_*/*0.stdin | ./basic +cat mcore_*/*1.stdin | ./basic + +# Use the Manticore API +cd ../script +python count_instructions.py ../linux/helloworld +``` + +You can also use Docker to quickly install and try Manticore: + +```bash +# Run container with a shared examples/ directory +# Note that `--rm` will make the container be deleted if you exit it +# (if you want to persist data from the container, use docker volumes) +# (we need to increase maximum stack size, so we use ulimit for that) +$ docker run --rm -it --ulimit stack=100000000:100000000 trailofbits/manticore bash + +# Change to examples directory +manticore@8d456f662d0f:~$ cd manticore/examples/linux/ + +# Build the examples +manticore@8d456f662d0f:~/manticore/examples/linux$ make + +# Use the Manticore CLI +manticore@8d456f662d0f:~/manticore/examples/linux$ manticore basic + + +manticore@8d456f662d0f:~/manticore/examples/linux$ cat mcore_*/*0.stdin | ./basic +manticore@8d456f662d0f:~/manticore/examples/linux$ cat mcore_*/*1.stdin | ./basic + +# Use the Manticore API +manticore@8d456f662d0f:~/manticore/examples/linux$ cd ../script +manticore@8d456f662d0f:~/manticore/examples/script$ python3 count_instructions.py ../linux/helloworld +``` \ No newline at end of file diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py index 5273abfa8..e73dab405 100644 --- a/manticore/core/manticore.py +++ b/manticore/core/manticore.py @@ -79,17 +79,65 @@ def to_class(self): class ManticoreBase(Eventful): - def __new__(cls, *args, **kwargs): - if cls in (ManticoreBase, ManticoreSingle, ManticoreThreading, ManticoreMultiprocessing): - raise ManticoreError("Should not instantiate this") + def _manticore_single(self): + self._worker_type = WorkerSingle - cl = consts.mprocessing.to_class() - # change ManticoreBase for the more specific class - bases = {cl if issubclass(base, ManticoreBase) else base for base in cls.__bases__} - cls.__bases__ = tuple(bases) + class FakeLock: + def _nothing(self, *args, **kwargs): + pass - random.seed(consts.seed) - return super().__new__(cls) + acquire = _nothing + release = _nothing + __enter__ = _nothing + __exit__ = _nothing + notify_all = _nothing + wait = _nothing + + def wait_for(self, condition, *args, **kwargs): + if not condition(): + raise Exception("Deadlock: Waiting for CTRL+C") + + self._lock = FakeLock() + self._killed = ctypes.c_bool(False) + self._running = ctypes.c_bool(False) + self._ready_states = [] + self._terminated_states = [] + self._busy_states = [] + self._killed_states = [] + self._shared_context = {} + + def _manticore_threading(self): + self._worker_type = WorkerThread + self._lock = threading.Condition() + self._killed = ctypes.c_bool(False) + self._running = ctypes.c_bool(False) + self._ready_states = [] + self._terminated_states = [] + self._busy_states = [] + self._killed_states = [] + self._shared_context = {} + + def _manticore_multiprocessing(self): + def raise_signal(): + signal.signal(signal.SIGINT, signal.SIG_IGN) + + self._worker_type = WorkerProcess + # This is the global manager that will handle all shared memory access + # See. https://docs.python.org/3/library/multiprocessing.html#multiprocessing.managers.SyncManager + self._manager = SyncManager() + self._manager.start(raise_signal) + # The main manticore lock. Acquire this for accessing shared objects + # THINKME: we use the same lock to access states lists and shared contexts + self._lock = self._manager.Condition() + self._killed = self._manager.Value(bool, False) + self._running = self._manager.Value(bool, False) + # List of state ids of States on storage + self._ready_states = self._manager.list() + self._terminated_states = self._manager.list() + self._busy_states = self._manager.list() + self._killed_states = self._manager.list() + self._shared_context = self._manager.dict() + self._context_value_types = {list: self._manager.list, dict: self._manager.dict} # Decorators added first for convenience. def sync(func: Callable) -> Callable: # type: ignore @@ -255,6 +303,12 @@ def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kw :param kwargs: other kwargs, e.g. """ super().__init__() + random.seed(consts.seed) + { + consts.mprocessing.single: self._manticore_single, + consts.mprocessing.threading: self._manticore_threading, + consts.mprocessing.multiprocessing: self._manticore_multiprocessing, + }[consts.mprocessing]() if any( not hasattr(self, x) @@ -812,7 +866,6 @@ def context(self): return self._shared_context @contextmanager - @sync def locked_context(self, key=None, value_type=list): """ A context manager that provides safe parallel access to the global @@ -843,19 +896,20 @@ def locked_context(self, key=None, value_type=list): :type value_type: list or dict or set """ - if key is None: - # If no key is provided we yield the raw shared context under a lock - yield self._shared_context - else: - # if a key is provided we yield the specific value or a fresh one - if value_type not in (list, dict): - raise TypeError("Type must be list or dict") - if hasattr(self, "_context_value_types"): - value_type = self._context_value_types[value_type] - context = self._shared_context - if key not in context: - context[key] = value_type() - yield context[key] + with self._lock: + if key is None: + # If no key is provided we yield the raw shared context under a lock + yield self._shared_context + else: + # if a key is provided we yield the specific value or a fresh one + if value_type not in (list, dict): + raise TypeError("Type must be list or dict") + if hasattr(self, "_context_value_types"): + value_type = self._context_value_types[value_type] + context = self._shared_context + if key not in context: + context[key] = value_type() + yield context[key] ############################################################################ # Public API @@ -1008,82 +1062,3 @@ def save_run_data(self): config.save(f) logger.info("Results in %s", self._output.store.uri) - - -class ManticoreSingle(ManticoreBase): - _worker_type = WorkerSingle - - def __init__(self, *args, **kwargs): - class FakeLock: - def _nothing(self, *args, **kwargs): - pass - - acquire = _nothing - release = _nothing - __enter__ = _nothing - __exit__ = _nothing - notify_all = _nothing - wait = _nothing - - def wait_for(self, condition, *args, **kwargs): - if not condition(): - raise Exception("Deadlock: Waiting for CTRL+C") - - self._lock = FakeLock() - self._killed = ctypes.c_bool(False) - self._running = ctypes.c_bool(False) - - self._ready_states = [] - self._terminated_states = [] - self._busy_states = [] - self._killed_states = [] - - self._shared_context = {} - super().__init__(*args, **kwargs) - - -class ManticoreThreading(ManticoreBase): - _worker_type = WorkerThread - - def __init__(self, *args, **kwargs): - self._lock = threading.Condition() - self._killed = ctypes.c_bool(False) - self._running = ctypes.c_bool(False) - - self._ready_states = [] - self._terminated_states = [] - self._busy_states = [] - self._killed_states = [] - - self._shared_context = {} - - super().__init__(*args, **kwargs) - - -def raise_signal(): - signal.signal(signal.SIGINT, signal.SIG_IGN) - - -class ManticoreMultiprocessing(ManticoreBase): - _worker_type = WorkerProcess - - def __init__(self, *args, **kwargs): - # This is the global manager that will handle all shared memory access - # See. https://docs.python.org/3/library/multiprocessing.html#multiprocessing.managers.SyncManager - self._manager = SyncManager() - self._manager.start(raise_signal) - # The main manticore lock. Acquire this for accessing shared objects - # THINKME: we use the same lock to access states lists and shared contexts - self._lock = self._manager.Condition() - self._killed = self._manager.Value(bool, False) - self._running = self._manager.Value(bool, False) - - # List of state ids of States on storage - self._ready_states = self._manager.list() - self._terminated_states = self._manager.list() - self._busy_states = self._manager.list() - self._killed_states = self._manager.list() - self._shared_context = self._manager.dict() - self._context_value_types = {list: self._manager.list, dict: self._manager.dict} - - super().__init__(*args, **kwargs) diff --git a/manticore/core/plugin.py b/manticore/core/plugin.py index 18e780ee3..46771c6b3 100644 --- a/manticore/core/plugin.py +++ b/manticore/core/plugin.py @@ -3,6 +3,7 @@ import cProfile import pstats import threading +from functools import wraps from .smtlib import issymbolic @@ -10,8 +11,43 @@ class Plugin: + def __init__(self): self.manticore = None + self._enabled_key = f"{str(type(self))}_enabled_{hash(self)}" + self._plugin_context_name = f"{str(type(self))}_context_{hash(self)}" + self.__decorate_callbacks() + + def __decorate_callbacks(self): + for attr in self.__dict__: + if attr.endswith('_callback'): + method = getattr(self, attr) + if callable(method): + setattr(self, attr, self._if_enabled(method)) + + def enable(self): + """ Enable all callbacks """ + with self.manticore.locked_context() as context: + context[self._enabled_key] = True + + def disable(self): + """ Disable all callbacks """ + with self.manticore.locked_context() as context: + context[self._enabled_key] = False + + def is_enabled(self): + """ True if callbacks are enabled """ + with self.manticore.locked_context() as context: + return context.get(self._enabled_key, True) + + @staticmethod + def _if_enabled(f): + """ decorator used to guard callbacks """ + @wraps(f) + def g(self, *args, **kwargs): + if self.is_enabled(): + return f(self, *args, **kwargs) + return g @property def name(self): @@ -25,7 +61,7 @@ def locked_context(self, key=None, value_type=list): when parallel analysis is activated. Code within the `with` block is executed atomically, so access of shared variables should occur within. """ - plugin_context_name = str(type(self)) + plugin_context_name = self._plugin_context_name with self.manticore.locked_context(plugin_context_name, dict) as context: if key is None: yield context @@ -37,7 +73,7 @@ def locked_context(self, key=None, value_type=list): @property def context(self): """ Convenient access to shared context """ - plugin_context_name = str(type(self)) + plugin_context_name = self._plugin_context_name if plugin_context_name not in self.manticore.context: self.manticore.context[plugin_context_name] = {} return self.manticore.context[plugin_context_name] diff --git a/manticore/core/smtlib/constraints.py b/manticore/core/smtlib/constraints.py index 3ed4d6f79..36aff2f5f 100644 --- a/manticore/core/smtlib/constraints.py +++ b/manticore/core/smtlib/constraints.py @@ -17,10 +17,16 @@ Constant, ) from .visitors import GetDeclarations, TranslatorSmtlib, get_variables, simplify, replace +from ...utils import config import logging logger = logging.getLogger(__name__) +consts = config.get_group("smt") +consts.add( + "related_constraints", default=False, description="Try slicing the current path constraint to contain only related items" +) + class ConstraintException(SmtlibError): """ @@ -56,6 +62,9 @@ def __reduce__(self): }, ) + def __hash__(self): + return hash(self.constraints) + def __enter__(self) -> "ConstraintSet": assert self._child is None self._child = self.__class__() @@ -96,7 +105,6 @@ def add(self, constraint) -> None: self._constraints = [constraint] else: return - self._constraints.append(constraint) def _get_sid(self) -> int: @@ -118,7 +126,8 @@ def __get_related(self, related_to=None): # satisfiable one, {}. # In light of the above, the core __get_related logic is currently disabled. # if related_to is not None: - if False: + # feliam: This assumes the previous constraints are already SAT (normal SE forking) + if consts.related_constraints and related_to is not None: number_of_constraints = len(self.constraints) remaining_constraints = set(self.constraints) related_variables = get_variables(related_to) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 7f393e064..708e6dcee 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -18,6 +18,7 @@ import collections import shlex import time +from functools import lru_cache from typing import Dict, Tuple from subprocess import PIPE, Popen import re @@ -421,6 +422,7 @@ def _pop(self): """Recall the last pushed constraint store and state.""" self._send("(pop 1)") + @lru_cache(maxsize=32) def can_be_true(self, constraints: ConstraintSet, expression: Union[bool, Bool] = True) -> bool: """Check if two potentially symbolic values can be equal""" if isinstance(expression, bool): @@ -438,6 +440,7 @@ def can_be_true(self, constraints: ConstraintSet, expression: Union[bool, Bool] return self._is_sat() # get-all-values min max minmax + @lru_cache(maxsize=32) def get_all_values(self, constraints, expression, maxcnt=None, silent=False): """Returns a list with all the possible values for the symbol x""" if not isinstance(expression, Expression): diff --git a/manticore/core/worker.py b/manticore/core/worker.py index fa0281e9c..f2e2ac0e5 100644 --- a/manticore/core/worker.py +++ b/manticore/core/worker.py @@ -132,7 +132,7 @@ def run(self, *args): assert current_state is None # Handling Forking and terminating exceptions except Concretize as exc: - logger.info("[%r] Performing %r", self.id, exc.message) + logger.debug("[%r] Performing %r", self.id, exc.message) # The fork() method can decides which state to keep # exploring. For example when the fork results in a # single state it is better to just keep going. diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index f2e71f91e..e5a2d9670 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -871,10 +871,10 @@ def _transaction(self, sort, caller, value=0, address=None, data=None, gas=21000 caller = int(caller) # Defaults, call data is empty if data is None: - data = bytearray(b"") - if isinstance(data, (str, bytes)): - data = bytearray(data) - if not isinstance(data, (bytearray, Array)): + data = b"" + if isinstance(data, str): + data = bytes(data) + if not isinstance(data, (bytes, Array)): raise TypeError("code bad type") # Check types @@ -1184,12 +1184,13 @@ def _on_unsound_symbolication(self, state, func, data, result): if value is not None: with self.locked_context("ethereum", dict) as ethereum_context: global_known_pairs = ethereum_context.get(f"symbolic_func_conc_{name}", set()) - global_known_pairs.add((data, value)) - ethereum_context[f"symbolic_func_conc_{name}"] = global_known_pairs + if (data, value) not in global_known_pairs: + global_known_pairs.add((data, value)) + ethereum_context[f"symbolic_func_conc_{name}"] = global_known_pairs + logger.info(f"Found a concrete {name} {data} -> {value}") concrete_pairs = state.context.get(f"symbolic_func_conc_{name}", set()) concrete_pairs.add((data, value)) state.context[f"symbolic_func_conc_{name}"] = concrete_pairs - logger.info(f"Found a concrete {name} {data} -> {value}") else: # we can not calculate the concrete value lets use a fresh symbol with self.locked_context("ethereum", dict) as ethereum_context: @@ -1425,16 +1426,13 @@ def _terminate_state_callback(self, state, e): # generate a testcase. FIXME This should be configurable as REVERT and # THROW; it actually changes the balance and nonce? of some accounts - if tx.result in {"SELFDESTRUCT", "REVERT", "THROW", "TXERROR"}: + if tx.return_value == 0: pass - elif tx.result in {"RETURN", "STOP"}: + else: # if not a revert, we save the state for further transactions with self.locked_context("ethereum.saved_states", list) as saved_states: saved_states.append(state.id) - else: - logger.debug("Exception in state. Discarding it") - # Callbacks def _did_evm_execute_instruction_callback(self, state, instruction, arguments, result): """ INTERNAL USE """ diff --git a/manticore/ethereum/plugins.py b/manticore/ethereum/plugins.py index 5353c52a7..acabd1a77 100644 --- a/manticore/ethereum/plugins.py +++ b/manticore/ethereum/plugins.py @@ -1,7 +1,6 @@ import sys from functools import reduce - import re from ..core.plugin import Plugin diff --git a/manticore/native/cpu/abstractcpu.py b/manticore/native/cpu/abstractcpu.py index 7b57bc2d2..2a41e88dd 100644 --- a/manticore/native/cpu/abstractcpu.py +++ b/manticore/native/cpu/abstractcpu.py @@ -89,7 +89,9 @@ class ConcretizeRegister(CpuException): Raised when a symbolic register needs to be concretized. """ - def __init__(self, cpu, reg_name, message=None, policy="MINMAX"): + def __init__( + self, cpu: "Cpu", reg_name: str, message: Optional[str] = None, policy: str = "MINMAX", + ): self.message = message if message else f"Concretizing {reg_name}" self.cpu = cpu diff --git a/manticore/native/memory.py b/manticore/native/memory.py index 167e0fe64..3e5ecdc8b 100644 --- a/manticore/native/memory.py +++ b/manticore/native/memory.py @@ -11,6 +11,7 @@ BitVecConstant, expression, issymbolic, + Expression, ) from ..native.mappings import mmap, munmap from ..utils.helpers import interval_intersection @@ -19,7 +20,7 @@ import functools import logging -from typing import Dict, Generator, Iterable, List, MutableMapping, Optional, Set +from typing import Dict, Generator, Iterable, List, MutableMapping, Optional, Set, Union logger = logging.getLogger(__name__) @@ -58,7 +59,14 @@ class ConcretizeMemory(MemoryException): Raised when a symbolic memory cell needs to be concretized. """ - def __init__(self, mem, address, size, message=None, policy="MINMAX"): + def __init__( + self, + mem: "Memory", + address: Union[int, Expression], + size: int, + message: Optional[str] = None, + policy: str = "MINMAX", + ): if message is None: self.message = f"Concretizing memory address {address} size {size}" else: diff --git a/manticore/native/state.py b/manticore/native/state.py index b3530d0e8..da0f6930b 100644 --- a/manticore/native/state.py +++ b/manticore/native/state.py @@ -1,7 +1,15 @@ +from collections import namedtuple +from typing import Any, NamedTuple + from ..core.state import StateBase, Concretize, TerminateState from ..native.memory import ConcretizeMemory, MemoryException +class CheckpointData(NamedTuple): + pc: Any + last_pc: Any + + class State(StateBase): @property def cpu(self): @@ -17,6 +25,14 @@ def mem(self): """ return self._platform.current.memory + def _rollback(self, checkpoint_data: CheckpointData) -> None: + """ + Rollback state to previous values in checkpoint_data + """ + # Keep in this form to make sure we don't miss restoring any newly added + # data. Make sure the order is correct + self.cpu.PC, self.cpu._last_pc = checkpoint_data + def execute(self): """ Perform a single step on the current state @@ -25,28 +41,36 @@ def execute(self): ConcretizeRegister, ) # must be here, otherwise we get circular imports + checkpoint_data = CheckpointData(pc=self.cpu.PC, last_pc=self.cpu._last_pc) try: result = self._platform.execute() # Instead of State importing SymbolicRegisterException and SymbolicMemoryException # from cpu/memory shouldn't we import Concretize from linux, cpu, memory ?? # We are forcing State to have abstractcpu - except ConcretizeRegister as e: + except ConcretizeRegister as exc: + # Need to define local variable to use in closure + e = exc expression = self.cpu.read_register(e.reg_name) - def setstate(state, value): - state.cpu.write_register(setstate.e.reg_name, value) + def setstate(state: State, value): + state.cpu.write_register(e.reg_name, value) - setstate.e = e + self._rollback(checkpoint_data) raise Concretize(str(e), expression=expression, setstate=setstate, policy=e.policy) - except ConcretizeMemory as e: + except ConcretizeMemory as exc: + # Need to define local variable to use in closure + e = exc expression = self.cpu.read_int(e.address, e.size) - def setstate(state, value): - state.cpu.write_int(setstate.e.address, value, setstate.e.size) + def setstate(state: State, value): + state.cpu.write_int(e.address, value, e.size) - setstate.e = e + self._rollback(checkpoint_data) raise Concretize(str(e), expression=expression, setstate=setstate, policy=e.policy) + except Concretize as e: + self._rollback(checkpoint_data) + raise e except MemoryException as e: raise TerminateState(str(e), testcase=True) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 6a2652a4a..34472aa34 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -2416,7 +2416,7 @@ def _open_transaction(self, sort, address, price, bytecode_or_data, caller, valu ) if sort == "CREATE": bytecode = bytecode_or_data - data = bytearray() + data = bytes() else: bytecode = self.get_code(address) data = bytecode_or_data @@ -2790,7 +2790,6 @@ def calculate_new_address(sender=None, nonce=None): return new_address def execute(self): - self._process_pending_transaction() if self.current_vm is None: raise TerminateState("Trying to execute an empty transaction", testcase=False) diff --git a/manticore/platforms/linux.py b/manticore/platforms/linux.py index af3b8c9fc..c4f746d70 100644 --- a/manticore/platforms/linux.py +++ b/manticore/platforms/linux.py @@ -1850,7 +1850,9 @@ def _sys_open_get_file(self, filename: str, flags: int) -> FdLike: elif filename == "/proc/self/maps": return ProcSelfMaps(flags, self) else: - raise EnvironmentError("/proc/self is largely unsupported") + raise EnvironmentError( + f"Trying to read from {filename}.\nThe /proc/self filesystem is largely unsupported." + ) if os.path.isdir(filename): return Directory(filename, flags) diff --git a/manticore/platforms/platform.py b/manticore/platforms/platform.py index dc95090a7..d54ca4d30 100644 --- a/manticore/platforms/platform.py +++ b/manticore/platforms/platform.py @@ -43,14 +43,6 @@ def __init__(self, idx, name): super().__init__(msg) -class ConcretizeSyscallArgument(OSException): - def __init__(self, reg_num, message="Concretizing syscall argument", policy="SAMPLED"): - self.reg_num = reg_num - self.message = message - self.policy = policy - super().__init__(message) - - class Platform(Eventful): """ Base class for all platforms e.g. operating systems or virtual machines. diff --git a/manticore/utils/log.py b/manticore/utils/log.py index f61c4f275..f49595f0a 100644 --- a/manticore/utils/log.py +++ b/manticore/utils/log.py @@ -104,7 +104,6 @@ def get_levels() -> List[List[Tuple[str, int]]]: ("manticore.core.plugin", logging.DEBUG), ("manticore.wasm.*", logging.INFO), ("manticore.utils.emulate", logging.INFO), - ("manticore.utils.helpers", logging.INFO), ], # 3 (-vv) [("manticore.native.cpu.*", logging.DEBUG), ("manticore.wasm.*", logging.DEBUG)], @@ -113,6 +112,7 @@ def get_levels() -> List[List[Tuple[str, int]]]: ("manticore.native.memory", logging.DEBUG), ("manticore.native.cpu.*", logging.DEBUG), ("manticore.native.cpu.*.registers", logging.DEBUG), + ("manticore.utils.helpers", logging.INFO), ], # 5 (-vvvv) [ diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index f77c5a58a..ae04a9908 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -1686,6 +1686,23 @@ def test_gas_check(self): result = str(e) self.assertEqual(result, "SELFDESTRUCT") + def test_selfdestruct(self): + with disposable_mevm() as m: + asm_acc = """ PUSH1 0x0 + SELFDESTRUCT + """ + m.create_account( + address=0x111111111111111111111111111111111111111, code=EVMAsm.assemble(asm_acc) + ) + m.create_account(address=0x222222222222222222222222222222222222222) + symbolic_data = m.make_symbolic_buffer(320) + m.transaction( + caller=0x222222222222222222222222222222222222222, + address=0x111111111111111111111111111111111111111, + data=symbolic_data, + value=0, + ) + self.assertEqual(m.count_ready_states(), 1) class EthPluginTests(unittest.TestCase): def test_FilterFunctions_fallback_function_matching(self): diff --git a/tests/native/binaries/symbolic_read_count b/tests/native/binaries/symbolic_read_count new file mode 100755 index 000000000..08eb77de5 Binary files /dev/null and b/tests/native/binaries/symbolic_read_count differ diff --git a/tests/native/binaries/symbolic_read_count.c b/tests/native/binaries/symbolic_read_count.c new file mode 100644 index 000000000..50a00b220 --- /dev/null +++ b/tests/native/binaries/symbolic_read_count.c @@ -0,0 +1,26 @@ +// Compiled on Ubuntu 18.04 Manticore Docker image with +// gcc -static symbolic_read_count.c -o symbolic_read_count + +#include +#include + +int main(int argc, char **argv) { + // Need at least one argument + if (argc != 2) { + return -1; + } + + // Just get the char ordinal value + unsigned int count = argv[1][0]; + if (count > 9) { + return 0; + } + + // Yes... this is very unsafe + char *buf[10]; + int sz = read(0, buf, count); + if (sz > 0) { + printf("WIN: Read more than zero data\n"); + } + return sz; +} diff --git a/tests/native/test_syscalls.py b/tests/native/test_syscalls.py index 6919860f4..d5e96091a 100644 --- a/tests/native/test_syscalls.py +++ b/tests/native/test_syscalls.py @@ -9,12 +9,36 @@ import os import errno import re +from glob import glob + +from manticore.native import Manticore from manticore.platforms import linux, linux_syscall_stubs from manticore.platforms.linux import SymbolicSocket from manticore.platforms.platform import SyscallNotImplemented, logger as platform_logger +def test_symbolic_syscall_arg() -> None: + BIN_PATH = os.path.join(os.path.dirname(__file__), "binaries", "symbolic_read_count") + tmp_dir = tempfile.TemporaryDirectory(prefix="mcore_test_") + m = Manticore(BIN_PATH, argv=["+"], workspace_url=str(tmp_dir.name)) + + m.run() + m.finalize() + + found_win_msg = False + win_msg = "WIN: Read more than zero data" + outs_glob = f"{str(m.workspace)}/test_*.stdout" + # Search all output messages + for output_p in glob(outs_glob): + with open(output_p) as f: + if win_msg in f.read(): + found_win_msg = True + break + + assert found_win_msg, f'Did not find win message in {outs_glob}: "{win_msg}"' + + class LinuxTest(unittest.TestCase): _multiprocess_can_split_ = True BIN_PATH = os.path.join(os.path.dirname(__file__), "binaries", "basic_linux_amd64") diff --git a/tests/other/test_locking.py b/tests/other/test_locking.py new file mode 100644 index 000000000..d6c2037f8 --- /dev/null +++ b/tests/other/test_locking.py @@ -0,0 +1,20 @@ +import unittest +from manticore.native import Manticore +from pathlib import Path + + +ms_file = str( + Path(__file__).parent.parent.parent.joinpath("examples", "linux", "binaries", "multiple-styles") +) + + +class TestResume(unittest.TestCase): + def test_resume(self): + m = Manticore(ms_file, stdin_size=17) + + with m.locked_context() as ctx: + self.assertNotIn("unlocked", str(m._lock)) + + +if __name__ == "__main__": + unittest.main()