<- HTB UNICTF

Potion Master

8 minutes to read

We are given a Haskell script called 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!"
  )

Running Haskell

Haskell is a programming language for functional programming. I have never used Haskell, so let’s start by running the official Docker image of Haskell and run the above script:

$ 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

To run a Haskell script, we must compile it and then run the resulting binary file:

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!

However, we won’t need to run Haskell to solve the challenge.

Static code analysis

Even if we don’t know Haskell, we can guess what the script is doing. Let’s start by the end of the file:

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

This one seems to be that if checkFlag flag returns True, then the message "The spell went off without a hitch!" is shown (and the flag is correct), otherwise we will see "You disappear in a puff of smoke!" (as shown above).

The flag is defined at the top of the file with a dummy value. We will need to find the correct flag:

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

Analyzing the check function

The flag is validated using a function named 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)

First, it is checking that content has length equal to 58. And content = map ord (extractFlag flag), which seems to be an array of numbers corresponding to the ASCII codes of the flag characters. On the other hand, extractFlag checks that the flag starts by HTB{, ends with } and returns the middle characters:

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

At this point, we already know that the flag will be HTB{ plus 58 characters plus }.

After the length check, the program checks that the arrays one and a are equal, then two and b, then three and c, and finally four and d. The arrays a, b, c, d are defined like this:

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]

And then we have one, two, three and 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)

All of them employ a function called chunks that takes the content array and splits it in chunks of the indicated size (obviously):

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))

Using map, the arrays are defined as a function applied to each chunk. The function called foldr is just like reduce in Python or JavaScript, and head takes the first element of an array.

These are the operations that are computed (say c = content):

  • one: The difference between the first and the second number of the chunk (c[0] - c[1], c[2] - c[3], c[4] - c[5] and so on)
  • two: The XOR between the elements of the chunk (c[0] ^ c[1] ^ c[2], c[3] ^ c[4] ^ c[5] and so on)
  • three: The sum of the elements of the chunk (c[0] + c[1] + c[2] + c[3], c[4] + c[5] + c[6] + c[7] and so on)
  • four: The first element the chunk (c[0], c[5], c[10] and so on)

Solving with z3

Now that we know what the checkFlag function is doing, we can use z3 to define a solver and declare the above constraints to find a solution that matches all of them (that will be the flag, presumably).

In Python, we can use this 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 + '}')

However, it looks like the solution is not fully correct:

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

Since there are special characters, we can add more constraints to force that all characters are valid ASCII digits:

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

Flag

Now we obtain the correct flag:

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

The full script can be found in here: solve.py.