Multiple Styles: The Writeup
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
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
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
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 = True
The 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
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:
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.