Merge branch 'master' into capstone-5-dev

* master: (35 commits) Switch to stable Black (#2536) Fix typo in Manticore.linux constructor docstring (#2535) Revert CI changes made in #2526 Release Manticore 0.3.7 (#2526) Optimise forking when there is only 1 solution (#2527) Epoll Implementation (#2529) Split off ENDBR32/64 from CHESS branch (#2533) Update to crytic-compile 0.2.2 (#2530) Also ignore missing unicorn registers in the fallback emulator (#2531) x86 FXSAVE & FXRSTOR support (#2511) Fix `BitVecExtract` simplification for constant folding (#2524) Add pip-audit action workflow (#2513) Add EXPLICIT fork policy (#2514) Enforce crytic-compile==0.2.1 (#2512) Improve namedtuple definition (#2506) Add SMT simplifications for bitvec subtraction (#2504) Fix handling of the program base address in Linux (#2500) Bump Sphinx version to 4.3.0 (#2503) Solver Improvements (#2502) Improves `namedtuple` definition (#2501) ...
trailofbits · Mar 3, 2022 · 7589f48 · 7589f48
2 parents f3b9234 + 904f336
commit 7589f48
Show file tree

Hide file tree

Showing 79 changed files with 1,802 additions and 642 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -15,10 +15,10 @@ jobs:
     runs-on: ubuntu-18.04
     steps:
     - uses: actions/checkout@v2
-    - name: Set up Python 3.6
-      uses: actions/setup-python@v1
+    - name: Set up Python 3.7
+      uses: actions/setup-python@v2
       with:
-        python-version: 3.6
+        python-version: 3.7
     - name: Lint
       if: github.event_name == 'pull_request'
       env:
@@ -45,28 +45,34 @@ jobs:
         type: ["ethereum_truffle", "ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "wasm", "wasm_sym", "other"]
     steps:
     - uses: actions/checkout@v1
-    - name: Set up Python 3.6
-      uses: actions/setup-python@v1
+    - name: Set up Python 3.7
+      uses: actions/setup-python@v2
       with:
-        python-version: 3.6
+        python-version: 3.7
     - name: Install NPM
       uses: actions/setup-node@v1
       with:
-        node-version: '13.x'
+        node-version: '16.x'
     - name: Install dependencies
       env:
         TEST_TYPE: ${{ matrix.type }}
       run: |
         #install utils
         pip install coveralls
         pip install -e ".[dev-noks]"
+        # Get version info
+        pip freeze
+        z3 --version
         #install cvc4
         sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
         sudo chmod +x /usr/bin/cvc4
+        cvc4 --version
         #install yices
-        sudo add-apt-repository ppa:sri-csl/formal-methods
-        sudo apt-get update
-        sudo apt-get install yices2
+        sudo wget -O yices.tar.gz https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz
+        sudo tar -xzf yices.tar.gz
+        cd yices-2.6.2
+        sudo ./install-yices
+        yices --version
         #install boolector
         mkdir -p /tmp/build
         cd /tmp/build
@@ -113,10 +119,10 @@ jobs:
     needs: tests
     steps:
     - uses: actions/checkout@v2
-    - name: Set up Python 3.6
-      uses: actions/setup-python@v1
+    - name: Set up Python 3.7
+      uses: actions/setup-python@v2
       with:
-        python-version: 3.6
+        python-version: 3.7
     - name: Build Dist
       run: |
         python3 -m pip install wheel

diff --git a/.github/workflows/osx.yml b/.github/workflows/osx.yml
@@ -14,10 +14,10 @@ jobs:
         type: ["ethereum_truffle", "ethereum_bench", "ethereum", "ethereum_vm", "wasm", "wasm_sym", "other"]
     steps:
     - uses: actions/checkout@v2
-    - name: Set up Python 3.6
-      uses: actions/setup-python@v1
+    - name: Set up Python 3.7
+      uses: actions/setup-python@v2
       with:
-        python-version: 3.6
+        python-version: 3.7
     - name: Install NPM
       uses: actions/setup-node@v1
       with:

diff --git a/.github/workflows/pip-audit.yml b/.github/workflows/pip-audit.yml
@@ -0,0 +1,27 @@
+name: pip-audit
+
+on:
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+  schedule: [ cron: "0 7 * * 2" ]
+
+jobs:
+  audit:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout repository
+      uses: actions/checkout@v2
+    - name: Set up Python 3.10
+      uses: actions/setup-python@v2
+      with:
+        python-version: "3.10"
+    - name: Install pip-audit
+      run: |
+        python -m pip install --upgrade pip
+        python -m pip install pip-audit
+    - name: Run pip-audit
+      run: |
+        python -m pip install .
+        pip-audit --strict --desc
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -12,10 +12,10 @@ jobs:
         type: ["ethereum_truffle", "ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "wasm", "wasm_sym", "other"]
     steps:
     - uses: actions/checkout@v1
-    - name: Set up Python 3.6
-      uses: actions/setup-python@v1
+    - name: Set up Python 3.7
+      uses: actions/setup-python@v2
       with:
-        python-version: 3.6
+        python-version: 3.7
     - name: Install NPM
       uses: actions/setup-node@v1
       with:
@@ -64,10 +64,10 @@ jobs:
     needs: tests
     steps:
     - uses: actions/checkout@v2
-    - name: Set up Python 3.6
-      uses: actions/setup-python@v1
+    - name: Set up Python 3.7
+      uses: actions/setup-python@v2
       with:
-        python-version: 3.6
+        python-version: 3.7
     - name: Build Dist
       run: |
         python3 -m pip install wheel

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,6 +1,36 @@
 # Change Log
 
-## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.6...HEAD)
+## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.7...HEAD)
+
+## 0.3.7 - 2022-02
+
+Thanks to our external contributors!
+ - [sobolevn](https://github.com/trailofbits/manticore/pulls?q=is%3Apr+author%3Asobolevn)
+ - [G-11-P](https://github.com/trailofbits/manticore/pulls?q=is%3Apr+author%3AG-11-P)
+
+### Ethereum
+* Use `crytic-compile` 0.2.2 [#2530](https://github.com/trailofbits/manticore/pull/2530)
+* Multi-transaction analysis now uses fixed attacker and owner contracts [#2464](https://github.com/trailofbits/manticore/pull/2464)
+
+### Native
+* **[Added API]** Retrieve list of unimplemented syscalls [#2491](https://github.com/trailofbits/manticore/pull/2491)
+* Add `FXSAVE`/`FXRSTOR` concrete support on x86 [#2511](https://github.com/trailofbits/manticore/pull/2511)
+* Add `last_executed_pc` property to CPU [#2475](https://github.com/trailofbits/manticore/pull/2475)
+* Support LD_LIBRARY_PATH [#2476](https://github.com/trailofbits/manticore/pull/2476)
+* Optional `will/did_read_memory` events [#2488](https://github.com/trailofbits/manticore/pull/2488) 
+* Fixed base address handling on Linux [#2500](https://github.com/trailofbits/manticore/pull/2500)
+* Add `ENDBR`-style NOPs [#2533](https://github.com/trailofbits/manticore/pull/2533)
+* Support `epoll`-related syscalls [#2529](https://github.com/trailofbits/manticore/pull/2529)
+
+### Other
+* **[Added API]** Add fork policy for providing explicit values [#2514](https://github.com/trailofbits/manticore/pull/2514)
+* Fixed Constant Folding [#2524](https://github.com/trailofbits/manticore/pull/2524)
+* Add simplifications for subtraction [#2504](https://github.com/trailofbits/manticore/pull/2504)
+* Parent state ID, last PC now available in state descriptors [#2479](https://github.com/trailofbits/manticore/pull/2479), [#2471](https://github.com/trailofbits/manticore/pull/2471)
+* States now contain a reference to the current manticore instance [#2486](https://github.com/trailofbits/manticore/pull/2486)
+* `fast_fail` config to exit after first state exception [#2487](https://github.com/trailofbits/manticore/pull/2487)
+* Scaling bugfix for large solver queries [#2502](https://github.com/trailofbits/manticore/pull/2502)
+* Don't fork when only one solution is found for `Concretize` [#2527](https://github.com/trailofbits/manticore/pull/2527)
 
 ## 0.3.6 - 2021-06-09
 

diff --git a/CITATION.cff b/CITATION.cff
@@ -0,0 +1,48 @@
+# YAML 1.2
+---
+abstract: "An effective way to maximize code coverage in software tests is through dynamic symbolic execution-a technique that uses constraint solving to systematically explore a program's state space. We introduce an open-source dynamic symbolic execution framework called Manticore for analyzing binaries and Ethereum smart contracts. Manticore's flexible architecture allows it to support both traditional and exotic execution environments, and its API allows users to customize their analysis. Here, we discuss Manticore's architecture and demonstrate the capabilities we have used to find bugs and verify the correctness of code for our commercial clients."
+authors: 
+  -
+    affiliation: "Trail of Bits"
+    family-names: Mossberg
+    given-names: Mark
+  -
+    affiliation: "Trail of Bits"
+    family-names: Manzano
+    given-names: Felipe
+  -
+    affiliation: "Trail of Bits"
+    family-names: Hennenfent
+    given-names: Eric
+  -
+    affiliation: "Trail of Bits"
+    family-names: Groce
+    given-names: Alex
+  -
+    affiliation: "Trail of Bits"
+    family-names: Greico
+    given-names: Gustavo
+  -
+    affiliation: "Trail of Bits"
+    family-names: Feist
+    given-names: Josselin
+  -
+    affiliation: "Trail of Bits"
+    family-names: Brunson
+    given-names: Trent
+  -
+    affiliation: "Trail of Bits"
+    family-names: Dinaburg
+    given-names: Artem
+cff-version: "1.1.0"
+date-released: 2019-11-11
+doi: "10.1109/ASE.2019.00133"
+keywords: 
+  - "symbolic execution"
+  - "binary analysis"
+  - ethereum
+license: "AGPL-3.0"
+message: "If you use this software in an academic work, please cite our paper."
+repository-code: "https://github.com/trailofbits/manticore"
+title: "Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts"
+...
diff --git a/Dockerfile b/Dockerfile
@@ -7,7 +7,7 @@ LABEL dockerfile_maintenance=trailofbits
 
 ENV LANG C.UTF-8
 
-RUN apt-get -y update && DEBIAN_FRONTEND=noninteractive apt-get -y install python3 python3-pip git wget
+RUN apt-get -y update && DEBIAN_FRONTEND=noninteractive apt-get -y install python3.7 python3.7-dev python3-pip git wget
 
 # Install solc 0.4.25 and validate it
 RUN wget https://github.com/ethereum/solidity/releases/download/v0.4.25/solc-static-linux \
@@ -17,9 +17,9 @@ RUN wget https://github.com/ethereum/solidity/releases/download/v0.4.25/solc-sta
 # If this fails, the solc-static-linux binary has changed while it should not.
 RUN [ "c9b268750506b88fe71371100050e9dd1e7edcf8f69da34d1cd09557ecb24580  /usr/bin/solc" = "$(sha256sum /usr/bin/solc)" ]
 
-RUN pip3 install -U pip
+RUN python3.7 -m pip install -U pip
 
 ADD . /manticore
-RUN cd manticore && pip3 install .[native]
+RUN cd manticore && python3.7 -m pip install .[native]
 
 CMD ["/bin/bash"]
diff --git a/README.md b/README.md
@@ -217,7 +217,7 @@ for idx, val_list in enumerate(m.collect_returns()):
 </details>
 
 ## Requirements
-* Manticore requires Python 3.6 or greater 
+* Manticore requires Python 3.7 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`

diff --git a/docs/conf.py b/docs/conf.py
@@ -25,7 +25,7 @@
 
 # If your documentation needs a minimal Sphinx version, state it here.
 #
-needs_sphinx = "1.0"
+needs_sphinx = "3.0"
 
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
@@ -54,9 +54,9 @@
 # built documents.
 #
 # The short X.Y version.
-version = "0.3.6"
+version = "0.3.7"
 # The full version, including alpha/beta/rc tags.
-release = "0.3.6"
+release = "0.3.7"
 
 # The language for content autogenerated by Sphinx. Refer to documentation
 # for a list of supported languages.

diff --git a/docs/requirements.txt b/docs/requirements.txt
@@ -0,0 +1 @@
+Sphinx==4.3.0
diff --git a/examples/evm/mappingchallenge.py b/examples/evm/mappingchallenge.py
@@ -27,7 +27,7 @@
 
 
 class StopAtDepth(Detector):
-    """ This just aborts explorations that are too deep """
+    """This just aborts explorations that are too deep"""
 
     def will_run_callback(self, *args):
         with self.manticore.locked_context("seen_rep", dict) as reps:

diff --git a/examples/script/concolic.py b/examples/script/concolic.py
@@ -29,7 +29,9 @@
 import copy
 from manticore.core.smtlib.expression import *
 
-prog = "../linux/simpleassert"
+from pathlib import Path
+
+prog = str(Path(__file__).parent.resolve().parent.joinpath("linux").joinpath("simpleassert"))
 VERBOSITY = 0
 
 
@@ -153,7 +155,7 @@ def constraints_to_constraintset(constupl):
 
 
 def input_from_cons(constupl, datas):
-    " solve bytes in |datas| based on "
+    "solve bytes in |datas| based on"
 
     def make_chr(c):
         try:

diff --git a/examples/wasm/if_check/solve.py b/examples/wasm/if_check/solve.py
@@ -3,15 +3,15 @@
 
 
 def getchar(state):
-    """ Symbolic `getchar` implementation. Returns an arbitrary single byte """
+    """Symbolic `getchar` implementation. Returns an arbitrary single byte"""
     res = state.new_symbolic_value(32, "getchar_res")
     state.constrain(0 < res)
     state.constrain(res < 256)
     return [res]
 
 
 class PrintRetPlugin(Plugin):
-    """ A plugin that looks for states that returned zero and solves for their inputs """
+    """A plugin that looks for states that returned zero and solves for their inputs"""
 
     def will_terminate_state_callback(self, state, *args):
         retval = state.stack.peek()

diff --git a/manticore/__init__.py b/manticore/__init__.py
@@ -1,7 +1,7 @@
 import sys
 
-if sys.version_info < (3, 6):
-    print("Manticore requires Python 3.6 or higher.")
+if sys.version_info < (3, 7):
+    print("Manticore requires Python 3.7 or higher.")
     sys.exit(-1)
 
 from .utils import config, log