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.can_be_NULL(state, byte) → bool

Checks if a given byte read from memory can be NULL

Parameters

  • byte – byte read from memory to be examined

  • constrs – state constraints

Returns

whether a given byte is NULL or can be NULL

manticore.native.models.cannot_be_NULL(state, byte) → bool

Checks if a given byte read from memory is not NULL or cannot be NULL

Parameters

  • byte – byte read from memory to be examined

  • constrs – state constraints

Returns

whether a given byte is not NULL or cannot be NULL

manticore.native.models.isvariadic(model)
Parameters

model (callable) – Function model

Returns

Whether model models a variadic function

Return type

bool

manticore.native.models.must_be_NULL(state, byte) → bool

Checks if a given byte read from memory is NULL. This supports both concrete & symbolic byte values.

Parameters

  • byte – byte read from memory to be examined

  • constrs – state constraints

Returns

whether a given byte is NULL or constrained to NULL

manticore.native.models.strcmp(state: manticore.native.state.State, s1: Union[int, manticore.core.smtlib.expression.BitVec], s2: Union[int, manticore.core.smtlib.expression.BitVec])

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 – Current program state

  • s1 – Address of string 1

  • s2 – Address of string 2

Returns

Symbolic strcmp result

Return type

Expression or int

manticore.native.models.strcpy(state: manticore.native.state.State, dst: Union[int, manticore.core.smtlib.expression.BitVec], src: Union[int, manticore.core.smtlib.expression.BitVec]) → Union[int, manticore.core.smtlib.expression.BitVec]

strcpy symbolic model

Algorithm: Copy every byte from src to dst until finding a byte that is NULL or is constrained to only the NULL value. Every time a byte is fouund that can be NULL but is not definetly NULL concretize and fork states.

Parameters

  • state – current program state

  • dst – destination string address

  • src – source string address

Returns

pointer to the dst

manticore.native.models.strlen_approx(state: manticore.native.state.State, s: Union[int, manticore.core.smtlib.expression.BitVec]) → Union[int, manticore.core.smtlib.expression.BitVec]

strlen symbolic model

Strategy: build a result tree to limit state explosion results approximate

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

Parameters

  • state – current program state

  • s – Address of string

Returns

Symbolic strlen result

manticore.native.models.strlen_exact(state: manticore.native.state.State, s: Union[int, manticore.core.smtlib.expression.BitVec]) → Union[int, manticore.core.smtlib.expression.BitVec]

strlen symbolic model

Strategy: produce a state for every symbolic string length for better accuracy

Algorithm: Counts the number of characters in a string forking every time a symbolic byte is found that can be NULL but is not constrained to NULL.

Parameters

  • state – current program state

  • s – Address of string

Returns

Symbolic strlen result

manticore.native.models.strncpy(state: manticore.native.state.State, dst: Union[int, manticore.core.smtlib.expression.BitVec], src: Union[int, manticore.core.smtlib.expression.BitVec], n: Union[int, manticore.core.smtlib.expression.BitVec]) → Union[int, manticore.core.smtlib.expression.BitVec]

strncpy symbolic model

Algorithm: Copy n bytes from src to dst. If the length of the src string is less than n pad the difference with NULL bytes. If a symbolic byte is found that can be NULL but is not definitely NULL fork and concretize states.

Parameters

  • state – current program state

  • dst – destination string address

  • src – source string address

  • n – number of bytes to copy

Returns

pointer to the dst

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(*args, **kwargs)
add_hook(pc_or_sys: Optional[Union[int, str]], callback: Callable[[manticore.core.state.StateBase], None], after: bool = False, syscall: bool = False) → None

Add a callback to be invoked on executing a program counter (or syscall). Pass None for pc_or_sys to invoke callback on every instruction (or syscall invocation). callback should be a callable that takes one State argument.

Parameters

  • pc_or_sys (int or None if syscall = False. int, str, or None if syscall = True) – Address of instruction to hook, syscall number, or syscall name

  • callback – Hook function

  • after – Hook after PC (or after syscall) executes?

  • syscall – Catch a syscall invocation instead of instruction?

property 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

property mem

Current virtual memory mappings

remove_hook(pc_or_sys: Optional[Union[int, str]], callback: Callable[[manticore.core.state.StateBase], None], after: bool = False, syscall: bool = False) → bool

Remove a callback with the specified properties :param pc_or_sys: Address of instruction, syscall number, or syscall name to remove hook from :type pc_or_sys: int or None if syscall = False. int, str, or None if syscall = True :param callback: The callback function that was at the address (or syscall) :param after: Whether it was after instruction executed or not :param syscall: Catch a syscall invocation instead of instruction? :return: Whether it was removed

Cpu

class manticore.native.state.State(*args, **kwargs)
property cpu

Current cpu state

class manticore.native.cpu.abstractcpu.Cpu(regfile: manticore.native.cpu.abstractcpu.RegisterFile, memory: manticore.native.memory.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

property 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

property 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: int) → manticore.native.cpu.disasm.Instruction

This will decode an instruction from memory pointed by pc

Parameters

pc – 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

property icount
property instruction
property last_executed_insn: Optional[manticore.native.cpu.disasm.Instruction]

The last instruction that was executed.

property last_executed_pc: Optional[int]

The last PC that was executed.

property memory: manticore.native.memory.Memory
pop_bytes(nbytes: int, force: bool = False)

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

Parameters

  • nbytes – How many bytes to read

  • force – whether to ignore memory permissions

Returns

Data read from the stack

pop_int(force: bool = 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: bool = False)

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

Parameters

  • data – Data to write

  • force – whether to ignore memory permissions

push_int(value: int, force: bool = False)

Decrement the stack pointer and write value to the stack.

Parameters

  • value – The value to write

  • force – whether to ignore memory permissions

Returns

New stack pointer

read_bytes(where: int, size: int, force: bool = False, publish: bool = True)

Read from memory.

Parameters

  • where – address to read data from

  • size – number of bytes

  • force – whether to ignore memory permissions

  • publish – whether to publish events

Returns

data

read_int(where: int, size: Optional[int] = None, force: bool = False, publish: bool = True)

Reads int from memory

Parameters

  • where – address to read from

  • size – number of bits to read

  • force – whether to ignore memory permissions

  • publish – whether to publish an event

Returns

the value read

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: int, max_length: Optional[int] = None, force: bool = False) → str

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

Parameters

  • where – Address to read string from

  • max_length – The size in bytes to cap the string at, or None [default] for no limit.

  • force – whether to ignore memory permissions

Returns

string read

property regfile

The RegisterFile of this cpu

render_instruction(insn=None)
render_register(reg_name)
render_registers()
write_bytes(where: int, data, force: bool = False) → None

Write a concrete or symbolic (or mixed) buffer to memory

Parameters

  • where – address to write to

  • data – 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: int, string: str, max_length: Optional[int] = None, force: bool = False) → None

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

Parameters

  • where – Address to write the string to

  • string – The string to write to memory

  • max_length –

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(*args, **kwargs)
property mem

Current virtual memory mappings

class manticore.native.memory.SMemory(constraints: manticore.core.smtlib.constraints.ConstraintSet, 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: bool = False) → None

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(*args, **kwargs)
add_hook(pc_or_sys: Optional[Union[int, str]], callback: Callable[[manticore.core.state.StateBase], None], after: bool = False, syscall: bool = False) → None

Add a callback to be invoked on executing a program counter (or syscall). Pass None for pc_or_sys to invoke callback on every instruction (or syscall invocation). callback should be a callable that takes one State argument.

Parameters

  • pc_or_sys (int or None if syscall = False. int, str, or None if syscall = True) – Address of instruction to hook, syscall number, or syscall name

  • callback – Hook function

  • after – Hook after PC (or after syscall) executes?

  • syscall – Catch a syscall invocation instead of instruction?

property 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

property mem

Current virtual memory mappings

remove_hook(pc_or_sys: Optional[Union[int, str]], callback: Callable[[manticore.core.state.StateBase], None], after: bool = False, syscall: bool = False) → bool

Remove a callback with the specified properties :param pc_or_sys: Address of instruction, syscall number, or syscall name to remove hook from :type pc_or_sys: int or None if syscall = False. int, str, or None if syscall = True :param callback: The callback function that was at the address (or syscall) :param after: Whether it was after instruction executed or not :param syscall: Catch a syscall invocation instead of instruction? :return: Whether it was removed

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.