# [CTF THCON18] Write-Up - Reverse: android (200 points)
## Description
Le challenge contenait un apk nommé « THC.apk ». Le texte qui l'accompagnait disait qu'il fallait trouver le serial pour activer l'application. N'ayant pas sous la main un émulateur android, je me suis lancé directement dans sa décompilation.
## Décompilation de l'application
Un APK est une simple archive zip que l'on peut extraire:
```> unzip -d THC THC.apk...> ls THCAndroidManifest.xml  classes.dex  META-INF  res  resources.ars```
Il contient les fichiers classiques d'une application Android. Le bytecode java est dans le *classes.dex*. L'outil **dex2jar** permet de le convertir au format *jar*. En quelques mots, le *jar* est le format historique pour stocker le bytecode java, mais Android préfère le format *dex* qui est optimisé pour les mobiles.
L'application **jd-gui** est très pratique pour décompiler les **.jar*.
```> dex2jar classes.dexdex2jar classes.dex -> ./classes-dex2jar.jar> jd-gui classes-dex2jar.jar```
## Analyse du code
Dans l'interface, on voit immédiatement un package nommé *com.thc.bestpig.serial* qui contient un fichier *MainActivity.class*. Les activités sont au coeur des interfaces utilisateurs sous Android. Ouvrons-le:
```javapackage com.thc.bestpig.serial;
import android.annotation.TargetApi;import android.content.DialogInterface;import android.content.DialogInterface.OnClickListener;import android.content.Intent;import android.os.Bundle;import android.support.v7.app.ActionBar;import android.support.v7.app.AlertDialog.Builder;import android.support.v7.app.AppCompatActivity;import android.text.InputFilter;import android.text.InputFilter.AllCaps;import android.text.InputFilter.LengthFilter;import android.view.View;import android.view.View.OnClickListener;import android.widget.Button;import android.widget.EditText;
public class MainActivity  extends AppCompatActivity{  protected boolean checkPassword(String paramString)  {    if (validateSerial(paramString))    {      new AlertDialog.Builder(this).setTitle("Well done ;)").setMessage("You can now validate this challenge.\n\nThe flag is the serial").setCancelable(false).setNeutralButton("Ok", new DialogInterface.OnClickListener()      {        public void onClick(DialogInterface paramAnonymousDialogInterface, int paramAnonymousInt)        {          paramAnonymousDialogInterface = new Intent(MainActivity.this.getApplicationContext(), PremiumActivity.class);          MainActivity.this.startActivity(paramAnonymousDialogInterface);        }      }).show();      return true;    }    new AlertDialog.Builder(this).setTitle("Premium activation failed").setMessage("Please don't try random serial, buy a legit premium license to support developers.").setCancelable(false).setNeutralButton("Ok", new DialogInterface.OnClickListener()    {      public void onClick(DialogInterface paramAnonymousDialogInterface, int paramAnonymousInt) {}    }).show();    return false;  }
  @TargetApi(21)  protected void onCreate(final Bundle paramBundle)  {    super.onCreate(paramBundle);    setContentView(2131296283);    getSupportActionBar().setDisplayShowHomeEnabled(true);    getSupportActionBar().setLogo(2131361792);    getSupportActionBar().setDisplayUseLogoEnabled(true);    paramBundle = (EditText)findViewById(2131165286);    paramBundle.setFilters(new InputFilter[] { new InputFilter.AllCaps(), new InputFilter.LengthFilter(19) });    ((Button)findViewById(2131165219)).setOnClickListener(new View.OnClickListener()    {      public void onClick(View paramAnonymousView)      {        MainActivity.this.checkPassword(paramBundle.getText().toString());      }    });  }
  protected boolean validateSerial(String paramString)  {    if (paramString.length() != 19) {}    while ((paramString.charAt(4) != '-') || (paramString.charAt(9) != '-') || (paramString.charAt(14) != '-') || (paramString.charAt(5) != paramString.charAt(6) + '\001') || (paramString.charAt(5) != paramString.charAt(18)) || (paramString.charAt(1) != paramString.charAt(18) % '\004' * 22) || (paramString.charAt(3) * paramString.charAt(15) / paramString.charAt(17) - 1 != paramString.charAt(10)) || (paramString.charAt(10) != paramString.charAt(1)) || (paramString.charAt(13) != paramString.charAt(10) + '\005') || (paramString.charAt(10) != paramString.charAt(5) - '\t') || (paramString.charAt(0) % paramString.charAt(7) * paramString.charAt(11) != 1440) || (paramString.charAt(2) - paramString.charAt(8) + paramString.charAt(12) != paramString.charAt(10) - '\t') || ((paramString.charAt(3) + paramString.charAt(12)) / 2 != paramString.charAt(16)) || (paramString.charAt(0) - paramString.charAt(2) + paramString.charAt(3) != paramString.charAt(12) + '\017') || (paramString.charAt(3) != paramString.charAt(13)) || (paramString.charAt(16) != paramString.charAt(0)) || (paramString.charAt(7) + '\001' != paramString.charAt(2)) || (paramString.charAt(15) + '\001' != paramString.charAt(11)) || (paramString.charAt(11) + '\003' != paramString.charAt(17)) || (paramString.charAt(7) + '\024' != paramString.charAt(6))) {      return false;    }    return true;  }}```
Il y a deux fonctions qui sautent aux yeux: **checkPassword()** et **validateSerial()**. Le **checkPassword()** appelle la fonction de validation du serial et affiche success en disant que le flag est le serial lui-même.
La fonction **validateSerial()** est très simple. Elle teste une série de conditions entre les 20 caractères du serial. On est sur un cas typique où il suffit de satisfaire toutes les contraintes entre les caractères pour trouver la valeur de chacun d'eux. Ce type de problème se résout à l'aide d'un solveur SAT.
## Trouver le serial avec z3
La librarie z3 a un solveur SAT très pratique. La définition des variables et des contraintes se fait naturellement en Python:
```python#!/usr/bin/env python
from z3 import *import os
solver = Solver()
# Define the serial charactersc0 = Int('c0')c1 = Int('c1')c2 = Int('c2')c3 = Int('c3')c4 = Int('c4')c5 = Int('c5')c6 = Int('c6')c7 = Int('c7')c8 = Int('c8')c9 = Int('c9')c10 = Int('c10')c11 = Int('c11')c12 = Int('c12')c13 = Int('c13')c14 = Int('c14')c15 = Int('c15')c16 = Int('c16')c17 = Int('c17')c18 = Int('c18')c19 = Int('c19')
# Define the possible values for each characters,# from ' ' and '~' (printable chars).solver.add((c0 >= 0x20, c0 <=0x7e))solver.add((c1 >= 0x20, c1 <=0x7e))solver.add((c2 >= 0x20, c2 <=0x7e))solver.add((c3 >= 0x20, c3 <=0x7e))solver.add((c4 >= 0x20, c4 <=0x7e))solver.add((c5 >= 0x20, c5 <=0x7e))solver.add((c6 >= 0x20, c6 <=0x7e))solver.add((c7 >= 0x20, c7 <=0x7e))solver.add((c8 >= 0x20, c8 <=0x7e))solver.add((c9 >= 0x20, c9 <=0x7e))solver.add((c10 >= 0x20, c10 <=0x7e))solver.add((c11 >= 0x20, c11 <=0x7e))solver.add((c12 >= 0x20, c12 <=0x7e))solver.add((c13 >= 0x20, c13 <=0x7e))solver.add((c14 >= 0x20, c14 <=0x7e))solver.add((c15 >= 0x20, c15 <=0x7e))solver.add((c16 >= 0x20, c16 <=0x7e))solver.add((c17 >= 0x20, c17 <=0x7e))solver.add((c18 >= 0x20, c18 <=0x7e))solver.add((c19 >= 0x20, c19 <=0x7e))
# Define the constraints that have been# founded in MainActivity.class.solver.add(c4 == 45)solver.add(c9 == 45)solver.add(c14 == 45)solver.add(c5 == (c6 + 1))solver.add(c5 == c18)solver.add(c1 == c18 % 4 * 22)solver.add(c10 == c3 * c15 / c17 - 1)solver.add(c10 == c1)solver.add(c13 == c10 + 5)solver.add(c10 == c5 - 9)solver.add(c0 % c7 * c11 == 1440)solver.add(c2 - c8 + c12 == c10 - 9)solver.add((c3 + c12) / 2 == c16)solver.add(c0 - c2 + c3 == c12 + 15)solver.add(c3 == c13)solver.add(c16 == c0)solver.add(c7 + 1 == c2)solver.add(c15 + 1 == c11)solver.add(c11 + 3 == c17)solver.add(c7 + 20 == c6)
# Check() returns true if there is a solution# and model() the values founded.if solver.check():	print(solver.model())else:	print('Not found.')```
On lance le script...
```> python2 solver.py[k!3 = 18, c17 = 83, c19 = 33, k!7 = 1, c8 = 71, c12 = 73, c2 = 55, c15 = 79, c11 = 80, c1 = 66, c18 = 75, c5 = 75, c6 = 74, c7 = 54, c16 = 72, c0 = 72, c3 = 71, c13 = 71, c10 = 66, c14 = 45, c9 = 45, c4 = 45]```
Une fois les caractères dans l'ordre et le decimal converti en ascii, on obtient le serial:
```HB7G-KJ6G-BPIG-OHSK!```Merci aux organisateurs !
By team Beers4Flags
``` ________|        ||  #BFF  ||________|   _.._,_|,_  (      |   )   ]~,"-.-~~[ .=] Beers ([ | ])  4   ([ '=]) Flags [   |:: '    |    ~~----~~```