[DevCTF-2022] Android SoDifficult

Problem Statement

Problem Name: soDifficult
Apk Link: https://anonfiles.com/rfn2zch9y6/app-universal-release_apk

Setting Up

As the name of the problem suggests, we have to do something with the .so file(s) (Obviously decompile it). For this we will use ApkLab as mentioned in editorials to previous questions, along with open source Ghidra or IDA. For this tutorial I have used ghidra as it is open-source and completely free.

First Things First

1. Launch the App. We need to enter some password🤔. Lets check the source code.
2. Decompile the apk using ApkLab and open the project.
3. Go through the AndroidManifest.xml file. Launch Activity class is com.ctf.rev.MainActivity.
4. Browse through the MainActivity Class. You should find a reference to the native checkPassword3 function call. So we need to try and identify this function in the the .so files located in lib folder. Here I will decompile lib/x86/libnative-lib.so file using ghidra.

Main App Screen

Decompiling the so file

First fire up the Ghidra using ghidraRun (or ghidraRun.bat if on windows). Create a new project. Import the .so file to decompile. Now double click on it, and if prompted to analyze, press Yes. Now the file should be decompiled.
In the left side of the app, you should see ‘Symbol Tree’ Panel. Expand the functions entry and navigate to the checkPassword3function. Well this looks like a very complicated code!

Code Snippet of decompiled function

Understanding the C Code

If we can understand the c code, we would know for what value the function returns True. This might be the flag or some hint to it!

Looking at the code, we see that variable __s stores the passed string(param3). Its length is stored in variable in sVar2 and its length should be 20 (0x14) for the conditions to be true. In the next 60 lines, various conditions on characters of string is being checked. These are some integer equations, all of which need to be satisfied. One can try and solve this manually, which would take a hell lot of time! Or we can treat this as a satisfiability problem, and use some library to solve this.

Solving the Satisfiability Equations

In this problem I will use the Z3-Solver by microsoft in python. You can install it using:

pip install z3-solver

Next in the python code we first need to initialize the variables and add constraint equations to solver as mentioned in the decompiled c code. Here is the python code for reference:

Running the code returns this gets us the flag!

Output: ctf{k1nG_0f_R3v3r5e}