github

illera88 / Ponce

  • воскресенье, 25 сентября 2016 г. в 03:17:59
https://github.com/illera88/Ponce

C++
Symbolic Execution just one-click away!



Ponce

Definition

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++.

Why?

Symbolic execution is not a new concept in the security community. It has been around for years but it is not until the last couple of years 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.

Installation

Ponce works with both x86 and x64 binaries. Installing the plugin is as simple as copying Ponce.plw and Ponce.p64 to the plugins\ folder in your IDA installation directory.

OS Support

Ponce currently works with IDA Pro on Windows for x86 and x64 binaries.

You can still debug Linux and Mac OS X binaries with Ponce using IDA's built-in remote debugger.

Ponce v0.2 will build native plugins for IDA Linux and IDA Mac OS X. Actually the code we wrote already takes these architectures into consideration using macros for the different operating systems.

Use cases

  • 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 addresses which can be leveraged as ROP gadgets.
  • Malware Analysis: Another use of Ponce is related to malware code. Analyzing the commands a particular family of malware supports 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 Ponce uses is the possibility of recognizing required magic numbers, headers or even entire protocols for controlled user input. For instance, Ponce can help you to list all 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!

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.

Use modes

  • Tainting engine: This engine is used to determine at every step of the binary's execution which parts of memory and registers are controllable by the user input.
  • Symbolic engine: This engine maintains a symbolic state of registers and part of memory at each step in a binary's execution path.

Examples

Use symbolic execution to solve a crackMe

Here we can see the use of the symbolic engine and how we can solve constrains:

  • Passing simple aaaaa as argument.
  • We first select the symbolic engine.
  • We convert to symbolic the memory pointed by argv1
  • Identify the symbolic condition that make us win and solve it.
  • Test the solution.

manual_symbolize_and_solve_crackme_hash2 The crackme source code can be found here

Negate and inject a condition

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:

  • We select the symbolic engine and set the option to symbolize argv.
  • We identify the condition that needs to be satisfied to win the crackMe.
  • We negate an inject the solution everytime 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.

crackmexor_negate_and_inject The crackme source code can be found here

Using the tainting engine to track user controlled input

In this example we can see the use of the tainting engine with cmake. We are:

  • Passing a file as argument to cmake to have him parsing it.
  • We select we want to use the tainting engine
  • We taint the buffer that fread()` reads from the file.
  • We resume the execution under the debugger control to see where the taint input is moved to.
  • Ponce will rename the tainted functions. These are the functions that somehow the user has influence on, not the simply executed functions.

cmake_tainting_fread

Use Negate, Inject & Restore

In the next example we are using the snapshot engine:

  • Passing a file as argument.
  • We select we want to use the symbolic engine.
  • We taint the buffer that fread()` reads from the file.
  • We create a snapshot in the function that parses the buffer read from the file.
  • When a condition is evaluated we negate it, inject the solution in memory and restore the snapshot with it.
  • The solution will be "valid" so we will satisfy the existent conditions.

fread_test_negate_restore_inject The example source code can be found here

Usage

In this section we will list the different Ponce options as well as keyboard shortcuts:

  • Access the configuration and taint/symbolic windows: Edit > Ponce > Show Config (Ctl+Shift+P and Ctl+Alt+T)

2016-09-15 11_39_08-configuracion

  • Enable/Disable Ponce tracing (Ctl+Shift+E)

2016-09-15 11_31_34-

  • Symbolize/taint a register (Ctl+Shift+R)

2016-09-15 11_32_32-

  • Symbolize/taint memory. Can be done from the IDA View or the Hex View (Ctl+Shift+M)

2016-09-15 11_32_52-ida - testproject idb testproject exe c__users_default default-pc_documents_vi2016-09-15 11_33_10-taint _ symbolize memory range

2016-09-15 12_09_11-inicio

  • Solve formula (Ctl+Shift+S)

2016-09-15 11_35_11-

  • Negate & Inject (Ctl+Shift+N)

2016-09-15 11_34_44-

  • Negate, Inject & Restore Snaphot (Ctl+Shift+I)

2016-09-15 11_47_19-

  • Create Execution Snapshot (Ctl+Shift+C)

2016-09-15 11_37_40-

  • Restore Execution Snapshot (Ctl+Shift+S)

2016-09-15 11_38_10-

  • Delete Execution Snapshot (Ctl+Shift+D)

2016-09-15 11_38_23-

  • Execute Native (Ctl+Shift+F9)

2016-09-15 12_07_10-

Triton

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! :)

Building

We provide compiled binaries for Ponce, but if you want to build your own plugin you can do so using Visual Studio 2013. We tried to make the building process as easy as possible:

  • Clone the project with submodules: git clone --recursive https://github.com/illera88/PonceProject.git
  • Open Build\PonceBuild\Ponce.sln: The project configuration is ready to use the includes and libraries shipped with the project that reside in external-libs\.
  • The VS project has a Post-Build Event that will move the created binary plugin to the IDA plugin folder for you. copy /Y $(TargetPath) "C:\Program Files (x86)\IDA 6.9\plugins". NOTE: use your IDA installation path.

The project has 4 build configurations:

  • x86ReleaseStatic: will create the 32 bits version statically linking every third party library into a whole large plugin file.
  • x86ReleaseZ3dyn: will create the 32 bits version statically linking every third party library but z3.lib.
  • x64ReleaseStatic: will create the 64 bits version statically linking every third party library into a whole large plugin file.
  • x64ReleaseZ3dyn: will create the 64 bits version statically linking every third party library but z3.lib.

The static version of z3.lib is ~ 1.1Gb and the linking time is considerable. That's the main reason why we have a building version that uses z3 dynamically (as a dll). If you are using z3 dynamically don't forget to copy the libz3.dll file into the IDA's directory.

FAQ

Why the name of Ponce?

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.

Can Ponce be used to analyze Windows, OS X and Linux binaries?

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.

How many instructions per second can handle Ponce?

In our tests we reach to process 3000 instructions per second. We plan to use the PIN tracer IDA offers to increase the speed.

Something is not working!

Open an issue, we will solve it ASAP ;)

I love your project! Can I collaborate?

Sure! Please do pull requests and work in the opened issues. We will pay you in beers for help ;)

Limitations

Symbolic execution has some inherent 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.

Authors