Introducing Ponce: One-click Symbolic Execution

In our previous post, we discussed concolic execution and how to use it to perform code coverage and find vulnerabilities in close source software. In this post, we’ll introduce the tools we use to find bugs in third-party software and present our latest innovation: Ponce, a simple IDA plugin to perform Symbolic Execution within your favorite debugging tool.

Athena — Poseidon

The RElabs vulnerability research team at Salesforce has developed a few internal tools that we use to perform fuzzing and find vulnerabilities in third-party software:

• Athena: This tool uses concolic execution to perform code coverage over user-controlled inputs. Multiplatform, works in Linux, OS X, and Windows. Relies on Triton for symbolic execution and DynamoRio as DBI. It’s a path explorer that discovers valid protocol templates (valid application inputs) without any knowledge of the audited binary. These valid inputs are later used by Poseidon to find crashes.
• Poseidon: This binary-focused guided fuzzing tool was coded from scratch by RElabs, using a structure similar to the open-source project Nightmare. Performs random modification on Athena’s generated templates, and counts the number of basic blocks executed by the modified template to follow deeper paths in the code.

The conjunction of these two tools is effective but requires considerable setup time. We have a visualization plugin to see the progress in IDA, but these are separate tools that do not have an easy and intuitive interface to be used within IDA.

Ponce, an open-source IDA plugin

Symbolic Execution is increasingly being discussed in security magazines and conferences. There are open source projects like Triton and Angr that allow you to use symbolic/concolic execution. However, these solutions are a very time-consuming to implement and have a rather steep learning curve.

To simplify this, we created Ponce, a C/C++ open-source IDA Pro plugin that implements symbolic execution and taint analysis within the most used disassembler/debugger for reverse engineers. The plugin is intuitive, easy to use, and easy to install, making symbolic execution and taint analysis just a click away!

Ponce currently works with IDA Pro on Windows for x86 and x64 binaries, but you can still debug Linux and Mac OS X binaries with Ponce using IDA’s built-in remote debugger. You could use the plugin in two modes:

• Taint analysis: this mode is used to understand and track where a user input occurs inside a program and where is it moved to.
• Symbolic analysis: in this mode, the plugin maintains a symbolic state of registers and memory at each step in a binary’s execution path, allowing the user to solve user-controlled conditions to do manually guided execution.

Both of them are integrated in IDA using its SDK to provide a great user experience while debugging your binary files.

How can Ponce help you?

There are multiple scenarios where this plugin could be helpful:

• Exploit development: Ponce can help you create an exploit in a far more efficient manner, as the exploit developer may easily see what parts of memory and which registers you control, as well as possible memory addresses which can be leveraged as ROP gadgets.
• Malware analysis: Analyzing the commands supported by a particular family of malware is easily determined by symbolizing a simple known command and negating all the conditions where the command is being checked.
• Protocol reversing: One of the most interesting uses of Ponce is the possibility of identifying required magic numbers, headers, or even entire protocols for controlled user input. For instance, Ponce can help you to list all of the accepted arguments for a given command line binary or extract the file format required for a specific file parser.
• CTF: Ponce speeds up the process of reverse engineer binaries during CTFs. As Ponce is totally integrated into IDA, you don’t need to worry about setup timing. It’s ready to be used!

How does it work?

In the previous post, we used the following code to show how Triton behaves with crackMe challenges:

char *serial = "\x31\x3e\x3d\x26\x31";
int check(char *ptr)
{
  int i = 0;
  while (i < 5){
    if (((ptr[i] - 1) ^ 0x55) != serial[i])
      return 1;
    i++;
  }
  return 0;
}

In this demo, we solve this crackMe with Ponce following the steps described:

• We select the symbolic engine and set the option to automatically symbolize argv.
• We identify the condition that must be satisfied to win the crackMe.
• We negate and inject the solution every time a byte of our input is checked against the key.
• Finally, we get the key elite that has been injected in memory and therefore reach the Win code.

Where can I find the code?

Ponce participated and won the IDA plugin contest 2016 and the code and documentation are hosted in Ponce’s GitHub repository. In the documentation, you’ll see other examples of following Ponce characteristics:

• Tracking the user input using the taint engine
• x64 support
• Multi-platform support from the IDA Pro Windows installation
• Runtime snapshot to speed up the manual code coverage

Future work

We are actively developing more Ponce features, so be on the lookout for these upcoming capabilities:

• Native support for MacOS and Linux flavors of IDA Pro
• Increased speed using the PIN tracer
• Automatically taint/symbolize all the possible user inputs, like file or socket reads.
• Implement some of the improvements we have already running in Athena, like symbolic index when reading/writing memory

(This post was originally published on 9–21–2016)