Potion Master

7 minutos de lectura

Se nos proporciona un script en Haskell llamado potion.hs:

import Data.Char (ord)
import Data.Bits (xor)

-- Complete the incantation...
flag = "HTB{XXX}"

extractFlag :: String -> String
extractFlag (s:rest)
  | s == 'H' ||  s == 'T' ||  s == 'B'
  = extractFlag rest
  | s == '{' && last rest == '}'
  = init rest
  | otherwise = error ("Invalid format")

chunks :: Int -> [a] -> [[a]]
chunks n l
  | n == 0 = []
  | n == 1 = [[x] | x <- l]
  | length l <= n = [l]
  | otherwise = [take n l] ++ (chunks n (drop n l))

takeLast :: Int -> [a] -> [a]
takeLast n = reverse . take n . reverse

a = [-43, 61, 58, 5, -4, -11, 64, -40, -43, 61, 62, -51, 46, 15, -49, -44, 47, 4, 6, -7, 47, 7, -59, 52, -15, 11, 7, 61, 0]  
b = [6, 106, 10, 0, 119, 52, 51, 101, 0, 0, 15, 48, 116, 22, 10, 58, 125, 100, 102, 33]
c = [304, 357, 303, 320, 304, 307, 349, 305, 257, 337, 340, 309, 428, 270, 66]
d = [52, 52, 95, 95, 110, 49, 51, 51, 95, 110, 110, 53]

checkFlag :: String -> Bool
checkFlag flag =
  length content == 58 &&
  all (==True) (map (\ (l,r) -> l == r) (zip one a)) &&
  all (==True) (map (\ (l,r) -> l == r) (zip two b)) &&
  all (==True) (map (\ (l,r) -> l == r) (zip three c)) &&
  all (==True) (map (\ (l,r) -> l == r) (zip four d))
  where content = map ord (extractFlag flag)
        one     = map (\ [l, r] -> (l - r)) (chunks 2 content)
        two     = map (foldr xor 0) (chunks 3 content)
        three   = map (foldr (+) 0) (chunks 4 content)
        four    = map head (chunks 5 content)

main = putStrLn (if (checkFlag flag)
    then "The spell went off without a hitch!"
    else "You disappear in a puff of smoke!"
  )

Ejecutando Haskell

Haskell es un lenguaje de programación para programación funcional. Nunca he usado Haskell, así que comencemos iniciando la imagen oficial de Docker de Haskell y ejecutando el script anterior:

$ docker run --rm -v "$(pwd):/ctf" -it haskell bash
Unable to find image 'haskell:latest' locally
latest: Pulling from library/haskell
34983cc1fd1c: Pull complete
35873fa6ec37: Pull complete
07615c620859: Pull complete
b02969cbb074: Pull complete
bfaf27b3e7c3: Pull complete
92d4324d1b8f: Pull complete
d609e5978a1c: Pull complete
b230c8cb62e7: Pull complete
Digest: sha256:6df0c290c28e0d63c183acd41a38fa598e0d164340e76a85af847b3c6f3203f6  
Status: Downloaded newer image for haskell:latest
root@5e3b89eff31f:/# cd /ctf
root@5e3b89eff31f:/ctf# ls
potion.hs

Para ejecutar un script en Haskell, debemos compilarlo y luego ejecutar el archivo binario resultante:

root@5e3b89eff31f:/ctf# ghc -o potion potion.hs
[1 of 2] Compiling Main             ( potion.hs, potion.o )  
[2 of 2] Linking potion
root@5e3b89eff31f:/ctf# ./potion
You disappear in a puff of smoke!

Sin embargo, no necesitaremos ejecutar Haskell para resolver el reto.

Análisis de código estático

Incluso si no sabemos Haskell, podemos intuir qué está haciendo el script. Comencemos al final del archivo:

main = putStrLn (if (checkFlag flag)
    then "The spell went off without a hitch!"  
    else "You disappear in a puff of smoke!"
  )

Parece que si checkFlag flag devuelve True, entonces se muestra el mensaje "The spell went off without a hitch!" (y la flag es correcta); si no, veremos "You disappear in a puff of smoke!" (como se muestra arriba).

La flag se define en la parte superior del archivo con un valor cualquiera. Tendremos que encontrar la flag correcta:

-- Complete the incantation...  
flag = "HTB{XXX}"

Analizar la función de verificación

La flag se valida utilizando una función llamada checkFlag:

checkFlag :: String -> Bool
checkFlag flag =
  length content == 58 &&
  all (==True) (map (\ (l,r) -> l == r) (zip one a)) &&
  all (==True) (map (\ (l,r) -> l == r) (zip two b)) &&
  all (==True) (map (\ (l,r) -> l == r) (zip three c)) &&
  all (==True) (map (\ (l,r) -> l == r) (zip four d))
  where content = map ord (extractFlag flag)
        one     = map (\ [l, r] -> (l - r)) (chunks 2 content)  
        two     = map (foldr xor 0) (chunks 3 content)
        three   = map (foldr (+) 0) (chunks 4 content)
        four    = map head (chunks 5 content)

Primero, está verificando que content tiene una longitud igual a 58. Y content = map ord (extractFlag flag), que parece ser una lista de números correspondientes a los códigos ASCII de los caracteres de la flag. Por otro lado, extractFlag verifica que la flag comienza por HTB{, termina con } y devuelve los caracteres intermedios:

extractFlag :: String -> String
extractFlag (s:rest)
  | s == 'H' ||  s == 'T' ||  s == 'B'
  = extractFlag rest
  | s == '{' && last rest == '}'
  = init rest
  | otherwise = error ("Invalid format")

En este punto, ya sabemos que la flag será HTB{ más 58 caracteres más }.

Después de la verificación de la longitud, el programa verifica que las listar one y a son iguales, luego two y b, luego three y c, y finalmente four y d. Las listas a, b, c, d se definen así:

a = [-43, 61, 58, 5, -4, -11, 64, -40, -43, 61, 62, -51, 46, 15, -49, -44, 47, 4, 6, -7, 47, 7, -59, 52, -15, 11, 7, 61, 0]  
b = [6, 106, 10, 0, 119, 52, 51, 101, 0, 0, 15, 48, 116, 22, 10, 58, 125, 100, 102, 33]
c = [304, 357, 303, 320, 304, 307, 349, 305, 257, 337, 340, 309, 428, 270, 66]
d = [52, 52, 95, 95, 110, 49, 51, 51, 95, 110, 110, 53]

Y luego tenemos one, two, three y four:

        one     = map (\ [l, r] -> (l - r)) (chunks 2 content)  
        two     = map (foldr xor 0) (chunks 3 content)
        three   = map (foldr (+) 0) (chunks 4 content)
        four    = map head (chunks 5 content)

Todos ellos emplean una función llamada chunks que toma la lista content y la divide en trozos del tamaño indicado (obviamente):

chunks :: Int -> [a] -> [[a]]
chunks n l
  | n == 0 = []
  | n == 1 = [[x] | x <- l]
  | length l <= n = [l]
  | otherwise = [take n l] ++ (chunks n (drop n l))

Usando map, las listas se definen como una función aplicada a cada fragmento. La función llamada foldr es como reduce en Python o JavaScript, y head toma el primer elemento de una lista.

Estas son las operaciones que se calculan (digamos que c = content):

one: La resta entre el primer y el segundo número del fragmento (c[0] - c[1], c[2] - c[3], c[4] - c[5]…)
two: El XOR entre los elementos del trozo (c[0] ^ c[1] ^ c[2], c[3] ^ c[4] ^ c[5]…)
three: La suma de los elementos del trozo (c[0] + c[1] + c[2] + c[3], c[4] + c[5] + c[6] + c[7]…)
four: El primer elemento el trozo (c[0], c[5], c[10]…)

Resolución con `z3`

Ahora que sabemos lo que está haciendo la función checkFlag, podemos usar z3 para definir un solucionador y declarar las restricciones anteriores para encontrar una solución que coincida con todas (que será la flag, presumiblemente).

En Python, podemos usar este script:

#!/usr/bin/env python3

from functools import reduce
from z3 import BitVec, Solver

x = [BitVec(f'x{i}', 8) for i in range(58)]
s = Solver()

a = [-43, 61, 58, 5, -4, -11, 64, -40, -43, 61, 62, -51, 46, 15, -49, -44, 47, 4, 6, -7, 47, 7, -59, 52, -15, 11, 7, 61, 0]  
b = [6, 106, 10, 0, 119, 52, 51, 101, 0, 0, 15, 48, 116, 22, 10, 58, 125, 100, 102, 33]
c = [304, 357, 303, 320, 304, 307, 349, 305, 257, 337, 340, 309, 428, 270, 66]
d = [52, 52, 95, 95, 110, 49, 51, 51, 95, 110, 110, 53]

for i in range(0, 58, 2):
    s.add(reduce(lambda x, y: x - y, x[i : i + 2]) == a[i // 2])

for i in range(0, 58, 3):
    s.add(reduce(lambda x, y: x ^ y, x[i : i + 3]) == b[i // 3])

for i in range(0, 58, 4):
    s.add(reduce(lambda x, y: x + y, x[i : i + 4]) == c[i // 4])

for i in range(0, 58, 5):
    s.add(x[i] == d[i // 5])

s.check()
model = s.model()

flag = ''.join(chr(model[i].as_long()) for i in x)

print('HTB{' + flag + '}')

Sin embargo, parece que la solución no es completamente correcta:

$ python3 solve.py
HTB{4_m0n4d_15_ju57_´ßm0n01d_1n_·è3_c47360ry_0f_3nd0func70r5!!}

Dado que hay caracteres especiales, podemos agregar más restricciones para forzar que todos los caracteres sean ASCII válidos:

for i in range(58):
    s.add(x[i] <= 0x7f)  
    s.add(0x20 <= x[i])

Flag

Ahora obtenemos la flag correcta:

$ python3 solve.py
HTB{4_m0n4d_15_ju57_4_m0n01d_1n_7h3_c47360ry_0f_3nd0func70r5!!}

El script completo se puede encontrar aquí: solve.py.

Ejecutando Haskell

Análisis de código estático

Analizar la función de verificación

Resolución con z3

Flag

Resolución con `z3`