Mobile application security researchers and pen testers alike rely on the Radare2 and Frida open-source tools for static analysis and code injection and are familiar with the R2frida plug-in that marries the two. A new OSS tool, ESILSolve, can simplify the process of reverse engineering complex mobile apps.
Learn about the many benefits of ESILSolve and how to harness symbolic execution in the below tutorial.
R2frida Background
R2frida is a plugin for Radare2 that combines the static analysis capabilities of Radare2 with the dynamic hooking and tracing capabilities of Frida.
R2frida reads and writes memory through Frida, using r2 for the disassembly and static analysis, while also providing Frida-specific commands to set hooks and trace code execution. Because R2frida is implemented as an IO plugin for R2, it reads and writes memory in the same manner as using R2 locally.
R2frida is great for working with locally running application, but is also designed specifically to work with mobile applications running on a connected Android or iOS device. Frida can instrument apps either through connection to Frida-server or by compiling or injecting Frida-gadget into the package. The ability to easily trace application behavior and patch code live with R2frida is what makes it incredibly powerful as a reverse engineering and security tool.
ESILSolve adds another capability to this already long list: Symbolic execution. Radare2 uses a simple IL created by NowSecure Researcher Pancake called Evaluable String Intermediate Language (ESIL). ESIL emulation powers some of the more advanced analysis features of r2 and is used to help define functions, search for cross-references, and provide useful annotations to the disassembly. ESILSolve is a symbolic execution engine for ESIL that uses the Z3 SMT solver to evaluate the generated abstract syntax trees. A more thorough exploration of the basics of ESILSolve can be found in my r2con 2020 presentation.
ESILSolve + R2frida: Even Better Together
The combination of R2frida and ESILSolve can be seen as a natural addition to the layers of abstraction of program state in r2. ESILSolve sits at the top, reading values through Radare2, which reads through Frida, which reads from the target’s real memory. An important thing to understand about ESILSolve is that though it uses R2 as its primary interface with the target program, it also has its own ESIL VM with independent memory and register states. This is similar to how R2 can have its own local representation of memory when iocache is on. ESILSolve registers are initialized from the values in R2 when a state is created, but after that they are manipulated completely separately.
Memory is handled slightly differently. When a memory read occurs ESILSolve first checks to see if there is already an internal representation of memory at the requested address, and if there is it will just use that. If not, ESILSolve will use R2pipe to read the concrete value from R2, storing it internally from then on. Writes will immediately add to the internal representation. Think of the ESILSolve states as another layer over the memory model of R2.
The power of this approach comes from the generality of Radare2 IO plugins. R2 provides the same API to read and write to memory regardless of whether the target is being opened statically, run locally or remotely in a debugger, or connected with R2frida. This allows ESILSolve to work (mostly) seamlessly with code from many different sources (check out examples/defcamp_r200 in the ESILSolve repo for a good example of ES+debugging). This means that it is easy to go from debugging a program to symbolically executing it once a certain breakpoint is hit or executing a mobile application on device until a Frida hook is reached.
ESILSolve’s approach offers many benefits to mobile application security researchers. We will explore a few.
- 1. Symbolic Execution Is Slow
The simplest advantage comes from the fact that symbolic execution engines execute code very slowly, even when all the data is concrete. ESILSolve is about as fast as angr (without unicorn), one of the faster dynamic symbolic execution frameworks, but that still isn’t great (to get comparable speeds to angr+unicorn one could similarly use ESILSolve+R2’s concrete ESIL emulation). Additionally it is often the case that the code one wishes to explore symbolically is a very small portion of the overall code that runs. Nothing is gained by having the symbolic engine execute other code when it is much faster to have it execute natively. - 2. Symbolic Execution Is Crappy
Symbolic execution engines also generally use representations of machine instructions that are incomplete or inaccurate in many ways. Whether it’s angr, manticore, miasm, or ESILSolve, the representation of instructions that are “executed” symbolically do not always capture all the complex possibilities of the real architecture. Additionally frameworks like angr use custom “Sim Procedures” to replace common library functions so they can run quicker and lead to less state explosion. These replacements may not always be faithful to the original code. Another big issue is IO and lower level code that is executed in the kernel or via IPC. Frameworks can gain considerable power by implementing replacements for these features as well, but they are complex and hard to get right. Similar power can be gained from hooking these parts of code where necessary, while letting the rest run normally on the hardware. ESILSolve has some ability to simulate common functions and simple filesystem operations. - 3. Mobile Apps Are Encrypted
On iOS, mobile apps are encrypted when they are downloaded through the Apple® App Store®. They need to be decrypted in order to perform any type of static analysis, including symbolic execution. While there are ways to do this off-device, it is much easier to just read the code at runtime. Attaching to an app with r2frida provides access to the decrypted code so that symbolic execution with ESILSolve works just as well as it does for code compiled locally from source.
ESILSolve + R2frida on iOS Apps
To demonstrate the capabilities of ESILSolve on iOS, we are going to target a CrackMe made by NowSecure Researcher Francesco. It is also included in the test/tests folder in the ESILSolve repo. The app has a single view with a text entry field and a nice big Validate button. We will use R2frida to investigate the app further. Attach to the running app with
r2 frida://attach/usb//iOSCrackme
Then we will seek to the address where iOSCrackMe is loaded using s `il` as it is the first address that comes up. Next, since the button says “Validate” a good first thing to check would be for symbols containing the word “validate”.
[0x100e18000]> is~validate
0x100e1d848 u -[ViewController validateTouched:]
0x100e1ddfc u validate
0x100e1d848 s -[ViewController validateTouched:]
0x100e1ddfc s validate
When this button is clicked the text in the field is passed as the only argument to the validate function which we can see in the validateTouched method as it contains
0x100e1d8f4 42010094 bl 0x100e1ddfc
We can seek to the validate function and decompile it with r2ghidra using pdgo which also shows us offsets, a surprise tool that will help us later.
Here I have renamed the returned value “result” with afvn result var_2ch. This makes it clearer that the failure condition is result == 0. It also shows that the argument string must be at least 16 bytes long and the target address we want to reach is 0x100e1e008. This is all the information we need to solve this CrackMe with ESILSolve!
This short Python program will output a valid serial number for the target CrackMe:
<br><br> from esilsolve import ESILSolver<br><br> import z3</p><br> <p># start the ESILSolver instance by attaching r2frida<br><br> esilsolver = ESILSolver("frida://attach/usb//iOSCrackMe")</p><br> <p>validate = esilsolver.r2api.get_address("validate")<br><br> # initialize state with context from hook, app is suspended<br><br> state = esilsolver.frida_state(validate)</p><br> <p># initialize symbolic bytes of solution<br><br> # and constrain them to be /[a-zA-Z]/<br><br> serial = z3.BitVec("serial", 16*8)<br><br> state.constrain_bytes(serial, "[a-zA-Z]")<br><br> addr = state.registers["x0"].as_long()<br><br> state.memory[addr] = serial</p><br> <p>state = esilsolver.run(validate+0x20c, avoid=[validate+0x218])<br><br> solution = state.evaluate_buffer(serial)<br><br> print("CODE: '%s'" % solution.decode())</p><br> <p># write solution into proper place<br><br> # esilsolver.r2api.write(addr, solution)<br><br> esilsolver.resume() # resume suspended app</p><br> <p>
The solution first imports ESILSolver and Z3. An esilsolver instance is created with the same URI that is used to launch R2frida normally. Sidenote: this is the case for all r2 URIs and ESILSolve. Next the address of validate is found and state = esilsolver.frida_state(validate) is used to set a Frida hook at that address and wait until it is hit. Enter anything you want into the box and press Validate.
The hook will be hit and frida_state will return an initialized ESILState with the exact state of the program when it reaches the hook. The app is then suspended so that symbolic execution can explore this state. Next the serial number — the text of the solution— is created as a symbolic z3 bitvector value. It is constrained to be upper or lowercase letters and it is 16 bytes long (16*8 bits). This is written into memory at the address in x0, which is the first argument of the function, overwriting whatever filler that was typed into the actual field.
The next line is the most important, it runs the symbolic execution from that initial state until it reaches the address validate+0x20c, which was 0x100e1e008 in our decompilation. It also avoids 0x100e1e014 which we saw set the result to 0, which is failure. This run(…) method returns the first state that reaches the target address. The solution can then be evaluated and printed! Then the app can be resumed with esilsolver.resume(). Optionally the commented out line can be used to set the argument address to the correct solution so that when the app is resumed the challenge is automatically solved as if the solution had been entered into the box!
This example demonstrates the core usefulness of ESILSolve + R2frida: the ability to seamlessly move from concrete execution to symbolic execution and back. Combined with the ability to easily patch the program on the fly, r2 can make complicated reversing tasks very easy to perform. The ESILSolve R2 plugin described next makes it even simpler — this video shows a demo of solving the CrackMe with the plugin.
Using the ESILSolve Plugin
The ESILSolve plugin is a core plugin for radare2 that implements a number of commands that perform the most common operations needed for symbolic execution. This includes initialization of states, setting of symbolic values, and constraining those values in different ways. The available commands can be listed with aesx? or X?
Using the plugin with R2frida is almost exactly the same as with a statically loaded file, but with the added ability to easily initialize a state when a Frida hook has been hit. This is accomplished by seeking to the desired code address and using aesxif (or Xif if the shortcuts are enabled). This places a hook at the address and blocks until this hook is hit (this is important in the context of using this feature in a script, I may add a non-blocking version otherwise). Once the hook is hit, an ESILSolve state is initialized with the register state of the hooked thread. This thread is then suspended until the user runs Xfc which continues the execution. The associated frida JS for this hook is very simple:
Interceptor.attach(ptr('0x%x'),function(){send(this.context);recv('continue',function(){}).wait()})
We suspend the thread (using .wait) to prevent continued execution from changing any memory values that ESILSolve uses while the symbolic execution runs. Remember that ESILSolve is only a layer over the existing memory, and it does not necessarily contain its own copies for every address.
Using ESILSolve with Android
ESILSolve also works on Android apps, and can even be run directly on unrooted Android devices using Termux. There is only one problem: ESILSolve has (very) limited support for DEX. It may get better support through the P-Code translation functionality (using the pcode=True option). For right now, and probably forever, it is easier to run ESILSolve on native instructions. Luckily modern Android provides a way to easily translate DEX code into native code: dex2oat. Dex2oat compiles dex files into odex and vdex files. The .odex files are simply ELF binaries and can have helpful debugging symbols added in by passing -g to dex2oat. Additionally you can set dex2oat to compile everything, not just methods that would typically be targeted. Conveniently both of these can be done systemwide by running
setprop dalvik.vm.dex2oat-flags -g
setprop dalvik.vm.dex2oat-filter everything
Depending on what Android version you use, this may need to be executed as root. Apps installed subsequently will have symbols in the generated odex files which will allow us to easily find the code we want to symbolically execute. In this case we are going to install a very simple CrackMe I wrote which is similar to the previous one, at least visually. In reality it can be solved easily without symex but we will ignore that for demonstration purposes here.
The flag for this CrackMe is a hex number. We begin by attaching to the app with r2frida as before and navigating to the odex module using
s `il~odex`
If there is no odex you can run adb shell pm compile -m everything com.nowsecure.escrackme (Or replace the app name with whatever your target is) and relaunch the app. We can find the validation method similarly to before by searching the symbols in this module for the term “check” using
is~check
The correct method is the last one com.nowsecure.escrackme.MainActivity.check(long). After seeking to this address we can run af; pdf to display the function.
Again the failure condition can be seen here as returning zero in w0. Initialize the ESILSolve state with Xi (use Xif to initialize the state once a hook has been hit). Set x2 to be a 8 byte symbolic value named flag with Xs x2 flag 8 and run until the instruction before the second ret with
Xr 0x7407a18a1c 0x7407a189c4
The second address tells ESILSolve to avoid the nop after the first failure check. Finally the value in w0 is then constrained to be 1 and the flag is evaluated. Converting to hex reveals that it is 0xcafebabe. (This video shows the whole process.)
Conclusion
R2frida + ESILSolve empower users to automate certain mobile application security tasks. The combination is based on the flexible features of Radare2 and Frida which drive NowSecure products and provides a great addition to the NowSecure toolset of mobile appsec testing solutions.
To learn more about mobile application security and our research, contact us to speak to an expert.
