-
Notifications
You must be signed in to change notification settings - Fork 472
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add doc, fix output bugs #1769
Merged
Merged
Add doc, fix output bugs #1769
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,172 @@ | ||
Property based symbolic executor: manticore-verifier | ||
==================================================== | ||
Manticore installs a separated CLI tool to do property based symbolic execution of smart contracts. :: | ||
|
||
$ manticore-verifier your_contract.sol | ||
|
||
**manticore-verifier** initializes an emulated blockchain ennvironment with a configurable set of | ||
feliam marked this conversation as resolved.
Show resolved
Hide resolved
|
||
acocunts and then sends various symbolic transactions to the target contract containing property methods. | ||
feliam marked this conversation as resolved.
Show resolved
Hide resolved
|
||
If a way to break a property is found the full transaction trace to reproduce the behaivor is provided. | ||
A configurable stopping condition bounds the exploration, properties not failing are considered to pass. | ||
|
||
|
||
Writing properties in {Solidity/ Vyper} | ||
--------------------------------------- | ||
**manticore-verifier** will detect and test property methods written in the | ||
original contract language. A property can be written in the original language | ||
by simply naming a method in a specific way. For example methods names starting with ```crytic_```. | ||
|
||
.. code-block:: javascript | ||
|
||
function crytic_test_true_property() view public returns (bool){ | ||
return true; | ||
} | ||
|
||
You can select your own way to name property methods using the ``--propre`` commandline argument. :: | ||
|
||
--propre PROPRE A regular expression for selecting properties | ||
|
||
Normal properties | ||
^^^^^^^^^^^^^^^^^ | ||
In the most common case after some precondition is met some logic property must always be true. | ||
Normal properties are property methods that must always return true (or REVERT). | ||
|
||
|
||
Reverting properties | ||
^^^^^^^^^^^^^^^^^^^^ | ||
Sometimes it is difficult to detect that a revert has happened in an internal transaction. | ||
manticor-verifier allows to test for ALWAYS REVERTing property methdos. | ||
feliam marked this conversation as resolved.
Show resolved
Hide resolved
|
||
Revert properties are property methods that must always REVERT. | ||
Reverting property are any property method that contains "revert". For example: | ||
|
||
.. code-block:: javascript | ||
|
||
function crytic_test_must_always_revert() view public returns (bool){ | ||
return true; | ||
} | ||
|
||
|
||
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. :: | ||
|
||
--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 as eparated unused account to actually check the property methods. | ||
feliam marked this conversation as resolved.
Show resolved
Hide resolved
|
||
There are 3 types of user accounts: | ||
|
||
- deployer: The account used to create the target contract | ||
- senders: A set of accounts used to send symbolic transactions. Think that these transactions are the ones trying to put the contract in a state that makes the property fail. | ||
- psender: The account used as caller to test tha actual property methos | ||
feliam marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
|
||
You can specify those via commanline arguments :: | ||
feliam marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
--deployer DEPLOYER (optional) address of account used to deploy the contract | ||
--senders SENDERS (optional) a comma separated list of sender addresses. | ||
The properties are going to be tested sending | ||
transactions from these addresses. | ||
--psender PSENDER (optional) address from where the property is tested | ||
|
||
|
||
Or, if you prefer, you can specify a yaml file like this :: | ||
|
||
deployer: "0x41414141414141414141" | ||
sender: ["0x51515151515151515151", "0x52525252525252525252"] | ||
psender: "0x616161616161616161" | ||
|
||
If you specify the accounts both ways the commandline takes precedence over the yaml file. | ||
If you do not provide specific accounts **manticore-verifier** will choose them for you. | ||
|
||
|
||
Stopping condition | ||
================== | ||
The exploration will continue to sent symbolic transactions until one of the stopping criteria is met. | ||
feliam marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
Maximun number of trasactions | ||
feliam marked this conversation as resolved.
Show resolved
Hide resolved
|
||
----------------------------- | ||
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 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 | ||
--------------------------- | ||
By default if a transaction does not produce new coverage the exploration is stopped. But you can add a further constraining, if the provided coverage percentage is obtained stop. Not that this is the total % of runtime bytecode covered. By default compilers add dead code and also in this case the rntime contains the code of the propertie methods. So use with care. :: | ||
feliam marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
--maxcov MAXCOV Stop after maxcov % coverage is obtained in the main | ||
contract | ||
|
||
|
||
Timeout | ||
------- | ||
Exploration will stop after the timeout seconds have pass. :: | ||
|
||
--timeout TIMEOUT Exploration timeout in seconds | ||
|
||
|
||
Walkthrough | ||
----------- | ||
Consider this little contract containing a bug: | ||
|
||
.. code-block:: javascript | ||
|
||
contract Ownership{ // It can have an owner! | ||
address owner = msg.sender; | ||
function Onwer() public{ | ||
owner = msg.sender; | ||
} | ||
modifier isOwner(){ | ||
require(owner == msg.sender); | ||
_; | ||
} | ||
} | ||
contract Pausable is Ownership{ //It is also pausable. You can pause it. You can resume it. | ||
bool is_paused; | ||
modifier ifNotPaused(){ | ||
require(!is_paused); | ||
_; | ||
} | ||
function paused() isOwner public{ | ||
is_paused = true; | ||
} | ||
function resume() isOwner public{ | ||
is_paused = false; | ||
} | ||
} | ||
contract Token is Pausable{ //<< HERE it is. | ||
mapping(address => uint) public balances; // It maintains a balance sheet | ||
function transfer(address to, uint value) ifNotPaused public{ //and can transfer value | ||
balances[msg.sender] -= value; // from one account | ||
balances[to] += value; // to the other | ||
} | ||
} | ||
|
||
Assuming the programmer did not want to allow the magic creation of tokens. | ||
We can design a property around the fact that the initial token count can not be increased over time. Even more relaxed, after the contract creation any account must have less that total count of tokens. The property looks like this : | ||
|
||
.. code-block:: javascript | ||
|
||
contract TestToken is Token{ | ||
constructor() public{ | ||
//here lets initialize the thing | ||
balances[msg.sender] = 10000; //deployer account owns it all! | ||
} | ||
|
||
function crytic_test_balance() view public returns (bool){ | ||
return balances[msg.sender] <= 10000; //nobody can have more than 100% of the tokens | ||
} | ||
|
||
} | ||
|
||
And you can unleash the verifier like this:: | ||
|
||
$manticore-verifier testtoken.sol --contract TestToken | ||
|
||
|
||
f/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This may need to be CLI-tools
And then inside that we should have manpage-like documentation on how to use the commandline tools for each tool. (So far we have plain manticore and manticore-verifier )