By Calvin Fong

During my internship at Trail of Bits, I explored the effectiveness of symbolic execution for finding vulnerabilities in native applications ranging from CTF challenges to popular open source libraries like image parsers, focusing on finding ways to enhance ManticoreUI. It is a powerful tool that improves accessibility to symbolic execution and vulnerability discovery, but its usability and efficiency leave much room for improvement. By the end, I implemented new ManticoreUI features that reduce analysis time through emulation, improved shared library support, and enabled symbolic state bootstrapping from GDB to side-step complex program initialization. With these new features, I found and reported a vulnerability in the DICOM Toolkit (DCTMK), which is a widely deployed set of libraries used in medical imaging!

The current state of ManticoreUI

Manticore is a symbolic execution engine that emulates applications with symbolic data, as opposed to concrete data. This allows Manticore to test all possible execution paths of its targets. ManticoreUI (MUI) is a graphical user interface plug-in for Binary Ninja that exposes the features of Manticore to users in a simpler way with helpful graphical elements. Its design allows users to reap the benefits of symbolic execution without having to worry about the nitty-gritty of the Manticore API.

One of my goals was to improve MUI’s user experience for finding vulnerabilities. I spent some time using MUI in CTF challenges, on artificially created vulnerable code samples, and on some small real-world targets. From this, I determined three general directions for improvement:

• I realized that many non-default features were not obvious to new or inexperienced Manticore users. These features were sometimes implemented in code but not covered in the documentation.
• I also noticed that real-world software targets were significantly more challenging to approach than smaller samples like CTF challenges. CTF challenges tend to be small command-line applications that typically receive input from standard input. However, there are many application types in the real world, including network services, daemons, and libraries. And the MUI user experience was very different for each type.
• Lastly, when testing software that processes large inputs, like format parsers with big iterating loops or complex C++ binaries, MUI’s emulation was obviously much slower than the execution speed of a real CPU.

Exposing useful features through ManticoreUI

To address the first improvement area, I made two of MUI’s useful features—function models and global hooks—more obvious to users.

Function models

Function models are Python re-implementations of common library functions with awareness of Manticore’s symbolic execution engine. These models override actual library functions during symbolic execution. This improves performance because Manticore does not have to emulate each native instruction individually.

ManticoreUI now prompts when there are library functions that could be substituted with an existing function model implementation, as shown below:

The Add Function Model command allows users to add a custom hook at the function address to use the function model instead of native code.

Global Hooks

Global hooks are another less obvious functionality. These are custom hooks that are triggered for every instruction that gets executed. They can be useful for implementing user-defined tracing functionality, like tracing every syscall that occurs (similar to strace). Alternatively, they can help with performing checks not bound to specific instructions (e.g., a global hook that ends the Manticore run when the RAX register has the value 0xdeadbeef). They can be added using the Add/Edit Global Hook command.

Improving the workflow for bug discovery

To address the second and third improvement areas, I implemented new MUI features that facilitate the bug discovery process. The emulate_until feature increases the performance of MUI, while shared library support and gdb state dumping improved MUI’s usability in complex targets. These features are described in greater depth below.

emulate_until

The emulate_until feature is an additional MUI solve option. Setting this value to an address will make Manticore use the Unicorn emulator to concretely emulate your target binary until it reaches the address specified. The Unicorn emulator is far faster than Manticore’s own emulated CPU, which greatly improves execution speed.

I noticed this feature was very useful for C++ binaries, which execute more instructions during initialization. When we symbolically executed a simple benchmark with a hello world C++ binary on an Ubuntu 20.04 machine, we observed the following run times:

	Default	emulate_until to main
Total Duration /s	311 seconds	12 seconds

Evidently, using Unicorn emulation with the emulate_until option causes significant performance benefits for even the simplest C++ binaries.

Shared library support

In vulnerability discovery, we commonly test underlying libraries of an application rather than a full application itself. Such workflows usually involve a simple harness binary that loads the library and calls library functions to be tested. Since MUI supported loading and setting hooks in only a single binary, the use of a harness binary with the shared library was a troublesome workflow for MUI.

With this new feature, users can separately load the shared library in MUI and set up all necessary hooks. Then, they can load the harness binary in MUI and link the Binary Ninja project file of the shared library. During execution, all hooks set in the shared library’s project will be resolved and added to the runtime accordingly.

While not yet implemented, this feature would be well suited for the Ghidra MUI Plugin. Binary Ninja projects contain only single binaries, while Ghidra projects can contain multiple binaries. This feature would enable a more convenient workflow for vulnerability discovery in Ghidra.

GDB state dumping

I ran into various issues while testing MUI with different targets, including unsupported system calls, unimplemented instructions, and applications that were too complicated to interact with through MUI/Manticore. I also frequently encountered situations where testing the entire application symbolically would lead to state explosion (i.e., too many forked states).

This led me to begin exploring the idea of limiting the use of Manticore’s execution engine. For example, rather than trying to symbolically execute from the start of the application, what about starting execution from a function of interest? This would still be very helpful when looking for vulnerabilities within a small subset of functions, and it reduces emulation issues by limiting the amount of code that Manticore has to symbolically execute.

I developed a GDB plugin for GEF that allows the user to dump the debugger’s state as a Manticore state object. This is stored in a file on the system that can later be loaded into MUI/Manticore to be used as the initial state of execution. This plugin dramatically increases the possibilities for MUI!

For example, network services that were usually hard to fully emulate in Manticore can now be run normally and attached to a debugger. Users can then dump the state from a breakpoint of choice and load that state into MUI to begin symbolic execution. This process allows MUI to be used with all sorts of complex targets.

This method has similarities with two other techniques: under-constrained symbolic execution and concolic execution. However, it is certainly the most “constrained” of the three methods. This is not necessarily a bad thing, but users must exercise judgment to determine which technique best suits their use case. One key weakness in using states from GDB is that injecting symbolic values requires a greater understanding of the current program state. For instance, if you replaced a variable value with a totally unconstrained symbolic value because you did not analyze certain if-else checks earlier in the program, Manticore may give inaccurate results.

Finding a vulnerability with the help of MUI

With MUI in my arsenal, I was determined to find a vulnerability while using the power of symbolic execution. My goal was not to find a vulnerability entirely through symbolic execution. Instead, I hoped to use MUI/Manticore as an oracle that could inform me about reachability and execution constraints, complementing traditional bug hunting methodologies like source auditing.

The codebase I targeted was the DICOM ToolKit (DCTMK). DCMTK is a set of libraries and utilities for working with the DICOM standard. Because DICOM files are usually used for medical imaging, DCMTK is used in software that handles medical products or data.

Rapidly assessing reachability with Manticore

I began by examining the source code with a focus on certain vulnerability sinks like memory accesses or memory allocations. When I discovered sinks that could lead to a vulnerability, I then relied on MUI to determine if the target code was reachable and if conditions for memory corruption could be created.

While reading the code for parsing BMP images, I noticed the following vulnerability sink:

// dcmdata\libi2d\i2dbmps.cc:330 
OFCondition I2DBmpSource::readBitmapData( 
  const Uint16 width, 
  const Uint16 height, 
  const Uint16 bpp, 
  const OFBool is TopDown, 
  const OFBool isMonochrome, 
  const Uint16 colors, 
  const Uint32* palette,
  char * & pixData, 
  Uint32& length) 
{
  …
  Uint8 *row_data; 
  …
  Uint16 samplesPerPixel = isMonochrome ? 1 : 3; 
  …
  length = width * height * samplesPerPixel;     // [1]
  …
  pixData = new char [length];                   // [2]
}

At [1] we see that the length variable is set to the product of width, height, and samplesPerPixel. This length is then used as the size to allocate a char buffer at [2]. This is a common sink for integer overflow vulnerabilities. If the product of width, height, and samplesPerPixel is sufficiently unbounded to overflow the capacity of length, it could make the allocation at [2] too small.

Since width and height are user-controlled, I wanted to determine if the user could provide any combination of values that would lead to an integer overflow. This is where MUI came into play! I used MUI as an oracle to determine if there could be an integer overflow of length, given the bounds of width, height, and samplesPerPixel.

A quick look through the code revealed that samplesPerPixel was maximally set to 3 for colored images. Additionally, width and height were limited to the range of unsigned 16-bit integers:

 if (tmp_height <= 0 || tmp_height > OFstatic_cast (Sint 32, UINT16_MAX)) 
   return makeOFCondition (OFM_dcmdata, 18, OF_error, "Unsupported BMP file - height too
large or zero"); 
 ...
 if (tmp_width <= 0 || tmp_width > OFstatic_cast (Sint 32, UINT16_MAX)) 
   return makeOFCondition (OFM_dcmdata, 18, OF_error, "Unsupported BMP file - width too
large or zero"); 

Using the GDB state dumping plugin, I set a breakpoint on the I2DBitmapSource::readBitmapData function and reached the breakpoint with a simple BMP image of a snail. By dumping the debuggee environment into a Manticore state, I could then load the state into MUI. The following video demonstrates this process:

With the state loaded in MUI, I could set the width and height to symbolic values. Using custom hooks, I forced Manticore to solve for a state where the integer overflow occurs. Manticore would use a sat-solver to determine if such a state was possible, allowing us to thoroughly verify the validity of this bug.

After running, I got the following values:

This meant that a crafted BMP image with the width and heights specified in the above image could create a situation where length was too small, causing an undersized allocation. Running the binary in GDB with this exploit image immediately led to a crash and a successful bug discovery!

Patch

Within a few hours of informing the vendors, they introduced a patch to fix the vulnerability. This was a very pleasant security response!

A successful revamp

I’m very happy with the progress I’ve made over the course of this internship, and I think the improved analysis performance, support for shared libraries, and side-step complex application initialization with GDB have molded ManticoreUI into a better tool for aiding vulnerability discovery that nicely complements traditional bug hunting methodologies.

Through this internship, I’ve learned a lot about the applications of symbolic execution in the security field, and I’m excited to see how it will continue to develop. Beyond symbolic execution, I had the opportunity to improve my skills in software development through working on the different components of ManticoreUI.

I’m very grateful for the help my mentor, Eric Kilmer, provided throughout the internship. He gave me guidance for the direction of the project and invaluable feedback to improve on the code and ideas I contributed. This internship was surely a memorable and fruitful experience for me.