From bf79b805abcb399980fcaf5d1c9ed959a9843db9 Mon Sep 17 00:00:00 2001 From: Eric Hennenfent Date: Fri, 15 May 2020 11:28:01 -0700 Subject: [PATCH] Update README, Add Issue Templates (#1685) * Add canned issue templates * Fix URL params * Update the README * Add CLA * Update Youtube URL * Remove sudo from example readme * Reword dependencies in main readme * Replace mkvirtualenv with default version --- .../bug_report.md} | 20 +- .github/ISSUE_TEMPLATE/config.yml | 14 + .github/ISSUE_TEMPLATE/feature_request.md | 20 ++ CONTRIBUTING.md | 6 +- README.md | 265 ++++++++---------- examples/README.md | 56 ++++ 6 files changed, 227 insertions(+), 154 deletions(-) rename .github/{ISSUE_TEMPLATE.md => ISSUE_TEMPLATE/bug_report.md} (75%) create mode 100644 .github/ISSUE_TEMPLATE/config.yml create mode 100644 .github/ISSUE_TEMPLATE/feature_request.md create mode 100644 examples/README.md 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