IDA 2016 plugin contest winner! Symbolic Execution just one-click away!
OTHER License
Ponce (pronounced [ 'poN θe ] pon-they ) is an IDA Pro plugin that provides users the ability to perform taint analysis and symbolic execution over binaries in an easy and intuitive fashion. With Ponce you are one click away from getting all the power from cutting edge symbolic execution. Entirely written in C/C++.
Symbolic execution is not a new concept in the security community. It has been around for many years but it is not until around 2015 that open source projects like Triton and Angr have been created to address this need. Despite the availability of these projects, end users are often left to implement specific use cases themselves.
We addressed these needs by creating Ponce, an IDA plugin that implements symbolic execution and taint analysis within the most used disassembler/debugger for reverse engineers.
Ponce works with both x86 and x64 binaries in any IDA version >= 7.0. Installing the plugin is as simple as copying the appropiate files from the latest builds to the plugins\
folder in your IDA installation directory.
Make sure you use the Ponce binary compiled for your IDA version to avoid any incompatibilities.
Ponce works on Windows, Linux and OSX natively!
The plugin will automatically run, guiding you through the initial configuration the first time it is run. The configuration will be saved to a configuration file so you won't have to worry about the config window again.
In the next gif we can see the use of automatic tainting and how we can negate a condition and inject it in memory while debugging:
argv
.elite
that has been injected in memory and therefore reach the Win
code.The crackme source code can be found here
In this example we can see the use of the tainting engine with cmake. We are:
In the next example we are using the snapshot engine:
The example source code can be found here
In this section we will list the different Ponce options as well as keyboard shortcuts:
Ponce relies on the Triton framework to provide semantics, taint analysis and symbolic execution. Triton is an awesome Open Source project sponsored by Quarkslab and maintained mainly by Jonathan Salwan with a rich library. We would like to thank and endorse Jonathan's work with Triton. You rock! :)
Since Ponce v0.3 we have moved the building compilation process to use CMake
. Doing this we unify the way that configuration and building happens for Linux, Windows and OSX. We now support providing feedback on the pseudocode about symbolic or taint instructions. For this feature to work you need to add hexrays.hpp
to your IDA SDK include folder. hexrays.hpp
can be found on plugins/hexrays_sdk/
on your IDA installation path. If you have not purchased the hex-rays decompiler you can still build Pnce by using -DBUILD_HEXRAYS_SUPPORT=OFF
. We use Github actions as our CI environment. Check the action files if you want to understand how the building process happens.
Juan Ponce de León (1474 – July 1521) was a Spanish explorer and conquistador. He discovered Florida in the United States. The IDA plugin will help you discover, explore and hopefully conquer the different paths in a binary.
Yes, you can natively use Ponce in IDA for Windows or remotely attach to a Linux or OS X box and use it. In the next Ponce version we will natively support Ponce for Linux and OS X IDA versions.
In our tests we reach to process 3000 instructions per second. We plan to use the PIN tracer IDA offers to increase the speed.
Open an issue, we will solve it ASAP ;)
Sure! Please do pull requests and work in the opened issues. We will pay you in beers for help ;)
Concolic execution and Ponce have some problems:
Symbolic memory load/write: When the index used to read a memory value is symbolic like in x = aray[symbolic_index]
some problems arise that could lead on the loose of track of the tainted/symbolized user controled input.
Triton doesn't work very well with floating point instructions.
Concolic execution only analyzed the executed instructions. That means that symbolic tracking is lost in cases like the following:
int check(char myinput) // Input is symbolic/tainted
{
int flag = 0;
if (myinput == 'A') //This condition is symbolic/tainted
flag = 1
else
flag =- 1;
return flag; // flag is not symbolic/tainted!
}