By Alan Chang, University of Oxford

During my summer internship, I had the wonderful opportunity to work on the Manticore User Interface (MUI). The MUI project aims to combine the strength of both Manticore, a powerful symbolic execution library, and Binary Ninja, a popular binary analysis tool, to provide a more intuitive and visual interface for working with symbolic execution.

A gentle introduction to symbolic execution

When conducting vulnerability research and reverse engineering, researchers often wish to thoroughly test a piece of software and explore all its possible states. Symbolic execution is one method that can address this matter. As shown in the following code snippet, the program execution can go into either the if case or the else case.

To test this code with a concrete input for x (e.g., x = 4), only one of the two states will be reached during execution. This means multiple runs of the program will be necessary to fully explore the state space. However, if we consider x to be symbolic, similar to the notion of a variable in mathematics, both states can be explored simultaneously, and we just have to keep track of the constraints on our symbolic variables at each point of the exploration process.

Specifically in this example, the if-else statement will create two states, one with the constraint x < 5 exploring ① and another with x ≥ 5 exploring ②. This is the key concept behind symbolic execution, which can help us figure out whether a given code segment is reachable and what input would be necessary.

The problem of state explosion

The symbolic execution technique, however, is not without its drawbacks. Notably, there’s the issue of state explosion. When there are many conditional branches and loops in a program, the number of states that need to be explored can grow exponentially. It can quickly become infeasible to explore them all. The example below illustrates this point. With just three loop iterations, the code snippet will end up with eight states to explore, and this number rapidly explodes as the iteration increments.

This issue of state explosion is further exacerbated by the fact that most symbolic execution libraries lack a method of visualizing the state exploration process. That means that it’s often difficult to even pinpoint where state explosions occur, let alone to begin fixing them.

The MUI project aims to address these issues by providing an interactive user interface to better visualize this state exploration process in symbolic execution and to keep the human in the loop. More specifically, the MUI is a Binary Ninja plugin with custom Qt widgets that provide a visual and intuitive interface to interact with Manticore, the open-source symbolic execution library developed by Trail of Bits.

MUI features and demonstration

To illustrate some of the MUI features, let’s try and solve a simple crackme challenge inside the Manticore repository. The objective is straightforward: we need to determine the correct input for this program.

First attempt: Using the find and avoid commands

Opening the ELF binary in Binary Ninja, we can quickly spot the two puts calls in the main function. These two function calls are used for the success and failure cases, respectively. Now, our objective can be rephrased as finding an input so that the code execution reaches the success case.

We can convey this objective to the MUI using the find command; the instruction is highlighted with green. Similarly, we can tell the MUI to avoid the failure case using the avoid command.

Now, with an objective specified, we can run the MUI to find the solution to this crackme challenge.

As shown in the gif, we can use Manticore to explore the state space of the challenge within the Binary Ninja UI, and we obtain the solution coldlikeminisodas. Giving this answer back to the program verifies that we have indeed solved the challenge.

Turning our attention back to the MUI, we can use the custom State List widget to see the way the MUI got to this solution and all the states that it explored. State 34 in the list denotes the final state in which we reached the success case.

To further visualize the relation between each of the states, we can use the Graph View widget. This widget shows a provenance tree containing all the states. Double-clicking on a state node will bring us to the last instruction before the state was forked or terminated. Using the tab shortcut, the tree graph can be expanded to show other terminated states.

A second solution: Custom hooks

In addition to all the cool features that we have already demonstrated, the MUI still has more tricks up its sleeves. Let’s solve this challenge again using a different method.

If we spend some time understanding the decompiled code, we can see that our user input is compared against the correct answer one character at a time, and when one character of our input does not match the correct answer, we see the failure message. With this knowledge, we can prevent all state forking by explicitly telling the MUI which path we want to take. This can be achieved with a custom hook and the code snippet below:

global bv,m,addr
def hook(state):
   flag_byte = state.cpu.AL - 0xa
 
   with m.locked_context() as context:
       if 'solution' in context:
           context["solution"] += chr(flag_byte)
       else:
           context["solution"] = chr(flag_byte)
       print(f'flag: {context["solution"]}')
 
   state.cpu.RIP = 0x400a51
m.hook(addr)(hook)

The custom hook feature here is a kind of fallback that gives you the full power of the Manticore API without having to write a complete script in a different environment. This allows researchers to do everything inside of Binary Ninja and reduce the amount of context switching required.

How about EVM?

Manticore is well known for its support for smart contracts, and the MUI plugin also offers basic EVM support. Documentation can be found in the project README file.

To get around the lack of built-in EVM support in Binary Ninja, the MUI leverages a few other open-source tools developed by Trail of Bits. Smart contracts are compiled using crytic-compile, an abstraction layer for smart contract build systems, and the generation and visualization of disassembly code and CFGs is handled by ethersplay, an EVM disassembler.

With these tools, the EVM feature set in the MUI is now on par with the default Manticore CLI, and more features are under active development. But even with the same features, the MUI really outshines the CLI tool in its usability and discoverability. Instead of looking through documentation to find the right command-line argument, users can now see all the available Manticore run options and pick the ones they need using a dynamically generated and up-to-date UI panel. Furthermore, the tight integration with Binary Ninja also means that these options can be persistently saved inside Binary Ninja Database (BNDB) project files, offering more convenience.

Conclusions

I’m really proud of what I was able to achieve with the MUI project during my internship. The MUI is already available for many use cases for researchers to improve their workflow. We have achieved what we set out to do with this project: to provide an intuitive and visual interface for working with symbolic execution.

This internship has been a great learning opportunity for me. Through this internship, I gained a deeper understanding of how symbolic execution works and learned about a lot of different topics ranging from project planning and documentation to Qt UI development, from multi-threaded applications to the Git workflow, and much more.

I would like to thank my mentors, Eric Kilmer and Sonya Schriner, for their tremendous help during my internship. Both of them provided me with guidance when I needed it but also gave me enough freedom to explore and innovate during the development of the MUI. My internship experience would not have been the same without them. I’m truly grateful for this internship opportunity at Trail of Bits, and I cannot wait to see what the future brings for the MUI project.