Challenge Details
This challenge is in the Hack the Box University CTF 2022.
We are not given a binary, but a source code written in Haskell
Code
import Data.Char (ord)import Data.Bits (xor)
-- Complete the incantation...flag = "HTB{XXX}"
-- validates flag format and extracts the flagextractFlag :: String -> StringextractFlag (s:rest) | s == 'H' || s == 'T' || s == 'B' = extractFlag rest | s == '{' && last rest == '}' = init rest | otherwise = error ("Invalid format")
-- creates a list of chunks of n elements from a listchunks :: 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))
-- takes the last n characters of an arraytakeLast :: 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 -> BoolcheckFlag 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!" )Understanding the program
main
In Haskell, main is a special function that is the entry point of the program.
It is the function that is executed when the program is run.
In this code, main is defined as a function that outputs a message
depending on the result of checkFlag applied to the flag string.
If checkFlag returns True, then main outputs
the string “The spell went off without a hitch!”.
If checkFlag returns False, then main
outputs the string “You disappear in a puff of smoke!”.
chunks
chunks is a function that divides a list into
sublists of a specified length.
It returns a list of these sublists.
If the length of the original list is not a
multiple of the specified length,
the last sublist will contain the remaining elements.
extractFlag
extractFlag is a function that takes the contents of the flag, following the flag format.
extractFlag "HTB{this_is_the_flag}"would return
"this_is_the_flagSide note: some strings are accepted by extractFlag, but are not necessarily in the correct format:
extractFlag "T{yet_another_flag}"extractFlag "B{one_more_flag}"checkFlag
checkFlag is a function that takes a string as input and
returns a boolean value indicating whether the
input string satisfies certain conditions.
The function first extracts the contents of the flag
string using the extractFlag function and converts
each character in the extracted string to its
ASCII code using the ord function from the Data.Char module.
Then it defines four lists, one, two, three, and four,
using list comprehension and the helper function chunks.
The one list is created by applying the function \ (l,r) -> l == r
to a list of pairs obtained by dividing the content
list into pairs of two elements using chunks 2.
This function compares each pair of elements and
returns True if they are equal, False otherwise.
The two list is created by applying the function foldr xor 0
to a list of lists obtained by dividing the content
list into lists of three elements using chunks 3.
This function performs a bitwise exclusive-or operation
on each list of three elements and returns the result.
The three list is created in a similar way,
but using the function foldr (+) 0 instead of foldr xor 0.
This function adds the elements of each list of four elements and returns the result.
Finally, the four list is created by applying the function head
to a list of lists obtained by dividing the content list into
lists of five elements using chunks 5.
This function returns the first element of each list.
The checkFlag function then checks that the length of content is 58
and that all elements in the lists one, two, three, and four
are equal to the corresponding elements in the
lists a, b, c, and d respectively.
If all these conditions are met, checkFlag
returns True, otherwise it returns False.
Solution
Brute-forcing may be an efficient solution, but you would need to consider some special cases.
My solution is to use Z3.
#!/usr/bin/env python3
from z3 import *import functools
def chunks(l, n): return [l[i:i+n] for i in range(0, len(l), n)]
def xor_chunk(e): return functools.reduce(lambda x,y: x^y, e)
# Create a solvers = Solver()
# Create a list of 58 bitvectors of size 8x = [BitVec('x%d' % i, 8) for i in range(58)]
one = list(map(lambda e: e[0] - e[1], chunks(x, 2)))two = list(map(lambda e: xor_chunk(e), chunks(x, 3)))three = list(map(sum, chunks(x, 4)))four = list(map(lambda e: e[0], chunks(x, 5)))
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, j in zip(one, a): s.add(i == j)for i, j in zip(two, b): s.add(i == j)for i, j in zip(three, c): s.add(i == j)for i, j in zip(four, d): s.add(i == j)
# make sure chars are printablefor i in x: s.add(i >= 32) s.add(i <= 126)
# Check if the constraints are satisfiableif s.check() == sat: # Get the model m = s.model() # Print the value print('HTB{' + ''.join([chr(m[x[i]].as_long()) for i in range(58)]) + '}')else: print('No solution found')