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
-
classmethod
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
(byte, constrs) → 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
(byte, constrs) → 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.
is_definitely_NULL
(byte, constrs) → 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.
isvariadic
(model)¶ Parameters: model (callable) – Function model Returns: Whether model models a variadic function Return type: bool
-
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 (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
(state: manticore.native.state.State, s: Union[int, manticore.core.smtlib.expression.BitVec]) → Union[int, manticore.core.smtlib.expression.BitVec]¶ 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 – Address of string
Returns: Symbolic strlen result
Return type: Expression or int
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: 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
-
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: int)¶ 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
-
icount
¶
-
instruction
¶
-
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)¶ Read from memory.
Parameters: - where – address to read data from
- size – 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: 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
-
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
(constraints, platform, **kwargs) -
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
(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.