Getting Started Native

The basics

The following is the simplest possible Manticore script to analyze a native binary:

from manticore.native import Manticore

m = Manticore("./path_to_binary")

m.run()

Platforms

The basic operations you can perform on a manticore.native.manticore.Manticore object are as follows

Hook decorator @m.hook()

@m.hook(breakpoint_addr)
def name(state):
	...

The hook decorator is a wrapper around m.add_hook(breakpoint_addr, callback) and will setup you decorated function as the callback. This is equivalent to a breakpoint in something like gdb.

State

States are forked whenever a binary can split into two different paths, through some sort of conditional instruction.

The state object allows the user to introspec into the current registers and memory at the given PC value similar to a breakpoint in a debugger like gdb.

To look at the current value stored in a register you should do

def name(state)
	print(hex(state.cpu.RAX))
	# you can also just print state.cpu to get a good look at the majority of registers
	print(state.cpu)

cpu

You can also look at memory with

def name(state)
	# will print out all of the memory mappings
	print(state.mem)

	print(state.cpu.read_int(memory_addr))

	# you can also read a specific amount of bytes with
	print(state.cpu.read_bytes(memory_addr, size))

	# to read raw bytes without triggering events with
	print(state.mem.read(memory_addr, num_bytes))
	# returns a list of bytes

	# you can also read c style strings
	print(state.cpu.read_string(state.cpu.RAX))

mem

Most of the time you will want to use state.cpu to read memory as it auto converts to big endian, which is probably what you want for most analysis in python.

Note: cpu based memory accesses will call read_int which causes a memread event which may not be desired by the user.

Note: Memory access will throw an exception under various scenarios like if the memory you are trying to read from is not mapped, you can catch this with a try except block. If it is a permission issue you can pass force=True to force a read.

Storing information

If you need to store information between states you should use m.locked_context().

with m.locked_context() as context:
	context["thing"] = "hello"

This provides a mutex like interface to a shared dict/list.

However if you would like for certain information to be kept on a state by state basis you can do

def name(state):
	state.context["trace"] = state.cpu.PC

This information will be kept only in this state and copied to both states if it forks.

Guiding execution

To help speed up execution and limit path explosion you can help manticore figure out good paths

A big issue for symbolic execution is path explosion and if you can limit that it will exponentially help.

for(int i = 0; i < 200; i++){
	if(input != i){
		goto bad;
	}
}
print("Correct password")
...
exit(0)

bad:
print("Incorrect password")
...
exit(1)

Path explosion occurs because every time you hit the if statement manticore forks the state into 2 more states. This leads to 2**200 states and will probably destroy your computers resources before it gets close to exploring all of them. However if you could tell manticore which of the two states is correct it will become essentially 200 states

This can be done via state.abandon() and you can stop manticore early with m.kill()

@m.hook(bad_addr)
def name(state):
	# tell manticore that this state should not be explored
	state.abandon()

...
@m.hook(win_addr)
def name(state):
	...
	# figure out what you need from binary
	...
	# stop running the binary if you dont need manticore to anymore
	m.kill()

Working with symbolic values

Symbolic values track what constraints a value needs for all the conditionals to get you to this location.

The default example for something like a ctf is user input is morphed/weakly hashed by a function and then compared to a value like this example.

Symbolic values store an expression that could be solved by an smt solver like Microsoft's z3. This will return valid values that could be used to reach that branch.

To generate a new symbolic buffer

def name(state):
	# generate a symbolic object
	symbolic = state.new_symbolic_buffer(num_bytes)

	# write it to a memory address
	state.cpu.write_bytes(buffer_addr, symbolic)

When you want to solve these values you can either access all symbolic values with state.generate_testcase("testcase_name") and it will solve all symbolic values and put them in the mcore_* folder in the .input file.

If you still have a reference to them like if you stored them in a context you can solve them individually with

def name(state):
	symbolic = state.context["value"]
	print(state.solve_one(symbolic))
	# or solve with many
	print(state.solve_n(symbolic, n))

You can also access all symbolic values with state.input_symbols

def name(state):
	for i in state.symbolic:
		if i.name == "STDIN":
			# symbolic stdin buffer
		if i.name == "ARGVX": # X being the arguement number
			# symbolic argv[X] buffer
		else:
			# likely a buffer you defined

You can add symbolic files with .add_symbolic_file however this should be done during Manticore.init because of the introduction of multiprocessing.

Be careful with symbolic files their support at this time is limited.

Function models