Skip to content
This repository was archived by the owner on Feb 14, 2025. It is now read-only.

manticore_workshop

Jump to bottom
Evan edited this page Jul 16, 2018 · 16 revisions

Table of contents

1. Manticore on the Command Line

1.1. Overview

Learning Objectives

  • Read Manticore output
  • Verify test cases created by Manticore
  • Read EVM

Tools

  • Manticore
  • solc

Target

1.2. Lesson

The easiest way to start working with manticore is on the command line. Manticore ships with many analysis options already built in. To analyze a contract with Manticore just pass the name of the contract to manticore on the command line

manticore <contract_source>

Without any additional arguments Manticore will run a "multi transaction analysis" on the contract during which it creates a completely new blockchain, a user to own the contract, and another 'attacker' user to interact with the contract. During the analysis manticore will have the attacker user initiate symbolic transactions until all of the code in the contract has been explored or code coverage ceases to improve.

After the analysis is complete manticore will output a folder(mcore_*) containing files that begin with global, test_. These files contain information generated during the symbolic exploration of the contract including the actual calldata of the transactions triggering each state. Each test is numbered and corresponds to

End States

An Ethereum transaction can end in a "terminated" state or an "alive" states.

Terminated States

  1. TXERROR

This error code indicates an unhandled error has occurred.

  1. THROW

Execution terminated in an exception. This can be caused by user generated exceptions with the throw statement or with exceptions like division by zero from doing arithmetic carelessly.

  1. REVERT

This indicates that the transaction is to be reverted. This can happen because of a failed assert(), require() or a call to revert(). Contracts may also be reverted in the event they run out of gas or for other reasons.

  1. SELFDESTRUCT This is the result of a selfdestruct() call or other operation that ultimately leads to execution of the selfdestruct opcode.

Alive States

  1. STOP

The Ethereum contract executed a STOP instruction. Identical to Return when no data is returned.

  1. RETURN

End state indicating the contract ended normally and optionally returned some data.

Manually verify path exploration

Run manticore on a contract without any arguments and explore the mcore_* directory produced. Each generated test case is prefixed with test_<number>. A summary of the test resides in the files ending in .summary. A record of the transactions executed reside in the files ending in .tx.

Remember that you can get the contract's function ids with solc --hashes

Exercise

Run manticore on the contract in the "simple" folder. Examine the output of manticore and answer the following questions:

  1. How many test cases were generated by Manticore? Are they unique?

  2. Examine a test case that terminates with a revert. There are no revert statements in contract.sol. Explain what happened.

  3. Modify contract.sol any way to like so that manticore generates 11 test cases.

  4. What are in the contents of each file?

Extension Contents
.constraints
.summary
.trace
.tx
.runtime_asm

2. Manticore Limitations

2.1. Overview

Learning Objectives

  • Discover the Limitations of Manticore
  • Predict when Manticore may not work

Tools

  • Manticore
  • Python

Target

2.2. Lesson

Read more about symbolic execution before proceeding to the exercise.

2.3. Exercise

Open contract.sol in hard_to_analyze.

  1. Can you predict how many test cases manticore would generate for this program?

  2. Can you rewrite this program so it has equivalent functionality without tripping up manticore.

  3. Can you create a program without loops that is challenging for manticore to analyze?

3. Scripting with Manticore

3.1. Overview

Learning Objectives

  • Learn about scripting in Manticore
  • Use symbolic data to relate inputs and outputs
  • Leverage the Manticore API to detect an integer overflow bug

Tools

  • Manticore
  • Python

Target

3.2. Lesson

Creating a harness to begin working with Manticore's internals

Manticore on the command line does a lot of set up that you have to do manually when using Manticore in a scripting environment. The following code Initializes a new symbolic blockchain m. On that blockchain it creates a two users with 1000 ETH each and a contract from contract.sol holding 0 ETH. The constructor for the contract (if one exists) is also executed here. At this point you can begin experimenting with the contract under test by executing transactions against it.

from manticore.ethereum import ManticoreEVM

#############################################
# Create a symbolic blockchain
#############################################

m = ManticoreEVM() # blockchain


with open('contract.sol','rb') as f:
    contract_src=f.read()

#############################################
# Create user and contract accounts
#############################################

owner_account=m.create_account(balance=1000)
attacker_account=m.create_account(balance=1000)

contract_account=m.solidity_create_contract(contract_src,
                                            owner=user_account,
                                            balance=0)

solidity_create_contract API docs solidity_create_accountAPI docs ManticoreEVM docs

Modeling a specific transaction

Modeling specific transactions in Manticore is just like invoking them in Solidity. When working with contract source code, Manticore parses all of the functions and makes them attributes of the python contract object. If the contract under test has a function called foo taking three arguments you could execute it in the following way:

contract_account.foo(1, 2, 3)

Should foo return a value it won't be returned by the above line. You can retrieve it from the ManticoreEVM object by accessing the last_return property.

In the above example all of the arguments are concrete, if you wanted to pass symbolic data to foo you can create some with make_symbolic_value() or with new_symbolic_value if you'd like to specify additional attributes about the data.

contract_account.foo(1, make_symbolic_value(), 3)

Options

Value

In addition to function arguments you can specify value to pass to the function.

contract_account.foo(1, make_symbolic_value(), 3, value=10)

Value is assumed to be in ETH and when left unspecified is assumed to be zero. You can also let value be symbolic.

Caller

Function calls are always initiated by an account on the blockchain. If you don't specify a caller it defaults to the contract owner which may not be what you want to model. It's good practice to always specify the caller to make the intention of your analysis known.

contract_account.foo(1, make_symbolic_value(), 3, value=10, caller=attacker_account)

3.3. Exercise

Change into the integer_overflow/high_level directory. contract.sol contains an integer overflow. Pass symbolic data to the function in the contract in order to taint the global variable. Can you use Manticore to prove that it's possible to overflow the variable? Initiate two transactions and then call the getter of the global variable. Use the operators library to describe to manticore what you don't want to happen and see if manticore can find inputs that make the bad thing happen.

Examining state

This is the most challenging and time consuming part of using Manticore effectively.

Until now we've only manipulated the blockchain by adding users and interacting with contracts. Manticore internally has a wealth of knowledge about how elements of the program relate to each other.

Detecting bad states manually

Internally Manticore uses SMT and z3 to model the program. Many people find the syntax of z3 pretty obtuse. Fortunately Manticore has a wrapper for all arithmetic operations that feels natural. Symbolic data objects also have common operators like + - / < > % == and so on overloaded. These overloads might get you into trouble if you're mixing manticore data types with python native data types so if you're uncertain always be explicit. When you make a comparison with symbolic data the resulting type is a condition. Conditions, when added to a model's constraints translate to an assert at the z3 layer. To add a condition object to a model invoke the constrain method of the ManticorEVM object or of a state object.

4. Advanced scripting with Manticore

4.1. Overview

Learning Objectives

  • Leverage symbolic data to the fullest extent possible
  • Discover the Plugin API
  • Detect all instances of integer overflow

Tools

  • Manticore
  • Python

Target

4.2. Lesson

Modeling transactions generally

In the Ethereum Virtual Machine function calls are made by the use of "transactions" that specify "calldata" to be processed. The calldata is composed of the function identifier and function arguments. You can make calldata symbolic in its entirety.

m.transaction(caller=user_account, address=contract_account, value=make_symbolic_value(), data=make_symbolic_buffer(164))

make_symbolic_buffer(164) represents 164 bytes of symbolic data. 4 bytes for a function identifier and 5, 32 byte quantities representing arguments.

Executing transactions in this way is extremely powerful. It allows you to free yourself from the burden of manually considering edge cases. Because everything is symbolic, including the actual function to be executed, Manticore will consider every possible case of a single function call being made. Earlier when you ran manticore on the command line this style of transaction was applied until all parts of the code were explored.

Detecting bad states with detector plugins

Detector plugins operate directly on EVM. Operating directly on EVM enables plugins authors to detect bad states directly instead of attempting to exhaustively model and instrument their applications. Instead of instrumenting the inputs and outputs of functions, detector plugins can instrument the inputs and outputs of EVM instructions. This increase in visibility can find bugs the previous method cannot.

4.3. Exercise

Read the DetectIntegerOverflow class inside Manticore's Ethereum library. Re-use the code from earlier exercises to Initialize the block chain, add users and create the contract. Instead of analyzing states manually, leverage the

Change into the integer_overflow/low_level directory. contract.sol is very similar to the contract in high_level with the exception that the global variable is no longer public. Manticore ships with a utility to automatically detect integer overflows by applying checks at the instruction level instead of at the function level. Register the IntegerOverflowDetector plugin and use it to verify the presence of an integer overflow.

Use the register_plugin method of the ManticoreEVM to attach the IntegerOverflowDetector plugin. The IntegerOverflowDetector object has a get_findings method which accepts states and returns information about detected integer overflows.

5. Detecting entire bug classes with Manticore

5.1. Overview

Learning Objectives

  • Write a detector plugin for Manticore
  • Find unchecked external calls in compiled third party contracts

Tools

  • Manticore

Target

5.2. Lesson

5.3. Exercise

Write a Detector plugin that can detect when the return value of a call isn't checked. External calls can fail for a variety of reasons but will always return a status code. Read how the integer overflow detector plugin is constructed for inspiration. The target directory has two folders, one is an old revision of the [King of the Ether Throne][koet] contract which, due to poor coding practices, could result in accidental loss of Ether. The other is a sample application that has the target behavior. Write a detector plugin that detects the bad behavior of the small contract first, then let it find bugs in the larger contract.

https://github.com/trailofbits/manticore/blob/master/manticore/ethereum.py#L196

Clone this wiki locally