Merge branch 'master' into chess

* master: Install pinned version of truffle to fix CI (#2467) Use fixed owner and attacker accounts in multi_tx_analysis (#2464) Manticore 0.3.6 (#2456) Fix IntrospectionAPIPlugin Name (#2459) Portfolio of parallel solvers (#2420) Replace Quick mode with Thorough mode (#2457) Fix incorrect comparison for symbolic file wildcards (#2454) Reduce the number of calls to the SMT solver in EVM (#2411) Fixes to Unicorn emulation - start/stop/resume (#1796) Add support for multiple compilation units (#2444) Basic solver stats (#2415)
trailofbits · Jul 15, 2021 · 98a87e3 · 98a87e3
2 parents 0fa906d + 378f8e8
commit 98a87e3
Show file tree

Hide file tree

Showing 26 changed files with 853 additions and 243 deletions.
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -0,0 +1,78 @@
+name: Upload to PyPI
+
+on:
+  release:
+    types: [published]
+
+jobs:
+  tests:
+    runs-on: ubuntu-18.04
+    strategy:
+      matrix:
+        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
+      with:
+        python-version: 3.6
+    - name: Install NPM
+      uses: actions/setup-node@v1
+      with:
+        node-version: '13.x'
+    - name: Install dependencies
+      env:
+        TEST_TYPE: ${{ matrix.type }}
+      run: |
+        #install utils
+        pip install coveralls
+        pip install -e ".[dev-noks]"
+        #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
+        #install yices
+        sudo add-apt-repository ppa:sri-csl/formal-methods
+        sudo apt-get update
+        sudo apt-get install yices2
+        #install boolector
+        mkdir -p /tmp/build
+        cd /tmp/build
+        git clone https://github.com/boolector/boolector.git
+        cd boolector
+        # Version 3.2.1
+        git checkout "f61c0dcf4a76e2f7766a6358bfb9c16ca8217224"
+        git log -1 --oneline > ../boolector.commit
+        ./contrib/setup-lingeling.sh
+        ./contrib/setup-btor2tools.sh
+        ./configure.sh
+        cd build
+        make -j4
+        mkdir -p /tmp/boolector
+        sudo make DESTDIR=/usr install
+        # Install solc unconditionally because it only takes a second or two
+        sudo wget -O /usr/bin/solc https://github.com/ethereum/solidity/releases/download/v0.4.24/solc-static-linux
+        sudo chmod +x /usr/bin/solc
+    - name: Run Tests
+      env:
+        TEST_TYPE: ${{ matrix.type }}
+      run: |
+        cp scripts/run_tests.sh .
+        ./run_tests.sh
+
+  upload:
+    runs-on: ubuntu-18.04
+    needs: tests
+    steps:
+    - uses: actions/checkout@v2
+    - name: Set up Python 3.6
+      uses: actions/setup-python@v1
+      with:
+        python-version: 3.6
+    - name: Build Dist
+      run: |
+        python3 -m pip install wheel
+        python3 setup.py sdist bdist_wheel
+    - name: Upload to PyPI
+      uses: pypa/[email protected]
+      with:
+        password: ${{ secrets.PYPI_UPLOAD }}
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,6 +1,30 @@
 # Change Log
 
-## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.5...HEAD)
+## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.6...HEAD)
+
+## 0.3.6 - 2021-06-09
+
+Thanks to our external contributors!
+ - [timgates42](https://github.com/trailofbits/manticore/commits?author=timgates42)
+
+### Ethereum
+* **[Changed API]** Default to quick mode: disable detectors and gas [#2457](https://github.com/trailofbits/manticore/pull/2457)
+* Allow symbolic balances from the beginning of execution [#1818](https://github.com/trailofbits/manticore/pull/1818)
+* Disable EVM Events in Testcases [#2417](https://github.com/trailofbits/manticore/pull/2417)
+
+### Native
+* **[Added API]** Syscall-specific hooks [#2389](https://github.com/trailofbits/manticore/pull/2389)
+* Fix wildcard behavior in symbolic files [#2454](https://github.com/trailofbits/manticore/pull/2454)
+* Bugfixes for control transfer between Manticore & Unicorn [#1796](https://github.com/trailofbits/manticore/pull/1796)
+
+### Other
+* Run multiple SMT solvers in parallel, take the fastest response [#2420](https://github.com/trailofbits/manticore/pull/2420)
+* Add socket for TUI [#1620](https://github.com/trailofbits/manticore/pull/1620)
+* Memory usage improvements in expression system [#2394](https://github.com/trailofbits/manticore/pull/2394)
+* Support for Boolector [#2410](https://github.com/trailofbits/manticore/pull/2410)
+* Solver Statistics API [#2415](https://github.com/trailofbits/manticore/pull/2415)
+* Allow duplicated config options [#2397](https://github.com/trailofbits/manticore/pull/2397)
+
 
 ## 0.3.5 - 2020-11-06
 

diff --git a/README.md b/README.md
@@ -46,10 +46,10 @@ Option 2: Installing from PyPI, with extra dependencies needed to execute native
 pip install "manticore[native]"
 ```
 
-Option 3: Installing a nightly development build (fill in the latest version from [the PyPI history](https://pypi.org/project/manticore/#history)):
+Option 3: Installing a nightly development build:
 
 ```bash
-pip install "manticore[native]==0.x.x.devYYMMDD"
+pip install --pre "manticore[native]"
 ```
 
 Option 4: Installing from the `master` branch:

diff --git a/docs/conf.py b/docs/conf.py
@@ -54,9 +54,9 @@
 # built documents.
 #
 # The short X.Y version.
-version = "0.3.5"
+version = "0.3.6"
 # The full version, including alpha/beta/rc tags.
-release = "0.3.5"
+release = "0.3.6"
 
 # The language for content autogenerated by Sphinx. Refer to documentation
 # for a list of supported languages.

diff --git a/examples/script/symbolic_file.py b/examples/script/symbolic_file.py
@@ -0,0 +1,77 @@
+#!/usr/bin/env python
+
+"""
+Example to show usage of introducing a file with symbolic contents
+
+This script should be the equivalent of:
+    $ echo "+++++++++++++" > symbolic_file.txt
+    $ manticore -v --file symbolic_file.txt ../linux/fileio symbolic_file.txt
+"""
+import copy
+import glob
+import os
+import pathlib
+import sys
+import tempfile
+
+from manticore.__main__ import main
+
+
+def test_symbolic_file(tmp_path):
+    # Run this file with Manticore
+    filepath = pathlib.Path(__file__).resolve().parent.parent / pathlib.Path("linux/fileio")
+    assert filepath.exists(), f"Please run the Makefile in {filepath.parent} to build {filepath}"
+
+    # Temporary workspace for Manticore
+    workspace_dir = tmp_path / "mcore_workspace"
+    workspace_dir.mkdir(parents=True, exist_ok=True)
+    assert (
+        len(os.listdir(workspace_dir)) == 0
+    ), f"Manticore workspace {workspace_dir} should be empty before running"
+
+    # Manticore will search for and read this partially symbolic file
+    sym_file_name = "symbolic_file.txt"
+    sym_file = tmp_path / sym_file_name
+    sym_file.write_text("+++++++++++++")
+
+    # Program arguments that would be passed to Manticore via CLI
+    manticore_args = [
+        # Show some progress
+        "-v",
+        # Register our symbolic file with Manticore
+        "--file",
+        str(sym_file),
+        # Setup workspace, for this test, or omit to use current directory
+        "--workspace",
+        str(workspace_dir),
+        # Manticore will execute our file here with arguments
+        str(filepath),
+        str(sym_file),
+    ]
+
+    # Bad hack to workaround passing the above arguments like we do on command
+    # line and have them parsed with argparse
+    backup_argv = copy.deepcopy(sys.argv[1:])
+    del sys.argv[1:]
+    sys.argv.extend(manticore_args)
+
+    # Call Manticore's main with our new argv list for argparse
+    main()
+
+    del sys.argv[1:]
+    sys.argv.extend(backup_argv)
+
+    # Manticore will write out the concretized contents of our symbolic file for
+    # each path in the program
+    all_concretized_sym_files = glob.glob(str(workspace_dir / f"*{sym_file_name}"))
+    assert (
+        len(all_concretized_sym_files) > 1
+    ), "Should have found more than 1 path through the program"
+    assert any(
+        map(lambda f: b"open sesame" in pathlib.Path(f).read_bytes(), all_concretized_sym_files)
+    ), "Could not find 'open sesame' in our concretized symbolic file"
+
+
+if __name__ == "__main__":
+    with tempfile.TemporaryDirectory() as workspace:
+        test_symbolic_file(pathlib.Path(workspace))
diff --git a/manticore/__main__.py b/manticore/__main__.py
@@ -230,10 +230,10 @@ def positive(value):
     )
 
     eth_flags.add_argument(
-        "--quick-mode",
+        "--thorough-mode",
         action="store_true",
-        help="Configure Manticore for quick exploration. Disable gas, generate testcase only for alive states, "
-        "do not explore constant functions. Disable all detectors.",
+        help="Configure Manticore for more exhaustive exploration. Evaluate gas, generate testcases for dead states, "
+        "explore constant functions, and run a small suite of detectors.",
     )
 
     config_flags = parser.add_argument_group("Constants")

diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py
@@ -14,7 +14,7 @@
 import shlex
 
 from ..core.plugin import Plugin, IntrospectionAPIPlugin, StateDescriptor
-from ..core.smtlib import Expression
+from ..core.smtlib import Expression, SOLVER_STATS
 from ..core.state import StateBase
 from ..core.workspace import ManticoreOutput
 from ..exceptions import ManticoreError
@@ -49,7 +49,11 @@
     default=False,
     description="If True enables to run workers over the network UNIMPLEMENTED",
 )
-consts.add("procs", default=10, description="Number of parallel processes to spawn")
+consts.add(
+    "procs",
+    default=12,
+    description="Number of parallel processes to spawn in order to run every task, including solvers",
+)
 
 proc_type = MProcessingType.threading
 if sys.platform != "linux":
@@ -380,8 +384,9 @@ def __init__(
             raise TypeError(f"Invalid initial_state type: {type(initial_state).__name__}")
         self._put_state(initial_state)
 
+        nworkers = max(consts.procs // initial_state._solver.ncores, 1)
         # Workers will use manticore __dict__ So lets spawn them last
-        self._workers = [self._worker_type(id=i, manticore=self) for i in range(consts.procs)]
+        self._workers = [self._worker_type(id=i, manticore=self) for i in range(nworkers)]
 
         # Create log capture worker. We won't create the rest of the daemons until .run() is called
         self._daemon_threads: typing.Dict[int, DaemonThread] = {
@@ -1106,6 +1111,10 @@ def run(self):
         """
         Runs analysis.
         """
+        # Start measuring the execution time
+        with self.locked_context() as context:
+            context["time_started"] = time.time()
+
         # Delete state cache
         # The cached version of a state may get out of sync if a worker in a
         # different process modifies the state
@@ -1219,7 +1228,28 @@ def save_run_data(self):
         with self._output.save_stream("manticore.yml") as f:
             config.save(f)
 
+        with self._output.save_stream("global.solver_stats") as f:
+            for s, n in sorted(SOLVER_STATS.items()):
+                f.write("%s: %d\n" % (s, n))
+
+        if SOLVER_STATS["timeout"] > 0 or SOLVER_STATS["unknown"] > 0:
+            logger.warning(
+                "The SMT solvers returned timeout or unknown for certain program paths. Results could not cover the entire set of possible paths"
+            )
+
         logger.info("Results in %s", self._output.store.uri)
+
+        time_ended = time.time()
+
+        with self.locked_context() as context:
+            if "time_started" in context:
+                time_elapsed = time_ended - context["time_started"]
+                logger.info("Total time: %s", time_elapsed)
+                context["time_ended"] = time_ended
+                context["time_elapsed"] = time_elapsed
+            else:
+                logger.warning("Manticore failed to run")
+
         self.wait_for_log_purge()
 
     def introspect(self) -> typing.Dict[int, StateDescriptor]:

diff --git a/manticore/core/plugin.py b/manticore/core/plugin.py
@@ -467,6 +467,10 @@ class IntrospectionAPIPlugin(Plugin):
 
     NAME = "introspector"
 
+    @property
+    def name(self) -> str:
+        return "IntrospectionAPIPlugin"
+
     def create_state(self, state_id: int):
         """
         Adds a StateDescriptor to the context in the READY state list