Merge branch 'master' into ekilmer-dev

* master: Create a model for strncpy (#1770) Add doc, fix output bugs (#1769) Update EVM usage example (#1772) New working model of strlen (#1725) Typo (#1768) Specialized iterative serialization for Array (#1756) Enable nightly uploads to PyPI (#1757) Manticore 0.3.4 (#1720) Manticore verifier (#1717) Nightly MacOS Tests (#1614) Remove/procrastinate solver query in ether leak detector (#1727) Fix constant folding & constraint set slicing (#1706)
trailofbits · Jul 17, 2020 · 2b8c280 · 2b8c280
2 parents ae2eec3 + 8a8f35c
commit 2b8c280
Show file tree

Hide file tree

Showing 44 changed files with 2,013 additions and 583 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -63,182 +63,34 @@ jobs:
       env:
         TEST_TYPE: ${{ matrix.type }}
       run: |
-        # Launches all examples; this assumes PWD is examples/script
-        launch_examples() {
-            COVERAGE_RCFILE=$GITHUB_WORKSPACE/.coveragerc
-            # concolic assumes presence of ../linux/simpleassert
-            echo "Running concolic.py..."
-            HW=../linux/helloworld
-            coverage run ./concolic.py
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            echo "Running count_instructions.py..."
-            coverage run ./count_instructions.py $HW |grep -q Executed
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            echo "Running introduce_symbolic_bytes.py..."
-            gcc -static -g src/state_explore.c -o state_explore
-            ADDRESS=0x$(objdump -S state_explore | grep -A 1 '((value & 0xff) != 0)' |
-                    tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:)
-            coverage run ./introduce_symbolic_bytes.py state_explore $ADDRESS
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            echo "Running run_simple.py..."
-            gcc -x c -static -o hello test_run_simple.c
-            coverage run ./run_simple.py hello
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            echo "Running run_hook.py..."
-            MAIN_ADDR=$(nm $HW|grep 'T main' | awk '{print "0x"$1}')
-            coverage run ./run_hook.py $HW $MAIN_ADDR
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            echo "Running state_control.py..."
-            # Straight from the header of state_control.py
-            gcc -static -g src/state_explore.c -o state_explore
-            SE_ADDR=0x$(objdump -S state_explore | grep -A 1 'value == 0x41' |
-                       tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:)
-            coverage run ./state_control.py state_explore $SE_ADDR
-            if [ $? -ne 0 ]; then
-                return 1
-            fi
-
-            return 0
-        }
-
-        make_vmtests(){
-            DIR=`pwd`
-            if  [ ! -f ethereum_vm/.done ]; then
-                echo "Automaking VMTests" `pwd`
-                cd ./tests/ && mkdir -p  ethereum_vm/VMTests_concrete && mkdir -p ethereum_vm/VMTests_symbolic
-                rm -Rf vmtests; git clone https://github.com/ethereum/tests --depth=1 vmtests
-                for i in ./vmtests/BlockchainTests/ValidBlocks/VMTests/*/*json; do python ./auto_generators/make_VMTests.py -f istanbul -i $i -o ethereum_vm/VMTests_concrete; done
-                rm ethereum_vm/VMTests_concrete/test_loop*.py #too slow
-                rm -rf ./vmtests
-                touch ethereum_vm/.done
-            fi
-            cd $DIR
-        }
-
-        make_wasm_tests(){
-            DIR=`pwd`
-            if  [ ! -f .wasm_done ]; then
-                echo "Automaking WASM Tests" `pwd`
-                cd ./tests/wasm
-                ./generate_tests.sh
-                touch .wasm_done
-            fi
-            cd $DIR
-        }
-
-        make_wasm_sym_tests(){
-            DIR=`pwd`
-            if  [ ! -f .wasm_sym_done ]; then
-                echo "Automaking Symbolic WASM Tests" `pwd`
-                cd ./tests/wasm_sym
-                ./generate_symbolic_tests.sh
-                touch .wasm_sym_done
-            fi
-            cd $DIR
-        }
-
-        install_truffle(){
-            npm install -g truffle
-        }
-
-        run_truffle_tests(){
-            COVERAGE_RCFILE=$GITHUB_WORKSPACE/.coveragerc
-            mkdir truffle_tests
-            cd truffle_tests
-            truffle unbox metacoin
-            coverage run -m manticore . --contract MetaCoin --workspace output --exclude-all --evm.oog ignore --evm.txfail optimistic
-            # Truffle smoke test. We test if manticore is able to generate states
-            # from a truffle project. 
-            if [ "$(ls output/*tx -l | wc -l)" != "26" ]; then
-                echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 26"
-                return 1
-            fi
-            echo "Truffle test succeded"
-            coverage xml
-            cd ..
-            cp truffle_tests/coverage.xml .
-            return 0
-        }
-
-        run_tests_from_dir() {
-            DIR=$1
-            COVERAGE_RCFILE=$GITHUB_WORKSPACE/.coveragerc
-            echo "Running only the tests from 'tests/$DIR' directory"
-            pytest --durations=100 --cov=manticore --cov-config=$GITHUB_WORKSPACE/.coveragerc -n auto "tests/$DIR"
-            coverage xml
-        }
-
-        run_examples() {
-            pushd examples/linux
-            make
-            for example in $(make list); do
-                ./$example < /dev/zero > /dev/null
-            done
-            echo Built and ran Linux examples
-            popd
-
-            pushd examples/script
-            launch_examples
-            RESULT=$?
-            echo Ran example scripts
-            coverage xml
-            popd
-            cp examples/script/coverage.xml .
-            return $RESULT
-        }
-
-        # Test type
-        case $TEST_TYPE in
-            ethereum_vm)
-                make_vmtests
-                run_tests_from_dir $TEST_TYPE
-                ;;
-            ethereum_truffle)
-                echo "Running truffle test"
-                install_truffle
-                run_truffle_tests
-                ;;
-            wasm)
-                make_wasm_tests
-                run_tests_from_dir $TEST_TYPE
-                ;;
-            wasm_sym)
-                make_wasm_sym_tests ;&  # Fallthrough
-            native)                 ;&  # Fallthrough
-            ethereum)               ;&  # Fallthrough
-            ethereum_bench)         ;&  # Fallthrough
-            other)
-                run_tests_from_dir $TEST_TYPE
-                ;;
-            examples)
-                run_examples
-                ;;
-            *)
-                echo "Unknown TEST_TYPE: '$TEST_TYPE'"
-                exit 3;
-                ;;
-        esac
+        cp scripts/run_tests.sh .
+        ./run_tests.sh
     - name: Coverage Upload
       uses: codecov/codecov-action@v1
       with:
         token: ${{ secrets.CODECOV_TOKEN }}
         file: ./coverage.xml
         yml: ./codecov.yml
 # Disabled this line because Codecov has been extra flaky lately, and having to re-run the entire
-# test suite until every coverage upload step succeeds is more of a hassle than it's worth. 
+# test suite until every coverage upload step succeeds is more of a hassle than it's worth.
 #        fail_ci_if_error: true
+  upload:
+    runs-on: ubuntu-latest
+    if: github.event_name == 'schedule'
+    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 --dev_release sdist bdist_wheel
+    - name: Upload to PyPI
+      uses: pypa/gh-action-pypi-publish@v1.2.2
+      with:
+        password: ${{ secrets.PYPI_UPLOAD }}
+
+
diff --git a/.github/workflows/osx.yml b/.github/workflows/osx.yml
@@ -0,0 +1,45 @@
+name: MacOS Tests
+
+on:
+  schedule:
+    # Run every day at 11 PM.
+    - cron:  '0 23 * * *'
+
+jobs:
+  tests:
+    runs-on: macos-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        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
+      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: |
+        EXTRAS="dev-noks"
+        pip install -e .[$EXTRAS]
+    - name: Install Mac Dependencies
+      run: |
+        brew install bash
+        brew tap ethereum/ethereum
+        brew install solidity@4
+        brew install wabt
+        brew install SRI-CSL/sri-csl/yices2
+        brew tap cvc4/cvc4
+        brew install cvc4/cvc4/cvc4
+    - name: Run Tests
+      env:
+        TEST_TYPE: ${{ matrix.type }}
+      run: |
+        cp scripts/run_tests.sh .
+        ./run_tests.sh
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,8 +1,59 @@
 # Change Log
 
-## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.3...HEAD)
+## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.4...HEAD)
 
-## 0.3.3 - 2020-01
+## 0.3.4 - 2020-06-26
+
+Thanks to our external contributors!
+ - [jimpo](https://github.com/trailofbits/manticore/commits?author=jimpo)
+ - [langston-barrett](https://github.com/trailofbits/manticore/commits?author=langston-barrett)
+
+### Ethereum
+* Support and test against EVM Istanbul [#1676](https://github.com/trailofbits/manticore/pull/1676)
+* **[Added API]** Added a `manticore-verifier` script for checking properties of smart contracts [#1717](https://github.com/trailofbits/manticore/pull/1717)
+* Fixed RETURNDATASIZE [#1612](https://github.com/trailofbits/manticore/pull/1612)
+* Added strategies for symbolic SHA3 replacement [#1609](https://github.com/trailofbits/manticore/pull/1609)
+* Fixed GAS instruction [#1633](https://github.com/trailofbits/manticore/pull/1633)
+* Improved balance-related exploration [#1615](https://github.com/trailofbits/manticore/pull/1615)
+* Add `__format__` to EVM accounts [#1613](https://github.com/trailofbits/manticore/pull/1613)
+* Discard basic blocks that unavoidably REVERT [#1630](https://github.com/trailofbits/manticore/pull/1630)
+* Extract printable bytes from return data [#1671](https://github.com/trailofbits/manticore/pull/1671)
+* Support CHAINID, EXTCODEHASH, and SELFBALANCE instructions [#1644](https://github.com/trailofbits/manticore/pull/1644)
+* **[Changed API]** Renamed several arguments in EVM API, including `gaslimit` --> `gas` [#1652](https://github.com/trailofbits/manticore/pull/1652)
+* Explore states that self-destruct [#1699](https://github.com/trailofbits/manticore/pull/1699)
+* Lazy solving for the Ethereum leak detector [#1727](https://github.com/trailofbits/manticore/pull/1727)
+
+### Native
+* Support for ARM modified-immediate encodings [#1638](https://github.com/trailofbits/manticore/pull/1638)
+* Support for `/proc/self/maps` [#1639](https://github.com/trailofbits/manticore/pull/1639)
+* Support for `llseek` [#1640](https://github.com/trailofbits/manticore/pull/1640)
+* Support for `arm_fadvise64_64` [#1648](https://github.com/trailofbits/manticore/pull/1648)
+* Allow symbolic sockets in `accept` [#1618](https://github.com/trailofbits/manticore/pull/1618)
+* Fixes to `open` [#1657](https://github.com/trailofbits/manticore/pull/1657)
+* Overhauled filesystem emulation [#1673](https://github.com/trailofbits/manticore/pull/1673)
+* Fixed system call argument concretization [#1697](https://github.com/trailofbits/manticore/pull/1697)
+* **[Added API]** Add a symbolic model for `strcpy` [#1681](https://github.com/trailofbits/manticore/pull/1681)
+
+### WASM
+* Delay branch condition concretization for better coverage [#1641](https://github.com/trailofbits/manticore/pull/1641)
+
+### Other
+* **[Added API]** Added a snapshot system [#1710](https://github.com/trailofbits/manticore/pull/1710)
+* Transparent compression for state files [#1624](https://github.com/trailofbits/manticore/pull/1624)
+* Unify around singleton interface for solver [#1649](https://github.com/trailofbits/manticore/pull/1649)
+* Use `__slots__` to reduce memory usage in expression system [#1635](https://github.com/trailofbits/manticore/pull/1635)
+* **[Removed API]** Removed `policy` argument from ManticoreBase, added `outputspace_url` to optionally separate working files from output files [#1651](https://github.com/trailofbits/manticore/pull/1651)
+* Disable broken `get_related` logic [#1674](https://github.com/trailofbits/manticore/pull/1674)
+* Disable flaky Z3 tactics [#1691](https://github.com/trailofbits/manticore/pull/1691)
+* Remove Keystone engine from dependencies [#1684](https://github.com/trailofbits/manticore/pull/1684)
+* Improved error messages [#1632](https://github.com/trailofbits/manticore/pull/1632), [#1704](https://github.com/trailofbits/manticore/pull/1704)
+* Made ConstraintSets hashable [#1703](https://github.com/trailofbits/manticore/pull/1703)
+* Added system to dynamically enable/disable plugins [#1696](https://github.com/trailofbits/manticore/pull/1696) [#1708](https://github.com/trailofbits/manticore/pull/1708)
+* Re-establish support for Yices and CVC4 [#1714](https://github.com/trailofbits/manticore/pull/1714)
+* Improved constant folding and constraint set slicing [#1706](https://github.com/trailofbits/manticore/pull/1706)
+
+
+## 0.3.3 - 2020-01-30
 
 Thanks to our external contributors!
 

diff --git a/README.md b/README.md
@@ -1,6 +1,6 @@
 # Manticore
 <p align="center">
-  <img src="docs/images/manticore.png?raw=true" width="256" title="Manticore">
+  <img src="https://raw.githubusercontent.com/trailofbits/manticore/master/docs/images/manticore.png" width="256" title="Manticore">
 </p>
 <br />
 
@@ -46,15 +46,21 @@ Option 2: Installing from PyPI, with extra dependencies needed to execute native
 pip install "manticore[native]"
 ```
 
-Option 3: Installing from the `master` branch:
+Option 3: Installing a nightly development build (fill in the latest version from [the PyPI history](https://pypi.org/project/manticore/#history)):
+
+```bash
+pip install "manticore[native]==0.x.x.devYYMMDD"
+```
+
+Option 4: 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:
+Option 5: Install via Docker:
 
 ```bash
 docker pull trailofbits/manticore
@@ -72,7 +78,8 @@ Manticore has a command line interface which can perform a basic symbolic analys
 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).
 
 #### EVM
-Solidity smart contracts must have a `.sol` extension for analysis by Manticore. See a [demo](https://asciinema.org/a/154012).
+Manticore CLI automatically detects you are trying to test a contract if (for ex.)
+ the contract has a `.sol` or a `.vy` extension. See a [demo](https://asciinema.org/a/154012).
 <details>
   <summary>Click to expand:</summary>
 
@@ -93,6 +100,12 @@ $ manticore examples/evm/umd_example.sol
 ```
 </details>
 
+##### Manticore-verifier
+
+An alternative CLI tool is provided that simplifys contract testing and 
+allows writing properties methods in the same high-level language the contract uses.
+Checkout manticore-verifier [documentation](http://manticore.readthedocs.io/en/latest/verifier.html).
+See a [demo](https://asciinema.org/a/xd0XYe6EqHCibae0RP6c7sJVE)
 
 #### Native
 <details>
@@ -132,7 +145,7 @@ contract Adder {
 """
 m = ManticoreEVM()
 
-user_account = m.create_account(balance=1000)
+user_account = m.create_account(balance=10000000)
 contract_account = m.solidity_create_contract(contract_src,
                                               owner=user_account,
                                               balance=0)
@@ -216,9 +229,9 @@ for idx, val_list in enumerate(m.collect_returns()):
 * 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. 
 
-## Using a different solverr (Z3, Yices, CVC4)
-Manticore relies on an external solver supporting smtlib2. Curently Z3, Yices and CVC4 are supported and can be selected via commandline or configuration settings.
-By default Manticore will use Z3. Once you installed a different solver you can choose a different solver like this:
+## Using a different solver (Z3, Yices, CVC4)
+Manticore relies on an external solver supporting smtlib2. Currently Z3, Yices and CVC4 are supported and can be selected via commandline or configuration settings.
+By default Manticore will use Z3. Once you've installed a different solver, you can choose which one to use like this:
 ```manticore --smt.solver yices```
 ### Installing CVC4
 For more details go to https://cvc4.github.io/. Otherwise just get the binary and use it.