Mastering Reverse Engineering with Z3 SMT Solver

By Luis Almaraz aka lehag
@lehag07

Descripción

Este reto fue presentado durante el CTF de TokyoWesterns 2019 donde participé junto con mi equipo Mayas. La única descripción que nos daba el reto es la siguiente: “Cracking is easy for you”. Existen distintas formas de resolver un crack me, sin embargo, en esta entrada se expone cómo es que conseguimos resolver el reto con ayuda del teorema conocido como Z3 [1].

Solución

Identificando el archivo easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f

1. Abrimos una terminal en donde se encuentra nuestro archivo.

user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$ 

2. Vemos los archivos del directorio actual.

user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$ ls -l
total 16
-rw-r--r-- 1 user user 10312 Aug 30 20:05 easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f
-rw-r--r-- 1 user user  3139 Aug 30 20:11 easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f.zip
user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$

3. Obtenemos la suma MD5 del archivo llamado easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f para conocer su integridad.

user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$ md5sum easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f
e63a34dc0be8a91437935a38e38b150a  easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f
user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$ 

4. Determinamos el tipo de archivo llamado easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f.

user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$ file easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f
easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 3.2.0, BuildID[sha1]=7e80b79602fcfd8121e9f4d9d26bb01a81f4afe5, stripped
user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$

Es un programa de tipo ELF de 64 bits cuyos símbolos de debuggeo han sido eliminados.

5. Visualizamos las cadenas del programa easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f para conocer algún tipo de hint que nos pueda servir más adelante. 

user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$  strings easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f
[snipped]
user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$

Hay algunas cadenas interesantes:
  1. ./bin flag_is_here 
  2. Incorrect 
  3. TWCTF{ 
  4. Correct: %s

Ejecutando el programa easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f

1. Asignamos permisos de ejecución al programa llamado easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f. 

user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$ chmod +x easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f
user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$

2. Ejecutamos el programa anterior.

user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$ ./easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f
./bin flag_is_hereuser@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$

El programa imprime el mensaje “./bin flag_is_here”.

3. Ejecutamos el programa easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f con un argumento.

user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$ ./easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f ABC123
incorrect
user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$

Esta vez el programa imprime el mensaje “incorrect”. Es necesario decompilar el programa para conocer cómo es el flujo de su ejecución.

Decompilando el programa easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f 

 1. Decompilamos el programa llamado easy_crack_me-768bbdb6d3c597598d0f0c913941e4e3523af09bcfcff117f81e27158d783b3f con IDA-PRO.

2. IDA-PRO presenta la función main la cual recibe un argumento, el flag, Figura 1.

Figura 1. La función main del programa.

3. Se verifica que el usuario haya proporcionado el flag como parámetro. Si no es el caso, el programa imprime el mensaje "./bin flag_is_here" y finaliza. De lo contrario, el programa continúa con su ejecución, Figura 2.

Figura 2. El programa verifica que el usuario haya proporcionado el flag como parámetro.

4. La longitud del flag debe ser igual a treinta y nueve, Figura 3.

Figura 3. Verificación de la longitud del flag.

5. Los primeros seis caracteres del flag tienen que ser "TWCTF{" y el valor en flag[38] debe ser "}". Si no es el caso, el programa imprime el mensaje "incorrect". De lo contrario, el programa continúa con su ejecución, Figura 4.

Figura 4. Comparación de los caracteres 'T', 'W', 'C', 'T', 'F', '{' y '}' en ciertas posiciones del flag.

6. El programa cuenta el número de caracteres hexadecimales del flag, Figura 5.

Figura 5. El flag debe contener caracteres hexadecimales.

 7. El número de caracteres hexadecimales en el flag debe ser igual a los contadores en el arreglo renombrado como hex_counter, Figura 6.

Figura 6. El programa revisa que el número de caracteres hexadecimales en el flag sea igual a los contadores en el arreglo renombrado como hex_counter.

El contenido del arreglo hex_counter es el siguiente:

hex_counter = [3, 2, 2, 0, 3, 2, 1, 3, 3, 1, 1, 3, 1, 2, 2, 3];

Se espera encontrar tres veces el carácter "0" en el flag, dos veces el carácter "1", dos veces el carácter "2", así sucesivamente hasta 3 veces el carácter "f". Si no es el caso, el programa imprime el mensaje "incorrect" y finaliza. De lo contrario, el programa continúa con su ejecución.

8. Ciertas operaciones son realizadas con algunos valores del flag. Los valores finales se almacenan en los arreglos renombrados como v_check1 y v_check2, Figura 7.

Figura 7. Los arreglos v_check1 y v_check2 almacenan los resultados de ciertas operaciones con algunos valores del flag.

9. Cada resultado de las operaciones anteriores almacenadas en los elementos de los arreglos v_check1 y v_check2 deben ser iguales a los de los arreglos renombrados como check1 y check2, respectivamente. Si no son iguales, en cada caso, el programa imprime el mensaje "incorrect" y finaliza. De lo contrario, el programa continúa con su ejecución, Figura 8.

Figura 8. La comparación entre los valores v_check1 con check1 y v_check2 con check2 debe coincidir.

El contenido de los arreglos check1 y check2 es el siguiente:

check1 = [0x15e, 0xda, 0x12f, 0x131, 0x100, 0x131, 0xfb, 0x102];
check2 = [0x52, 0xc, 0x1, 0xf, 0x5c, 0x5, 0x53, 0x58];

10. De nuevo, ciertas operaciones con algunos valores del flag son realizadas. Los valores finales se almacenan en los arreglos renombrados como v_check3 y v_check4, Figura 9.

Figura 9. Los arreglos v_check3 y v_check4 almacenan los resultados de ciertas operaciones con algunos valores del flag.

11. Los resultados de las operaciones anteriores almacenadas en los elementos de los arreglos v_check3 y v_check4 deben coincidir a los de los arreglos renombrados como check3 y check4, respectivamente. Si no son iguales, en cada caso, el programa imprime el mensaje "incorrect" y finaliza. De lo contrario, el programa continúa con su ejecución, Figura 10.

Figura 10. La comparación entre los valores v_check3 con check3 y v_check4 con check4 debe coincidir.

El contenido de los arreglos check3 y check4 es el siguiente:

check3 = [0x129, 0x103, 0x12b, 0x131, 0x135, 0x10b, 0xff, 0xff];
check4 = [0x1, 0x57, 0x7, 0xd, 0xd, 0x53, 0x51, 0x51];

12. Luego, el programa crea un arreglo renombrado como v_check5, realiza ciertas operaciones con algunos valores del flag, de acuerdo con determinadas condiciones y almacena cada resultado en el arreglo anterior, Figura 11.

Figura 11. El arreglo v_check5 almacena el resultado de ciertas operaciones con algunos valores del flag.

13. Cada resultado de las operaciones anteriores almacenadas en el arreglo v_check5 tiene que ser igual al del arreglo renombrado como check5. Si no son iguales, en cada caso, el programa imprime el mensaje "incorrect" y finaliza. De lo contrario, el programa continúa con su ejecución, Figura 12.

Figura 12. La comparación entre los valores de v_check5 con los de check5 debe coincidir.

El contenido del arreglo check5 es el siguiente:

check5 = [0x80 ,0x80, 0xff, 0x80, 0xff, 0xff, 0xff, 0xff, 0x80, 0xff, 0xff, 0x80, 0x80, 0xff, 0xff, 0x80, 0xff, 0xff, 0x80, 0xff, 0x80, 0x80, 0xff, 0xff, 0xff, 0xff, 0x80, 0xff, 0xff, 0xff, 0x80, 0xff];

14. Existe una variable renombrada como check6 que se inicializa con el valor cero, luego se realizan ciertas operaciones con algunos valores del flag y se almacena el resultado final en la variable anterior, Figura 13.

Figura 13. La variable check6 almacena el resultado final de ciertas operaciones con algunos valores del flag.

15. El resultado final en check6 debe ser igual a 1160. Si no es el caso, el programa imprime el mensaje "incorrect" y finaliza. De lo contrario, el programa continúa con su ejecución, Figura 14.

Figura 14. La comparación entre la variable check6 con 1160 debe coincidir.

16. Finalmente, el programa compara algunos valores en las posiciones flag[37], flag[7], flag[11], flag[12], flag[23] y flag[31] contra los valores 53, 102, 56 , 55, 50 y 52, respectivamente. Si no es el caso, el programa imprime el mensaje "incorrect" y finaliza. De lo contrario, el programa imprime el mensaje "Correct" y el flag. Figura 15

Figura 15. La última comparación con algunos valores del flag.

Programando el script solucionador

1. Una vez que entendemos los pasos de verificación previos para validar el flag, nos propusimos resolver el reto utilizando la técnica llamada Z3 [1].

2. Por ello, programamos el siguiente script en Python 2:

#!/usr/bin/env python2
## Author: lehag
## Code: easy_crack_me.py
from z3 import *
import os

## Creating the array
flag = [BitVec('val_%i'%i,8) for i in range(0,39)];  ## flag_length == 39

## Creating the solver
s = Solver();

## Conditions
s.add(flag[0] == ord('T'));
s.add(flag[1] == ord('W'));
s.add(flag[2] == ord('C'));
s.add(flag[3] == ord('T'));
s.add(flag[4] == ord('F'));
s.add(flag[5] == ord('{'));
s.add(flag[38] == ord('}'));

## Required values
s1 = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
hex_values = "0123456789abcdef";
for i in range(0, len(hex_values)):
    for j in range(6, len(flag) - 1):
        s1[i] += If(flag[j] == ord(hex_values[i]), 1, 0);

## Check
hex_counter = [3, 2, 2, 0, 3, 2, 1, 3, 3, 1, 1, 3, 1, 2, 2, 3];
for i in range(0, len(s1)):
    s.add(s1[i] == hex_counter[i]);

## Required values
v_check1 = [];
v_check2 = [];
for k in range(0, 8):
    v10 = 0;
    v11 = 0;
    for l in range(0, 4):
        v5 = flag[4*k + 6 + l];
        v10 += v5;
        v11 ^= v5;
    v_check1.append(v10);
    v_check2.append(v11);

## Check
check1 = [0x15e, 0xda, 0x12f, 0x131, 0x100, 0x131, 0xfb, 0x102];
check2 = [0x52, 0xc, 0x1, 0xf, 0x5c, 0x5, 0x53, 0x58];
for i in range(0, len(v_check1)):
    s.add(v_check1[i] == check1[i]);
for i in range(0, len(v_check2)):
    s.add(v_check2[i] == check2[i]);

## Required values
v_check3 = [];
v_check4 = [];
for m in range(0, 8):
    v14 = 0;
    v15 = 0;
    for n in range(0, 4):
        v6 = flag[8*n + 6 + m];
        v14 += v6;
        v15 ^= v6;
    v_check3.append(v14);
    v_check4.append(v15);

## Check
check3 = [0x129, 0x103, 0x12b, 0x131, 0x135, 0x10b, 0xff, 0xff];
check4 = [0x1, 0x57, 0x7, 0xd, 0xd, 0x53, 0x51, 0x51];
for i in range(0, len(v_check3)):
    s.add(v_check3[i] == check3[i]);
for i in range(0, len(v_check4)):
    s.add(v_check4[i] == check4[i]);

## Required values
v_check5 = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
       0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
for ii in range(0, 32):
    v7 = flag[ii + 6];
    v_check5[ii] = If(And(v7 > 47, v7 <= 57), 255, If(And(v7 > 96, v7 <= 102), 128, 0));

## Check
check5 = [0x80,0x80,0xff,0x80,0xff,0xff,0xff,0xff,0x80,0xff,0xff,0x80,0x80,
        0xff,0xff,0x80,0xff,0xff,0x80,0xff,0x80,0x80,0xff,0xff,0xff,0xff,0x80,
        0xff,0xff,0xff,0x80,0xff];
for i in range(0, len(v_check5)):
    s.add(v_check5[i] == check5[i]);

## Required values
check6 = 0;
for jj in range(0, 16):
    check6 += flag[2* (jj + 3)];

## Check
s.add(check6 == 1160);

## Conditions
s.add(flag[37] == 53);
s.add(flag[7] == 102);
s.add(flag[11] == 56);
s.add(flag[12] == 55);
s.add(flag[23] == 50);
s.add(flag[31] == 52);

## Checking constraints
if(s.check() == sat):
    m = s.model();
    string = "";
    for i in range(39):
  string += chr(m[flag[i]].as_long());
    print(string);
else:
    print("Sorry ... :(");

3. Ejecutamos el script anterior y obtenemos el flag.

user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$ python2 easy_crack_me.py
TWCTF{df2b4877e71bd91c02f8ef6004b584a5}
user@blackbox:~/Tokyo Westerns/RE/Easy Crack Me$

Flag

TWCTF{df2b4877e71bd91c02f8ef6004b584a5}

Referencias

[1] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.225.8231&rep=rep1&type=pdf

Felicitaciones

A Julio Vidal aka m12 - @_jcvg_, por ser quien resolivó el reto durante el CTF.

Go Mayas!

Comentarios

Publicar un comentario