Magic with Manticore
Manticore is a next-generation binary analysis tool with a simple yet powerful API for symbolic execution, taint analysis, and instrumentation. Using Manticore one can identify ‘interesting’ code locations and deduce inputs that reach them. This can generate inputs for improved test coverage, or quickly lead execution to a vulnerability.
I used Manticore’s power to solve Magic, a challenge from this year’s DEFCON CTF qualifying round that consists of 200 unique binaries, each with a separate key. When the correct key is entered into each binary, it prints out a sum:
enter code: ==== The meds helped sum is 12
Reverse engineering 200 executables in order to extract strings one at a time takes a significant amount of time. This challenge necessitates automation. As CTFs feature more of these challenges, modern tools will be required to remain competitive.
We’ll be combining the powers of two such tools –Binary Ninja and Manticore– in three different solutions to showcase how you can apply them in your own work.
Challenge structure
The Magic binaries have a simple structure. There is a main function that prompts for the key, reads from stdin, runs the checker function, and then prints out the sum. The checker function loads bytes of the input string one at a time and calls a function to check each character. The character-checking functions do a comparison against a fixed character value. If it matches, the function returns a value to be summed, if it does not, the program exits.
Main, the checker function, and a single character checking function
Manticore’s API is very straight forward. We will use hooks to call functions when instructions are reached, the CPU class to access registers, and the solver. The workflow involves loading a binary by providing the path and adding analysis hooks on instructions in that binary. After that, you run Manticore. As the addresses are reached, your hooks are executed, and you can reason about the state of the program.
Functions defined as hooks take a single parameter: state. The state contains functionality to create symbolic values or buffers, solve for symbolic values, and abandon paths. It also contains a member, cpu, which holds the state of the registers, and allows the reading and writing of memory and registers.
Strategies
There are many ways to solve Magic. We’ll present three methods to demonstrate the flexibility of Manticore.
- A symbolic solution that hooks every instruction in order to discover where the character-checking functions are. When Manticore is at a character-checking function, it sets hooks to solve for the necessary value.
- A concrete solution that hooks the address of each character-checking function and simply reads the value from the opcodes.
- A symbolic solution that hooks the address of each character-checking function and solves for the value.
This is not an exhaustive list of the approaches you could take with Manticore. There is a saying, ‘there are many ways to skin a cat;’ Manticore is a cat-skinning machine.
Function addresses will be extracted using Binary Ninja. All strategies require an address for the terminating hook that prints out the solution. The latter two strategies need the addresses of the character-checking functions.
Address extraction with the Binary Ninja API
In order to extract the character-checking functions’ addresses, as well as the end_hook() address, we will be using Binary Ninja. Binary Ninja is a reverse engineering platform made for the fast-paced CTF environment. It’s user friendly and has powerful analysis features. We will use its API to locate the addresses we want. Loading the file in the Binary Ninja API is very straight forward.
bv = binja.BinaryViewType.get_view_of_file(path)
To reach the checker function, we first need the executable’s main function. We start by retrieving the entry block of the program’s entry function. We know the address of main is loaded in the 11th instruction of the LLIL. From that instruction we do a sanity check that it is a constant being loaded into RDI, then extract the constant (main’s address). Calling get_function_at() with main’s address gives the main function to be returned.
def get_main(bv):
entry_fn = bv.entry_function
entry_block = entry_fn.low_level_il.basic_blocks[0]
assign_rdi_main = entry_block[11]
rdi, main_const = assign_rdi_main.operands
if rdi != 'rdi' or main_const.operation != LLIL_CONST:
raise Exception('Instruction `rdi = main` not found.')
main_addr = main_const.operands[0]
main_fn = bv.get_function_at(main_addr)
return main_fn
The get_checker() function is similar to get_main(). It locates the address of the checker function which is called from main. Then it loads the function at that address and returns it.
1. Symbolic solution via opcode identification
Each character-checking function has identical instructions. This means we can examine the opcodes and use them as an indication of when we’ve reached a target function. We like this solution for situations in which we might not necessarily know where we need to set hooks but can identify when we’ve arrived.
- Set a hook on every instruction.
- Check if the opcodes match the first few instructions of the check functions.
- Set a hook on the positive branch to solve for the register value RDI and store the value.
- Set a hook on the negative branch to abandon that state.
- Set a hook at the pre-branch (current instruction) to check if we know the value that was solved for. If we know the value, set RDI so we do not need to solve for it again.
- Check if the opcodes match the first few instructions of the check functions.
- Set a hook at a terminating instruction.
The state.abandon() call on the negative branch is crucial. This stops Manticore from reasoning over that branch, which can take a while in more complex code. Without abandonment, you’re looking at a 3 hour solve; with it, 1 minute.
def symbolic(m, end_pc):
# hook every instruction using None as the address
@m.hook(None)
def hook_all(state):
# read an integer at the program counter
cpu = state.cpu
pc = cpu.PC
instruction = cpu.read_int(pc)
# check the instructions match
# cmp rdi, ??
# je +0xe
if (instruction & 0xFFFFFF == 0xff8348) and (instruction >> 32 & 0xFFFF == 0x0e74):
# the positive branch is 0x14 bytes from the beginning of the function
target = pc + 0x14
# if the target address is not seen yet
# add to list and declare solver hook
if target not in m.context['values']:
set_hooks(m, pc)
# set the end hook to terminate execution
end_hook(m, end_pc)
We’re using Manticore’s context here to store values. The context dictionary is actually the dictionary of a multiprocessing manager. When you start using multiple workers, you will need to use the context to share data between them.
The function set_hooks() will be reused in strategy 3: Symbolic solution via address hooking. It sets the pre-branch, positive-branch, and negative-branch hooks.
def set_hooks(m, pc):
# pre branch
@m.hook(pc)
def write(state):
_pc = state.cpu.PC
_target = _pc + 0x14
if _target in m.context['values']:
if debug:
print 'Writing %s at %s...' % (chr(m.context['values'][_target]), hex(_pc))
state.cpu.write_register('RDI', m.context['values'][_target])
# print state.cpu
# negative branch
neg = pc + 0x6
@m.hook(neg)
def bail(state):
if debug:
print 'Abandoning state at %s...' % hex(neg)
state.abandon()
# target branch
target = pc + 0x14
@m.hook(target)
def solve(state):
_cpu = state.cpu
_target = _cpu.PC
_pc = _target - 0x14
# skip solver step if known
if _target in m.context['values']:
return
val = _cpu.read_register('RDI')
solution = state.solve_one(val)
values = m.context['values']
values[_target] = solution
m.context['values'] = values
target_order = m.context['target_order']
target_order.append(_target)
m.context['target_order'] = target_order
if debug:
print 'Reached target %s. Current key: ' % (hex(_target))
print "'%s'" % ''.join([chr(m.context['values'][ea]) for ea in m.context['target_order']])
Note that there is a strange update pattern with the values dictionary and target_order array. They need to be reassigned to the context dictionary in order to notify the multiprocessing manager that they have changed.
The end_hook() function is used to declare a terminating point in all three strategies. It declares a hook after all the check-character functions. The hook prints out the characters discovered, then terminates Manticore.
def end_hook(m, end_pc):
@m.hook(end_pc)
def hook_end(state):
print 'GOAL:'
print "'%s'" % ''.join([chr(m.context['values'][ea]) for ea in m.context['target_order']])
m.terminate()
2. Concrete solution via address hooking
Since this challenge performs a simple equality check on each character, it is easy to extract the value. It would be more efficient to solve this statically. In fact, it can be solved with one hideous line of bash.
$ ls -d -1 /path/to/magic_dist/* | while read file; do echo -n "'"; grep -ao $'\x48\x83\xff.\x74\x0e' $file | while read line; do echo $line | head -c 4 | tail -c 1; done; echo "'"; done
However, in situations like this, we can take advantage of concretizing. When a value is written to a register, it is no longer symbolic. This causes the branch to be explicit and skips solving. This also means that the abandon hook on the negative branch is no longer necessary, since it will always take the positive branch due to the concrete value.
- Set a hook on each character-checking function.
- Extract the target value from the opcodes.
- Write that target value to the register RDI.
- Set a hook at a terminating instruction.
def concrete_pcs(m, pcs, end_pc):
# for each character checking function address
for pc in pcs:
@m.hook(pc)
def write(state):
# retrieve instruction bytes
_pc = state.cpu.PC
instruction = state.cpu.read_int(_pc)
# extract value from instruction
val = instruction >> 24 & 0xFF
# concretize RDI
state.cpu.write_register('RDI', val)
# store value for display at end_hook()
_target = _pc + 0x14
values = m.context['values']
values[_target] = val
m.context['values'] = values
target_order = m.context['target_order']
target_order.append(_target)
m.context['target_order'] = target_order
if debug:
print 'Reached target %s. Current key: ' % (hex(_pc))
print "'%s'" % ''.join([chr(m.context['values'][ea]) for ea in m.context['target_order']])
end_hook(m, end_pc)
3. Symbolic solution via address hooking
It is easy to extract the value from each function statically. However, if each character-checking function did some arbitrary bit math before comparing the result, we would not want to reimplement all of those instructions for a static extraction. This is where a hybrid approach would be useful. We identify target functions statically, and then solve for the value in each function.
- Set a hook on each character-checking function.
- Set a hook on the positive branch to solve for the register value RDI and store the value.
- Set a hook on the negative branch to abandon that state.
- Set a hook at the pre-branch (current instruction) to check if we know the value that was solved for.
- If we know the value, write it to RDI so we do not need to solve for it again.
- Set a hook at a terminating instruction.
def symbolic_pcs(m, pcs, end_pc):
for pc in pcs:
set_hooks(m, pc)
end_hook(m, end_pc)
Bringing everything together
With those three functions we have the target addresses we need. Putting everything together in main() we have a dynamic solver for the challenge Magic. You can find the full code listing here.
def main():
path = sys.argv[1]
m = Manticore(path)
m.context['values'] = {}
m.context['target_order'] = []
pcs, end_pc = get_pcs(path)
# symbolic(m, end_pc)
# concrete_pcs(m, pcs, end_pc)
symbolic_pcs(m, pcs, end_pc)
m.run()
A run with our debug print statements enabled will help show the execution of this script. The first time the positive branch is hit we see a Reached target [addr]. Current Key: statement and the key up to this point. Sometimes the negative branch will be taken and the state will be abandoned. We see Writing [chr] at [addr]… when we use our previously solved values to concretize the branch. Finally, when the end_hook() is hit we see GOAL: with our final key.
Start working smarter with Manticore
Manticore delivers symbolic execution over smaller portions of compiled code. It can very quickly discover the inputs required to reach a specific path. Combine the mechanical efficiency of symbolic execution with human intuition and enhance your capabilities. With a straightforward API and powerful features, Manticore is a must-have for anyone working in binary analysis.
Take the Manticore challenge
How about you give this a shot? We created a challenge very similar to Magic, but designed it so you can’t simply grep for the solution. Install Manticore, compile the challenge, and take a step into the future of binary analysis. Try it today! The first solution to the challenge that executes in under 5 minutes will receive a bounty from the Manticore team. (Hint: Use multiple workers and optimize.)
Thanks to @saelo for contributing the functionality required to run Magic with Manticore.