Introduction
For Defcon Quals 2019, I wrote a challenge called VeryAndroidoso.
It is an Android crackme, written using both Java and native code.
Many teams solved this challenge using reverse engineering and Frida.
However, I designed it so that it could also be solved using angr.
In fact, angr now has some experimental support for symbolic execution of Java and Android apps (including apps using a combination of Dalvik bytecode and native C/C++ code).
The code of my solution using angr is available in the angr-doc repository.
A few notes
To run correctly, the solution script needed a small fix to angr.
This fix adds support for the cmp Soot bytecode expression.
To avoid potentially leaking information about the challenge, the fix was pushed and merged to the angr repository only after the end of the competition.
I think that a team who wanted to use angr to solve this challenge could have quite easily figured out how to fix this issue.
A more subtle issue is the following Exception from CLE:
...
File "/home/antoniob/git/angr_pypy/angr-dev/cle/cle/backends/externs/__init__.py", line 112, in allocate
raise CLEOperationError("Ran out of room in the extern object...! Report this as a bug.")
cle.errors.CLEOperationError: Ran out of room in the extern object...! Report this as a bug.
My understanding is that this happens due to a bug on how the JNI interface is implemented. The linked solution contains a workaround for this issue:
# extern_size=0x800000 prevents CLE bug
project = angr.Project(apk_location, main_opts=loading_opts, extern_size=0x800000)
My solution provides good examples of how to:
- load a mixed Java/native Android app,
- specify Java “addresses” (different code locations),
- run symbolic execution starting from a specific Java code location and having specific symbolic values,
- run symbolic execution until a condition is met, pruning failed paths,
- write SimProcedures re-defining Java methods,
- read and write values from the symbolic Java memory.
My solve.py script runs in about one hour using pypy.
It does not stop immediately after a solution is found since it explores all paths.
For this reason, it takes more time to finish than what strictly necessary, but I could use it to double check that this challenge had a single solution.
