Skip to content

Commit

Permalink
Merge branch 'master' into test-multiple-pythons
Browse files Browse the repository at this point in the history
* master:
  Project is in Maintenance Mode (#2645)
  update link to empirehacking slack (#2644)
  Add CODEOWNERS file (#2633)
  Bump coverallsapp/github-action from 1.1.3 to 2.1.0 (#2632)
  Bump pypa/gh-action-pip-audit from 1.0.4 to 1.0.6 (#2618)
  Fix: typos (#2615)
  [chore] fix build badges (#2614)
  • Loading branch information
ekilmer committed Sep 15, 2023
2 parents 43d35fd + 8861005 commit 4d8a184
Show file tree
Hide file tree
Showing 6 changed files with 24 additions and 15 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -158,7 +158,7 @@ jobs:
runs-on: ubuntu-22.04
steps:
- name: Coveralls Finished
uses: coverallsapp/github-action@1.1.3
uses: coverallsapp/github-action@v2.1.0
with:
github-token: ${{ secrets.GITHUB_TOKEN }}
parallel-finished: true
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/pip-audit.yml
Original file line number Diff line number Diff line change
Expand Up @@ -22,4 +22,4 @@ jobs:
python -m pip install --upgrade pip setuptools
python -m pip install .
- name: Run pip-audit
uses: pypa/gh-action-pip-audit@v1.0.4
uses: pypa/gh-action-pip-audit@v1.0.6
1 change: 1 addition & 0 deletions CODEOWNERS
Validating CODEOWNERS rules …
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
* @ekilmer
2 changes: 1 addition & 1 deletion CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ instead.
## Questions

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/)
response if you ask in our [chat room](https://slack.empirehacking.nyc/)
(in the #manticore channel).

## Legal
Expand Down
18 changes: 13 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,18 +1,26 @@
# :warning: Project is in Maintenance Mode :warning:

This project is no longer internally developed and maintained. However, we are happy to review and accept small, well-written pull requests by the community. We will only consider bug fixes and minor enhancements.

Any new or currently open issues and discussions shall be answered and supported by the community.

# Manticore
<p align="center">
<img src="https://raw.githubusercontent.com/trailofbits/manticore/master/docs/images/manticore.png" width="256" title="Manticore">
</p>
<br />


[![Build Status](https://img.shields.io/github/workflow/status/trailofbits/manticore/CI/master)](https://github.com/trailofbits/manticore/actions?query=workflow%3ACI)
[![Build Status](https://img.shields.io/github/actions/workflow/status/trailofbits/manticore/ci.yml?branch=master)](https://github.com/trailofbits/manticore/actions?query=workflow%3ACI)
[![Coverage Status](https://coveralls.io/repos/github/trailofbits/manticore/badge.svg)](https://coveralls.io/github/trailofbits/manticore)
[![PyPI Version](https://badge.fury.io/py/manticore.svg)](https://badge.fury.io/py/manticore)
[![Slack Status](https://empireslacking.herokuapp.com/badge.svg)](https://empireslacking.herokuapp.com)
[![Slack Status](https://slack.empirehacking.nyc/badge.svg)](https://slack.empirehacking.nyc)
[![Documentation Status](https://readthedocs.org/projects/manticore/badge/?version=latest)](http://manticore.readthedocs.io/en/latest/?badge=latest)
[![Example Status](https://img.shields.io/github/workflow/status/trailofbits/manticore-examples/CI/master)](https://github.com/trailofbits/manticore-examples/actions?query=workflow%3ACI)
[![Example Status](https://img.shields.io/github/actions/workflow/status/trailofbits/manticore-examples/ci.yml?branch=master)](https://github.com/trailofbits/manticore-examples/actions?query=workflow%3ACI)
[![LGTM Total Alerts](https://img.shields.io/lgtm/alerts/g/trailofbits/manticore.svg?logo=lgtm&logoWidth=18)](https://lgtm.com/projects/g/trailofbits/manticore/alerts/)



Manticore is a symbolic execution tool for the analysis of smart contracts and binaries.

## Features
Expand Down Expand Up @@ -102,7 +110,7 @@ $ manticore examples/evm/umd_example.sol

##### Manticore-verifier

An alternative CLI tool is provided that simplifys contract testing and
An alternative CLI tool is provided that simplifies 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)
Expand Down Expand Up @@ -248,7 +256,7 @@ Yices is incredibly fast. More details here https://yices.csl.sri.com/

## Getting Help

Feel free to stop by our #manticore slack channel in [Empire Hacking](https://empireslacking.herokuapp.com/) for help using or extending Manticore.
Feel free to stop by our #manticore slack channel in [Empire Hacking](https://slack.empirehacking.nyc/) for help using or extending Manticore.

Documentation is available in several places:

Expand Down
14 changes: 7 additions & 7 deletions docs/verifier.rst
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ Manticore installs a separated CLI tool to do property based symbolic execution

**manticore-verifier** initializes an emulated blockchain environment with a configurable set of
accounts and then sends various symbolic transactions to the target contract containing property methods.
If a way to break a property is found the full transaction trace to reproduce the behaivor is provided.
If a way to break a property is found the full transaction trace to reproduce the behavior is provided.
A configurable stopping condition bounds the exploration, properties not failing are considered to pass.


Expand Down Expand Up @@ -48,16 +48,16 @@ Reverting property are any property method that contains "revert". For example:
Selecting a target contract
===========================
**manticore-verifier** needs to be pointed to a the target contract containing any number of property methods.
The target contract is the entry point of the exploration. It needs to initilize any internal structure or external contracts to a correct initial state. All methods of this contract matching the property name criteria will be tested. ::
**manticore-verifier** needs to be pointed to the target contract containing any number of property methods.
The target contract is the entry point of the exploration. It needs to initialize any internal structure or external contracts to a correct initial state. All methods of this contract matching the property name criteria will be tested. ::

--contract_name CONTRACT_NAME The target contract name defined in the source code


User accounts
=============
You can specify what are the accounts used in the exploration.
Normaly you do not want the owner or deployer of the contract to send the symbolic transaction and to use a separate unused account to actually check the property methods.
Normally you do not want the owner or deployer of the contract to send the symbolic transaction and to use a separate unused account to actually check the property methods.
There are 3 types of user accounts:

- deployer: The account used to create the target contract
Expand Down Expand Up @@ -90,12 +90,12 @@ The exploration will continue to send symbolic transactions until one of the sto

Maximum number of transactions
-----------------------------
You can be interested only in what could happen under a number of transactions. After a maximun number of transactions is reached the explorations ends. Properties that had not be found to be breakable are considered a pass.
You can be interested only in what could happen under a number of transactions. After a maximum number of transactions is reached the explorations ends. Properties that had not been found to be breakable are considered a pass.
You can modify the max number of transactions to test vis a command line argument, otherwise it will stop at 3 transactions. ::

--maxt MAXT Max transaction count to explore
Maximun coverage % attained
Maximum coverage % attained
---------------------------
By default, if a transaction does not produce new coverage, the exploration is stopped. But you can add a further constraint so that if the provided coverage percentage is obtained, stop. Note that this is the total % of runtime bytecode covered. By default, compilers add dead code, and also in this case the runtime contains the code of the properties methods. So use with care. ::

Expand All @@ -105,7 +105,7 @@ By default, if a transaction does not produce new coverage, the exploration is s

Timeout
-------
Exploration will stop after the timeout seconds have pass. ::
Exploration will stop after the timeout seconds have passed. ::

--timeout TIMEOUT Exploration timeout in seconds

Expand Down

0 comments on commit 4d8a184

Please sign in to comment.