Reversing 100: Z3 SMT Solver

By BioITINES Team

Con este reto lo primero que se hizo fue detectar que el binario babyRev era un ELF64, por lo que lo ejecutamos en la consola de Linux y nos arrojó el siguiente mensaje:

Tomando en cuenta esto, determinamos que debíamos pasarle un argumento al programa desde la consola para su ejecución.

Si esa condición se cumplía, validaba el argumento “flag” mediante un ciclo, carácter por carácter para cumplir con las siguientes condiciones.
Detectamos que había dos condiciones para generar la clave que era la longitud de la misma igual a 16 (10 Hex).

Y la suma del total de sus caracteres deberia ser igual a 1364 (554 Hex):

Dicho esto, optamos por usar Z3 Solver para generar la clave y el código que usamos fue el siguiente:

Se agregan las condiciones requeridas para encontrar la flag en las lineas 7 y 9, se pide al solver encontrar la solucion en la linea 14 y finalmente de encontrarse una solucion se imprimen los valores en la linea 17 arrojando lo siguiente:

Y al ingresarla en el ejecutable del reto nos arrojó lo siguiente:

Bingo!!!!!

HackDef Team:

Este reto arrojaba varias soluciones, el resolverlo con Z3 fue de alto nivel aunque no necesario para un reto con una logica tan sencilla, pero que bueno que se conoce este solver el cual ayudara con retos mas complejos.