[DevCTF-2022] Android SoDifficult
Problem Name: soDifficult
Apk Link: https://anonfiles.com/rfn2zch9y6/app-universal-release_apk
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
- Launch the App. We need to enter some password🤔. Lets check the source code.
- Decompile the apk using ApkLab and open the project.
- Go through the AndroidManifest.xml file. Launch Activity class is
- Browse through the MainActivity Class. You should find a reference to the native
checkPassword3function call. So we need to try and identify this function in the the .so files located in
libfolder. Here I will decompile
lib/x86/libnative-lib.sofile using ghidra.
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!
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!