The following is a writeup of the challenge 'multiple-styles' from the manticore wiki.
If we were to run the command manticore multiple-styles, manticore would begin an automatic analysis of the binary, and would eventually figure out the necessary inputs to reach any code path. However, as this can take an exceptionally long time (depending on the complexity of the binary), we will do some manual analysis of the binary in order to speed things up. Below is an annotated disassembly of the main function, produced by Binary Ninja.
First off, towards the bottom, we can see two blocks that each print a string, then exit. One prints "Sounds fake but ok", the other prints "You got it!". Presumably, the former indicates failure, while the latter indicates success.
In the first block, we can see that instructions 0x4009d1 to 0x4009e7 read 17 bytes from stdin into a buffer starting at an offset of 0x50 bytes from the base pointer.
Near the end of the first block, we can see that instructions 0x4009ec to 0x400a08 push 17 bytes into a buffer starting at an offset of 0x30 bytes from the base pointer. It's likely that these correspond to our flag, but a quick test reveals that just passing them to stdin doesn't produce a solution. Nonetheless, I've labeled the beginning of this buffer as flag_lower in the disassembly.
The next few blocks seem to perform a modified string comparison. Most importantly, we can see that the block starting at 0x400a17 loads a byte from the input buffer (rbp - 0x50), adds 10 to it, then compares it with a byte from flag_lower. If the comparison fails, it immediately falls through to the failure block. If the two bytes match, it continues the loop, until eventually jumping to the success block.
From here, we've got all the information we need to solve this challenge. Clearly, at instruction 0x400a3b, all we need to do is subtract 10 from the byte from flag_lower to get the correct value we need to pass to stdin. The following Manticore script accomplishes that:
from manticore import Manticore
m = Manticore('./multiple-styles')
m.context['flag'] = ""
@m.hook(0x400a3b)
def hook(state):
cpu = state.cpu
m.context['flag'] += chr(cpu.AL - 10)
@m.hook(0x400a3e)
def hook2(state):
cpu = state.cpu
cpu.ZF = True
@m.hook(0x400a40)
def hookf(state):
print("Failed")
m.terminate()
@m.hook(0x400a6c)
def hooks(state):
print("Success!")
print(m.context['flag'])
m.terminate()
m.concrete_data = "12345678" * 2 + "\n"
m.run()First off, we load the Manticore module, then load the multiple-styles binary.
from manticore import Manticore
m = Manticore('./multiple-styles')Next, we create a flag entry in the manticore context dictionary. This will give us a place to store the flag that we can access between the different hooks.
m.context['flag'] = ""Now, we'll create some hooks. A hook is not unlike a debugger breakpoint - it tells manticore to pause the program just before executing the instruction at a given address, run some code of ours, then continue executing.
We define a hook using the @m.hook(<address>) decorator, which tells manticore that the following function should be run as a hook when the instruction at <address> is reached. This first hook fires before the compare instruction at the end of the block which compares the stored flag to the shifted input. From looking at the disassembly, we can see that at this point, the value of the flag is stored in the lowest byte of eax (AL). The final line of this hook grabs this value, subtracts ten from it to undo the transformation from instruction 0x400a27, then appends the resulting character to the flag entry in the context dictionary.
@m.hook(0x400a3b)
def hook(state):
cpu = state.cpu
m.context['flag'] += chr(cpu.AL - 10)The second hook fires just before the jump instruction at the end of this block. All it does is set the zero flag to true so that regardless of whether the values in memory matched, we will always jump back to the beginning of the loop. Strictly speaking, we could have avoided the need for this hook by copying the value in AL into the memory it is compared with in the previous step.
@m.hook(0x400a3e)
def hook2(state):
cpu = state.cpu
cpu.ZF = TrueThe final two hooks simply print out the flag (assuming success) and kill the program. While it's not entirely necessary to add hooks for both the success and failure conditions, it does aid debugging in more complex challenges.
@m.hook(0x400a40)
def hookf(state):
print("Failed")
m.terminate()
@m.hook(0x400a6c)
def hooks(state):
print("Success!")
print(m.context['flag'])
m.terminate()Finally, we set m.concrete_data to 17 filler bytes (which has the effect of passing these bytes to stdin) and tell manticore to begin running the program. Eventually, our success hook fires and prints the flag.
m.concrete_data = "12345678" * 2 + "\n"
m.run()Ideally, we'd rather not have to figure out how to calculate the value to pass to stdin ourselves. While it was easy enough to reverse the transformation on the input bytes here, most real-world challenges will not be so trivial. Fortunately, thanks to manticore's symbolic execution capabilities, we can get it to do this for us.
from manticore import Manticore
m = Manticore('./multiple-styles')
m.context['flag'] = ""
@m.hook(0x400a6c)
def hook(state):
cpu = state.cpu
transform_base = cpu.RBP - 0x50
for i in range(17):
solved = state.solve_one(cpu.read_int(transform_base + i, 8))
print(solved)
m.context['flag'] += chr(solved)
print(m.context['flag'])
m.terminate()
m.run()You'll notice that the address where we place our hook is 0x400a6c, the same place we put the success hook in the previous example. Essentially, this solution marks a destination address for manticore, then helps it figure out how to get there.
From our analysis of the binary, you may remember that it reads the values from stdin into a buffer starting at RBP - 0x50. We'll save this address in a variable called transform_base.
We'll then iterate over the bytes in the buffer starting at transform_base and for each byte, tell manticore to solve for a value of this byte that allows us to reach the current address. Once we've found a value, we append it to the flag entry in the context dictionary.
When we're all done, we print this entry and kill the program. After letting this solver run for about 60 seconds, it prints out the flag: coldlikeminisodas.
Having seen the previous, entirely concrete solution, this example may seem confusing. There, we used manticore like a programmable debugger, modifying the loop so that it would never fail. However, here we only needed to hook the success condition. Why? Manticore doesn't really execute the program so much as it explores the states it's possible for the program to reach. The instruction where our hook is marks the success state for Manticore, and the state.solve_one operation uses z3 to solve the constraints established by examining the rest of the program in order to figure out the values that need to go in the memory at transform_base + i to allow us to arrive at the current state.
I've updated the code to support
manticore==0.3.1. I'm not sure if using global values is ok tho.