CTF Toulouse Hacking Conference - 2018

THC-2018 CTF

First contact

After downloading the APK from the github repository we fire up android studio and the emulator. We install the APK by dragging it into the emulator interface and launch the app.

The application consists of a text field where we can enter a serial and a button “Activate Software” to supposedly activate the software from the given serial.

If we try a random serial a pop up appears asking us to enter a valid serial.

Static analysis with JADX

We start our reverse engineering with a static analysis of the application. We use JADX to do this.

We can see that there aren’t a lot of classes :

• BuildConfig
• MainActivity
• PremiumActivity

From the manifest, we can see that the class MainActivity is started from the launcher :

        <activity android:name="com.thc.bestpig.serial.MainActivity">
            <intent-filter>
                <action android:name="android.intent.action.MAIN"/>
                <category android:name="android.intent.category.LAUNCHER"/>
            </intent-filter>
        </activity>

The MainActivity contains a method called validateSerial :

    public boolean validateSerial(String serial) {
        if (serial.length() == 19
        && serial.charAt(4) == '-'
        && serial.charAt(9) == '-'
        && serial.charAt(14) == '-'
        && serial.charAt(5) == serial.charAt(6) + 1
        && serial.charAt(5) == serial.charAt(18)
        && serial.charAt(1) == (serial.charAt(18) % 4) * 22
        && ((serial.charAt(3) * serial.charAt(15)) / serial.charAt(17)) - 1 == serial.charAt(10)
        && serial.charAt(10) == serial.charAt(1)
        && serial.charAt(13) == serial.charAt(10) + 5
        && serial.charAt(10) == serial.charAt(5) - 9
        && (serial.charAt(0) % serial.charAt(7)) * serial.charAt(11) == 1440
        && (serial.charAt(2) - serial.charAt(8)) + serial.charAt(12) == serial.charAt(10) - 9
        && (serial.charAt(3) + serial.charAt(12)) / 2 == serial.charAt(16)
        && (serial.charAt(0) - serial.charAt(2)) + serial.charAt(3) == serial.charAt(12) + 15
        && serial.charAt(3) == serial.charAt(13)
        && serial.charAt(16) == serial.charAt(0)
        && serial.charAt(7) + 1 == serial.charAt(2)
        && serial.charAt(15) + 1 == serial.charAt(11)
        && serial.charAt(11) + 3 == serial.charAt(17)
        && serial.charAt(7) + 20 == serial.charAt(6)) {
            return true;
        }
        return false;
    }

Cracking the serial the hard way

Getting the first letter

From the validateSerial function we have the following system of equations where x0 is serial.charAt(0) and so on :

A) x5 = x6 + 1
B) x5 = x18
C) x1 = (x18 % 4) * 22
D) ((x3 * x15) / x17) - 1 = x10
E) x10 = x1
F) x13 = x10 + 5
G) x10 = x5 - 9
H) (x0 % x7) * x11 = 1440
I) (x2 - x8) + x12 = x10 - 9
J) (x3 + x12) / 2 = x16
K) (x0 - x2) + x3 = x12 + 15
L) x3 = x13
M) x16 = x0
N) x7 + 1 = x2
O) x15 + 1 = x11
P) x11 + 3 = x17
Q) x7 + 20 = x6

After some substitions we get the following inequality

x5 - 9 = (x5 mod 4) * 22

Since x5 - 9 = (x5 mod 4) * 22, we know that there is an integer k such that :

x5 - 9 = (4k + x5) * 22

From there we now have an equation for x5 :

x5 = - (88k + 9)/21

Since x5 must be an integer we create a small kotlin script to test multiple possibilities for k and return the ones where x5 is an integer :

fun main() {
    for (k in 0..100) {
        var res = (88.0*k+9.0)/21.0
        if (res.roundToInt().toDouble() == res) {
            println("k = $k => x5 = " + (88.0 * k + 9.0) / 21.0)
        }
    }
}

We get the following possibilities, so we assume we know x5 for now :

k = 3 => x5 = 13.0
k = 24 => x5 = 101.0
k = 45 => x5 = 189.0
k = 66 => x5 = 277.0
k = 87 => x5 = 365.0

We have now use this knowledge to solve the system of equations and express every variable with x5 :

x0 = x5 - 3
x1 = x5 - 9
x2 = x5 - 20
x3 = x5 - 4
x6 = x5 - 1
x7 = x5 - 21
x8 = x5 - 4
x10 = x5 - 9
x12 = x5 - 2
x13 = x5 - 4
x16 = x5 - 3

Working with integers

You might have noticed that x11, x15 and x17 are missing. If you tried to solve the system of equations without taking into account equation H) you might get something like:

x11 = x5 - 7
x15 = x5 - 8
x17 = x5 - 4

The problem is that these value are incorrect and do not work with the equation D), you will get something like 16 = 64 which is obviously false.

The reason for that is that to find x11, x15 and x17 you will use the following set of equations :

D) ((x3 * x15) / x17) - 1 = x10
O) x15 + 1 = x11
P) x11 + 3 = x17

When you get to this point, you already know how to express x3 and x10 from x5 so it should look like this :

D)  ((x5 - 4) * x15) / x17 = x5 - 8
O) x15 + 1 = x11
P) x11 + 3 = x17

When you try to solve this set of equations the usual way, you might fail to take into account that you are working with integers and integer division. This means that when you perform a division, you are rounding up the result to get an integer.

Now if we perform some substitutions we can get this equation:

D) (x17 - 4) / x17 = (x5 - 8) / (x5 - 4)

Since we are performing integer division we have :

(x17 - 4) / x17 = 0
(x5 - 8)  / (x5 - 4) = 0

So this equation is really saying 0 = 0 if we try to apply divisions.

Finding x11, x15 and x17

To find the remaining letters we have to use equation H)

H) (x0 % x7) * x11 = 1440

From this equation we know that there is a k (different from the previous one) such that:

1440 = (x0 + k*x7) * x11

If I replace x0 and x7 by their values expressed from x5, and if I prettify the equation I can get x11 from x5 and k :

x11 = 1440 / (x5*(1+k) - 21*k - 3)

Now I can create a function to compute the different possibilities for x11 from x5:

fun findx11(x5 : Int) {
    for (k in -100..100) {
        val x11 = 1440.0 / (x5*(1+k) - 21*k - 3.0 )
        if (x11 == x11.toInt().toDouble()) {
            println("k = $k ; x11 = $x11")
        }
    }
}

When I have found the correct x11 I will be able to deduce x15 and x17.

Tying it altogether

I am not finished yet here. I could finish manually by a process of trial and error but I still have equation D) that I did not apply as a constraint. I will use it to help me find the proper x5 and the proper x11.

D) ((x3 * x15) / x17) - 1 = x10

If I remodel the equation to express it from x11 and x5 here is what I get:

(x5 - 4) * (x11 - 1) / (x11 + 3) = (x5 - 8)

Since I have only guesses for x5 and x11, I have to use this equation to validate the pair that satisfies all the constraints.

Here is the final code used to crack the serial:

import kotlin.math.roundToInt

fun main() {
    guessX5().forEach {x5 ->
        guessX11(x5).forEach {x11 ->
            if((x5 - 4) * (x11 - 1) / (x11 + 3) == (x5 - 8)) {
                println(computeSerial(x5, x11))
            }
        }
    }
}

fun guessX5() : List<Int> {
    val list = mutableListOf<Int>()
    for (k in -100..100) {
        var guess = -(88.0*k+9.0)/21.0
        if (guess.isInt()) {
            list.add(guess.toInt())
        }
    }
    return list
}


fun guessX11(x5 : Int) : List<Int> {
    val list = mutableListOf<Int>()
    for (k in -100..100) {
        val guess = 1440.0 / (x5*(1+k) - 21*k - 3.0 )
        if (guess.isInt()) {
            list.add(guess.toInt())
        }
    }
    return list
}

fun Double.isInt() : Boolean {
    return this.roundToInt().toDouble() == this
}

fun computeSerial(x5: Int, x11: Int) : String {
    val x = Array(19, init = {0})
    x[0] = x5 - 3
    x[1] = x5 - 9
    x[2] = x5 - 20
    x[3] = x5 - 4
    x[4] = 45
    x[5] = x5
    x[6] = x5 - 1
    x[7] = x5 - 21
    x[8] = x5 - 5
    x[9] = 45
    x[10] = x5 - 9
    x[11] = x11
    x[12] = x5 - 2
    x[13] = x5 - 4
    x[14] = 45
    x[15] = x11 - 1
    x[16] = x5 - 3
    x[17] = x11 + 3
    x[18] = x5
    return x.joinToString("") { i -> i.toChar().toString() }
}

The serial is HB7G-KJ6F-BPIG-OHSK.