Native

Platforms

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:

Manticore
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:

Manticore

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

Models

Models here are intended to be passed to invoke_model(), not invoked directly.

manticore.native.models.isvariadic(model)
Parameters:model (callable) – Function model
Returns:Whether model models a variadic function
Return type:bool
manticore.native.models.strcmp(state, s1, s2)

strcmp symbolic model.

Algorithm: Walks from end of string (minimum offset to NULL in either string) to beginning building tree of ITEs each time either of the bytes at current offset is symbolic.

Points of Interest: - We’ve been building up a symbolic tree but then encounter two concrete bytes that differ. We can throw away the entire symbolic tree! - If we’ve been encountering concrete bytes that match at the end of the string as we walk forward, and then we encounter a pair where one is symbolic, we can forget about that 0 ret we’ve been tracking and just replace it with the symbolic subtraction of the two

Parameters:
  • state (State) – Current program state
  • s1 (int) – Address of string 1
  • s2 (int) – Address of string 2
Returns:

Symbolic strcmp result
Return type:

Expression or int
manticore.native.models.strlen(state, s)

strlen symbolic model.

Algorithm: Walks from end of string not including NULL building ITE tree when current byte is symbolic.

Parameters:
  • state (State) – current program state
  • s (int) – Address of string
Returns:

Symbolic strlen result
Return type:

Expression or int
manticore.native.models.variadic(func)

A decorator used to mark a function model as variadic. This function should take two parameters: a State object, and a generator object for the arguments.

Parameters:func (callable) – Function model

State

class manticore.native.state.State(constraints, platform, **kwargs)
cpu

Current cpu state

execute()

Perform a single step on the current state

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
mem

Current virtual memory mappings

Cpu

class manticore.native.state.State(constraints, platform, **kwargs)
cpu

Current cpu state

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]
backup_emulate(insn)

If we could not handle emulating an instruction, use Unicorn to emulate it.

Parameters:instruction (capstone.CsInsn) – The instruction object to emulate
canonical_registers

Returns the list of all register names for this CPU.

Return type:tuple
Returns:the list of register names for this CPU.
canonicalize_instruction_name(instruction)

Get the semantic name of an instruction.

concrete_emulate(insn)

Start executing in Unicorn from this point until we hit a syscall or reach break_unicorn_at

Parameters:insn (capstone.CsInsn) – The instruction object to emulate
decode_instruction(pc)

This will decode an instruction from memory pointed by pc

Parameters:pc (int) – address of the instruction
emulate(insn)

Pick the right emulate function (maintains API compatiblity)

Parameters:insn – single instruction to emulate/start emulation from
emulate_until(target: int)

Tells the CPU to set up a concrete unicorn emulator and use it to execute instructions until target is reached.

Parameters:target – Where Unicorn should hand control back to Manticore. Set to 0 for all instructions.
execute()

Decode, and execute one instruction pointed by register PC

icount
instruction
memory
pop_bytes(nbytes, force=False)

Read nbytes from the stack, increment the stack pointer, and return data.

Parameters:
  • nbytes (int) – How many bytes to read
  • force – whether to ignore memory permissions
Returns:

Data read from the stack
pop_int(force=False)

Read a value from the stack and increment the stack pointer.

Parameters:force – whether to ignore memory permissions
Returns:Value read
push_bytes(data, force=False)

Write data to the stack and decrement the stack pointer accordingly.

Parameters:
  • data (str) – Data to write
  • force – whether to ignore memory permissions
push_int(value, force=False)

Decrement the stack pointer and write value to the stack.

Parameters:
  • value (int) – The value to write
  • force – whether to ignore memory permissions
Returns:

New stack pointer
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
read_string(where, max_length=None, force=False)

Read a NUL-terminated concrete buffer from memory. Stops reading at first symbolic byte.

Parameters:
  • where (int) – Address to read string from
  • max_length (int) – The size in bytes to cap the string at, or None [default] for no limit.
  • force – whether to ignore memory permissions
Returns:

string read
Return type:

str
regfile

The RegisterFile of this cpu

render_instruction(insn=None)
render_register(reg_name)
render_registers()
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
write_string(where, string, max_length=None, force=False)

Writes a string to memory, appending a NULL-terminator at the end.

Parameters:
  • where (int) – Address to write the string to
  • string (str) – The string to write to memory
  • max_length (int) –

The size in bytes to cap the string at, or None [default] for no limit. This includes the NULL terminator.

Parameters:force – whether to ignore memory permissions

Memory

class manticore.native.state.State(constraints, platform, **kwargs)
mem

Current virtual memory mappings

class manticore.native.memory.SMemory(constraints, symbols=None, *args, **kwargs)

The symbolic memory manager. This class handles all virtual memory mappings and symbolic chunks.

Todo:improve comments
munmap(start, size)

Deletes the mappings for the specified address range and causes further references to addresses within the range to generate invalid memory references.

Parameters:
  • start – the starting address to delete.
  • size – the length of the unmapping.
read(address, size, force=False)

Read a stream of potentially symbolic bytes from a potentially symbolic address

Parameters:
  • address – Where to read from
  • size – How many bytes
  • force – Whether to ignore permissions
Return type:

list
write(address, value, force=False)

Write a value at address.

Parameters:
  • address (int or long or Expression) – The address at which to write
  • value (str or list) – Bytes to write
  • force – Whether to ignore permissions

State

class manticore.native.state.State(constraints, platform, **kwargs)
cpu

Current cpu state

execute()

Perform a single step on the current state

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
mem

Current virtual memory mappings

Function Models

The Manticore function modeling API can be used to override a certain function in the target program with a custom implementation in Python. This can greatly increase performance.

Manticore comes with implementations of function models for some common library routines (core models), and also offers a user API for defining user-defined models.

To use a core model, use the invoke_model() API. The available core models are documented in the API Reference:

from manticore.native.models import strcmp
addr_of_strcmp = 0x400510
@m.hook(addr_of_strcmp)
def strcmp_model(state):
    state.invoke_model(strcmp)

To implement a user-defined model, implement your model as a Python function, and pass it to invoke_model(). See the invoke_model() documentation for more. The core models are also good examples to look at and use the same external user API.

Symbolic Input

Manticore allows you to execute programs with symbolic input, which represents a range of possible inputs. You can do this in a variety of manners.

Wildcard byte

Throughout these various interfaces, the ‘+’ character is defined to designate a byte of input as symbolic. This allows the user to make input that mixes symbolic and concrete bytes (e.g. known file magic bytes).

For example: "concretedata++++++++moreconcretedata++++++++++"

Symbolic arguments/environment

To provide a symbolic argument or environment variable on the command line, use the wildcard byte where arguments and environment are specified.:

$ manticore ./binary +++++ +++++
$ manticore ./binary --env VAR1=+++++ --env VAR2=++++++

For API use, use the argv and envp arguments to the manticore.native.Manticore.linux() classmethod.:

Manticore.linux('./binary', ['++++++', '++++++'], dict(VAR1='+++++', VAR2='++++++'))

Symbolic stdin

Manticore by default is configured with 256 bytes of symbolic stdin data which is configurable with the stdin_size kwarg of manticore.native.Manticore.linux() , after an optional concrete data prefix, which can be provided with the concrete_start kwarg of manticore.native.Manticore.linux().

Symbolic file input

To provide symbolic input from a file, first create the files that will be opened by the analyzed program, and fill them with wildcard bytes where you would like symbolic data to be.

For command line use, invoke Manticore with the --file argument.:

$ manticore ./binary --file my_symbolic_file1.txt --file my_symbolic_file2.txt

For API use, use the add_symbolic_file() interface to customize the initial execution state from an __init__()

@m.init
def init(initial_state):
    initial_state.platform.add_symbolic_file('my_symbolic_file1.txt')

Symbolic sockets

Manticore’s socket support is experimental! Sockets are configured to contain 64 bytes of symbolic input.