API Reference¶
This API is under active development, and should be considered unstable.
Core Helpers¶
-
manticore.
issymbolic
(value)¶ Helper to determine whether an object is symbolic (e.g checking if data read from memory is symbolic)
Parameters: value (object) – object to check Returns: whether value is symbolic Return type: bool
-
manticore.
istainted
(arg, taint=None)¶ Helper to determine whether an object if tainted. :param arg: a value or Expression :param taint: a regular expression matching a taint value (eg. ‘IMPORTANT.*’). If None, this function checks for any taint value.
Native Helpers¶
ManticoreBase¶
-
class
manticore.core.manticore.
ManticoreBase
(initial_state, workspace_url=None, policy='random', **kwargs)¶ -
locked_context
(key=None, value_type=<class 'list'>)¶ A context manager that provides safe parallel access to the global Manticore context. This should be used to access the global Manticore context when parallel analysis is activated. Code within the with block is executed atomically, so access of shared variables should occur within.
Example use:
with m.locked_context() as context: visited['visited'].append(state.cpu.PC)
Optionally, parameters can specify a key and type for the object paired to this key.:
with m.locked_context('feature_list', list) as feature_list: feature_list.append(1)
Note: If standard (non-proxy) list or dict objects are contained in a referent, modifications to those mutable values will not be propagated through the manager because the proxy has no way of knowing when the values contained within are modified. However, storing a value in a container proxy (which triggers a __setitem__ on the proxy object) does propagate through the manager and so to effectively modify such an item, one could re-assign the modified value to the container proxy:
Parameters: - key (object) – Storage key
- value_type (list or dict or set) – type of value associated with key
-
run
(timeout=None)¶ Runs analysis. :param timeout: Analysis timeout, in seconds
-
static
verbosity
(level)¶ Sets global vervosity level. This will activate different logging profiles globally depending on the provided numeric value
-
native.Manticore¶
-
class
manticore.native.
Manticore
(path_or_state, argv=None, workspace_url=None, policy='random', **kwargs)¶ -
classmethod
decree
(path, concrete_start='', **kwargs)¶ Constructor for Decree binary analysis.
Parameters: - path (str) – Path to binary to analyze
- concrete_start (str) – Concrete stdin to use before symbolic input
- kwargs – Forwarded to the Manticore constructor
Returns: Manticore instance, initialized with a Decree State
Return type:
-
classmethod
linux
(path, argv=None, envp=None, entry_symbol=None, symbolic_files=None, concrete_start='', pure_symbolic=False, stdin_size=None, **kwargs)¶ Constructor for Linux binary analysis.
Parameters: - path (str) – Path to binary to analyze
- argv (list[str]) – Arguments to provide to the binary
- envp (str) – Environment to provide to the binary
- entry_symbol – Entry symbol to resolve to start execution
- symbolic_files (list[str]) – Filenames to mark as having symbolic input
- concrete_start (str) – Concrete stdin to use before symbolic input
- stdin_size (int) – symbolic stdin size to use
- kwargs – Forwarded to the Manticore constructor
Returns: Manticore instance, initialized with a Linux State
Return type:
-
classmethod
BaseState¶
-
class
manticore.core.state.
StateBase
(constraints, platform, **kwargs)¶ Representation of a unique program state/path.
Parameters: - constraints (ConstraintSet) – Initial constraints
- platform (Platform) – Initial operating system state
Variables: context (dict) – Local context for arbitrary data storage
-
abandon
()¶ Abandon the currently-active state.
Note: This must be called from the Executor loop, or a
hook()
.
-
constrain
(constraint)¶ Constrain state.
Parameters: constraint (manticore.core.smtlib.Bool) – Constraint to add
-
new_symbolic_buffer
(nbytes, **options)¶ Create and return a symbolic buffer of length nbytes. The buffer is not written into State’s memory; write it to the state’s memory to introduce it into the program state.
Parameters: - nbytes (int) – Length of the new buffer
- label (str) – (keyword arg only) The label to assign to the buffer
- cstring (bool) – (keyword arg only) Whether or not to enforce that the buffer is a cstring (i.e. no NULL bytes, except for the last byte). (bool)
- taint (tuple or frozenset) – Taint identifier of the new buffer
Returns: Expression
representing the buffer.
-
new_symbolic_value
(nbits, label=None, taint=frozenset())¶ Create and return a symbolic value that is nbits bits wide. Assign the value to a register or write it into the address space to introduce it into the program state.
Parameters: - nbits (int) – The bitwidth of the value returned
- label (str) – The label to assign to the value
- taint (tuple or frozenset) – Taint identifier of this value
Returns: Expression
representing the value
-
solve_buffer
(addr, nbytes, constrain=False)¶ Reads nbytes of symbolic data from a buffer in memory at addr and attempts to concretize it
Parameters: - address (int) – Address of buffer to concretize
- nbytes (int) – Size of buffer to concretize
- constrain (bool) – If True, constrain the buffer to the concretized value
Returns: Concrete contents of buffer
Return type: list[int]
-
solve_n
(expr, nsolves)¶ Concretize a symbolic
Expression
into nsolves solutions.Parameters: expr (manticore.core.smtlib.Expression) – Symbolic value to concretize Returns: Concrete value Return type: list[int]
-
solve_one
(expr, constrain=False)¶ Concretize a symbolic
Expression
into one solution.Parameters: - expr (manticore.core.smtlib.Expression) – Symbolic value to concretize
- constrain (bool) – If True, constrain expr to concretized value
Returns: Concrete value
Return type: int
-
symbolicate_buffer
(data, label='INPUT', wildcard='+', string=False, taint=frozenset())¶ Mark parts of a buffer as symbolic (demarked by the wildcard byte)
Parameters: - data (str) – The string to symbolicate. If no wildcard bytes are provided, this is the identity function on the first argument.
- label (str) – The label to assign to the value
- wildcard (str) – The byte that is considered a wildcard
- string (bool) – Ensure bytes returned can not be NULL
- taint (tuple or frozenset) – Taint identifier of the symbolicated data
Returns: If data does not contain any wildcard bytes, data itself. Otherwise, a list of values derived from data. Non-wildcard bytes are kept as is, wildcard bytes are replaced by Expression objects.
native.State¶
-
class
manticore.native.state.
State
(constraints, platform, **kwargs)¶ -
invoke_model
(model)¶ Invokes a model. Modelling can be used to override a function in the target program with a custom implementation.
For more information on modelling see docs/models.rst
A model is a callable whose first argument is a manticore.native.State instance. If the following arguments correspond to the arguments of the C function being modeled. If the model models a variadic function, the following argument is a generator object, which can be used to access function arguments dynamically. The model callable should simply return the value that should be returned by the native function being modeled.f
Parameters: model – callable, model to invoke
-
SLinux¶
Symbolic Linux
-
class
manticore.platforms.linux.
SLinux
(programs, argv=None, envp=None, symbolic_files=None, disasm='capstone', pure_symbolic=False)¶ Builds a symbolic extension of a Linux OS
Parameters: - programs (str) – path to ELF binary
- disasm (str) – disassembler to be used
- argv (list) – argv not including binary
- envp (list) – environment variables
- symbolic_files (tuple[str]) – files to consider symbolic
-
add_symbolic_file
(symbolic_file)¶ Add a symbolic file. Each ‘+’ in the file will be considered as symbolic; other chars are concretized. Symbolic files must have been defined before the call to run().
Parameters: symbolic_file (str) – the name of the symbolic file
Cpu¶
-
class
manticore.native.cpu.abstractcpu.
Cpu
(regfile, memory, **kwargs)¶ Base class for all Cpu architectures. Functionality common to all architectures (and expected from users of a Cpu) should be here. Commonly used by platforms and py:class:manticore.core.Executor
The following attributes need to be defined in any derived class
- arch
- mode
- max_instr_width
- address_bit_size
- pc_alias
- stack_alias
-
all_registers
¶ Returns all register names for this CPU. Any register returned can be accessed via a cpu.REG convenience interface (e.g. cpu.EAX) for both reading and writing.
Returns: valid register names Return type: tuple[str]
-
read_bytes
(where, size, force=False)¶ Read from memory.
Parameters: - where (int) – address to read data from
- size (int) – number of bytes
- force – whether to ignore memory permissions
Returns: data
Return type: list[int or Expression]
-
read_int
(where, size=None, force=False)¶ Reads int from memory
Parameters: - where (int) – address to read from
- size – number of bits to read
- force – whether to ignore memory permissions
Returns: the value read
Return type: int or BitVec
-
read_register
(register)¶ Dynamic interface for reading cpu registers
Parameters: register (str) – register name (as listed in self.all_registers) Returns: register value Return type: int or long or Expression
-
write_bytes
(where, data, force=False)¶ Write a concrete or symbolic (or mixed) buffer to memory
Parameters: - where (int) – address to write to
- data (str or list) – data to write
- force – whether to ignore memory permissions
-
write_int
(where, expression, size=None, force=False)¶ Writes int to memory
Parameters: - where (int) – address to write to
- expr (int or BitVec) – value to write
- size – bit size of expr
- force – whether to ignore memory permissions
-
write_register
(register, value)¶ Dynamic interface for writing cpu registers
Parameters: - register (str) – register name (as listed in self.all_registers)
- value (int or long or Expression) – register value
Models¶
Models here are intended to be passed to invoke_model()
, not invoked directly.
-
manticore.native.models.
strlen
()¶
-
manticore.native.models.
strcmp
()¶
EVM¶
Symbolic EVM implementation based on the yellow paper: http://gavwood.com/paper.pdf
-
class
manticore.ethereum.
ABI
¶ This class contains methods to handle the ABI. The Application Binary Interface is the standard way to interact with contracts in the Ethereum ecosystem, both from outside the blockchain and for contract-to-contract interaction.
-
static
function_call
(type_spec, *args)¶ Build transaction data from function signature and arguments
-
static
function_selector
(method_name_and_signature)¶ Makes a function hash id from a method signature
-
static
serialize
(ty, *values, **kwargs)¶ Serialize value using type specification in ty. ABI.serialize(‘int256’, 1000) ABI.serialize(‘(int, int256)’, 1000, 2000)
-
static
-
class
manticore.ethereum.
ManticoreEVM
(workspace_url: str = None, policy: str = 'random')¶ Manticore EVM manager
Usage Ex:
from manticore.ethereum import ManticoreEVM, ABI m = ManticoreEVM() #And now make the contract account to analyze source_code = ''' pragma solidity ^0.4.15; contract AnInt { uint private i=0; function set(uint value){ i=value } } ''' #Initialize user and contracts user_account = m.create_account(balance=1000) contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0) contract_account.set(12345, value=100) m.finalize()
-
static
compile
(source_code, contract_name=None, libraries=None, runtime=False, solc_bin=None, solc_remaps=[])¶ Get initialization bytecode from a Solidity source code
-
create_account
(balance=0, address=None, code=None, name=None)¶ Low level creates an account. This won’t generate a transaction.
Parameters: - balance (int or BitVecVariable) – balance to be set on creation (optional)
- address (int) – the address for the new account (optional)
- code – the runtime code for the new account (None means normal account), str or bytes (optional)
- name – a global account name eg. for use as reference in the reports (optional)
Returns: an EVMAccount
-
create_contract
(owner, balance=0, address=None, init=None, name=None, gas=None)¶ Creates a contract
Parameters: - owner (int or EVMAccount) – owner account (will be default caller in any transactions)
- balance (int or BitVecVariable) – balance to be transferred on creation
- address (int) – the address for the new contract (optional)
- init (str) – initializing evm bytecode and arguments
- name (str) – a unique name for reference
- gas – gas budget for the creation/initialization of the contract
Return type: EVMAccount
-
finalize
(procs=10)¶ Terminate and generate testcases for all currently alive states (contract states that cleanly executed to a STOP or RETURN in the last symbolic transaction).
Parameters: procs – nomber of local processes to use in the reporting generation
-
generate_testcase
(state, message='', only_if=None, name='user')¶ Generate a testcase to the workspace for the given program state. The details of what a testcase is depends on the type of Platform the state is, but involves serializing the state, and generating an input (concretizing symbolic variables) to trigger this state.
The only_if parameter should be a symbolic expression. If this argument is provided, and the expression can be true in this state, a testcase is generated such that the expression will be true in the state. If it is impossible for the expression to be true in the state, a testcase is not generated.
This is useful for conveniently checking a particular invariant in a state, and generating a testcase if the invariant can be violated.
For example, invariant: “balance” must not be 0. We can check if this can be violated and generate a testcase:
m.generate_testcase(state, 'balance CAN be 0', only_if=balance == 0) # testcase generated with an input that will violate invariant (make balance == 0)
Parameters: - state (manticore.core.state.State) –
- message (str) – longer description of the testcase condition
- only_if (manticore.core.smtlib.Bool) – only if this expr can be true, generate testcase. if is None, generate testcase unconditionally.
- name (str) – short string used as the prefix for the workspace key (e.g. filename prefix for testcase files)
Returns: If a testcase was generated
Return type: bool
-
get_balance
(address, state_id=None)¶ Balance for account address on state state_id
-
get_code
(address, state_id=None)¶ Storage data for offset on account address on state state_id
-
get_metadata
(address) → Optional[manticore.ethereum.solidity.SolidityMetadata]¶ Gets the solidity metadata for address. This is available only if address is a contract created from solidity
-
get_storage_data
(address, offset, state_id=None)¶ Storage data for offset on account address on state state_id
-
get_world
(state_id=None)¶ Returns the evm world of state_id state.
-
global_coverage
(account)¶ Returns code coverage for the contract on account_address. This sums up all the visited code lines from any of the explored states.
-
human_transactions
(state_id=None)¶ Transactions list for state state_id
-
json_create_contract
(jfile, owner=None, name=None, contract_name=None, balance=0, gas=None, network_id=None, args=())¶ Creates a solidity contract based on a truffle json artifact. https://github.com/trufflesuite/truffle/tree/develop/packages/truffle-contract-schema :param jfile: truffle json artifact :type jfile: str or IOBase :param owner: owner account (will be default caller in any transactions) :type owner: int or EVMAccount :param contract_name: Name of the contract to analyze (optional if there is a single one in the source code) :type contract_name: str :param balance: balance to be transferred on creation :type balance: int or BitVecVariable :param gas: gas budget for each contract creation needed (may be more than one if several related contracts defined in the solidity source) :type gas: int :param network_id: Truffle network id to instantiate :param tuple args: constructor arguments :rtype: EVMAccount
-
last_return
(state_id=None)¶ Last returned buffer for state state_id
-
make_symbolic_address
(name=None, select='both')¶ Creates a symbolic address and constrains it to pre-existing addresses or the 0 address.
Parameters: - name – Name of the symbolic variable. Defaults to ‘TXADDR’ and later to ‘TXADDR_<number>’
- select – Whether to select contracts or normal accounts. Not implemented for now.
Returns: Symbolic address in form of a BitVecVariable.
-
make_symbolic_arguments
(types)¶ Build a reasonable set of symbolic arguments matching the types list
-
make_symbolic_buffer
(size, name=None, avoid_collisions=False)¶ Creates a symbolic buffer of size bytes to be used in transactions. You can operate on it normally and add constraints to manticore.constraints via manticore.constrain(constraint_expression)
Example use:
symbolic_data = m.make_symbolic_buffer(320) m.constrain(symbolic_data[0] == 0x65) m.transaction(caller=attacker_account, address=contract_account, data=symbolic_data, value=100000 )
-
make_symbolic_value
(nbits=256, name=None)¶ Creates a symbolic value, normally a uint256, to be used in transactions. You can operate on it normally and add constraints to manticore.constraints via manticore.constrain(constraint_expression)
Example use:
symbolic_value = m.make_symbolic_value() m.constrain(symbolic_value > 100) m.constrain(symbolic_value < 1000) m.transaction(caller=attacker_account, address=contract_account, data=data, value=symbolic_value )
-
new_address
()¶ Create a fresh 160bit address
-
preconstraint_for_call_transaction
(address: Union[int, manticore.ethereum.account.EVMAccount], data: manticore.core.smtlib.expression.Array, value: Union[int, manticore.core.smtlib.expression.Expression, None] = None, contract_metadata: Optional[manticore.ethereum.solidity.SolidityMetadata] = None) → manticore.core.smtlib.expression.BoolOperation¶ Returns a constraint that excludes combinations of value and data that would cause an exception in the EVM contract dispatcher. :param address: address of the contract to call :param value: balance to be transferred (optional) :param data: symbolic transaction data :param contract_metadata: SolidityMetadata for the contract (optional)
-
register_detector
(d)¶ Unregisters a plugin. This will invoke detector’s on_unregister callback. Shall be called after .finalize.
-
run
(**kwargs)¶ Runs analysis. :param timeout: Analysis timeout, in seconds
-
solidity_create_contract
(source_code, owner, name=None, contract_name=None, libraries=None, balance=0, address=None, args=(), solc_bin=None, solc_remaps=[], working_dir=None, gas=None)¶ Creates a solidity contract and library dependencies
Parameters: - source_code (str) – solidity source code
- owner (int or EVMAccount) – owner account (will be default caller in any transactions)
- contract_name (str) – Name of the contract to analyze (optional if there is a single one in the source code)
- balance (int or BitVecVariable) – balance to be transferred on creation
- address (int or EVMAccount) – the address for the new contract (optional)
- args (tuple) – constructor arguments
- solc_bin (str) – path to solc binary
- solc_remaps (list of str) – solc import remaps
- working_dir (str) – working directory for solc compilation (defaults to current)
- gas (int) – gas budget for each contract creation needed (may be more than one if several related contracts defined in the solidity source)
Return type: EVMAccount
-
transaction
(caller, address, value, data, gas=None)¶ Issue a symbolic transaction in all running states
Parameters: - caller (int or EVMAccount) – the address of the account sending the transaction
- address (int or EVMAccount) – the address of the contract to call
- value (int or BitVecVariable) – balance to be transfered on creation
- data – initial data
- gas – gas budget
Raises: NoAliveStates – if there are no alive states to execute
-
transactions
(state_id=None)¶ Transactions list for state state_id
-
unregister_detector
(d)¶ Unregisters a detector. This will invoke detector’s on_unregister callback. Shall be called after .finalize - otherwise, finalize won’t add detector’s finding to global.findings.
-
world
¶ The world instance or None if there is more than one state
-
static