Writeup by FloDarPie for babyfuscation

First step - gather intelligence

As the name intend it, there is a bit of obfuscation. Let’s rename some functions and variables.

00401395    int32_t main(int32_t argc, char** argv, char** envp)

004013d6        for (int32_t i = 0; i s<= 0x4f; i += 1)
004013cb            *(sx.q(i) + &buffer1) ^= 0x42
004013cb        
0040140d        for (int32_t i_1 = 0; i_1 s<= 0x4f; i_1 += 1)
00401402            (*"P|aavpg23J|f4ev3u|f}w3g{v3u")[sx.q(i_1)] ^= 0x13
00401402        
00401444        for (int32_t i_2 = 0; i_2 s<= 0x4f; i_2 += 1)
00401439            (*"`EXYP")[sx.q(i_2)] ^= 0x37
00401439        
0040144b        première_fonction()
00401455        deuxieme_fonction()
00401465        return retour_reponse()

We can pursue this work, identifie each operation, follow the path… but is quite fastidious. We can at least have the squeleton of the program :

main()

 - première_fonction()
        puts()
        fgets()
 - deuxieme_fonction()
 - retour_reponse()
    if(__):
        puts()
    else:
        puts()

If we run an example :

$ ./babyfuscation.txt 
Enter the flag: 
toto
Wrong flag. Try again!

We understand tha the binary wrapped the input gived through fgets and print and answer with puts.

We can solve the lines 00401402 and 00401439 to understand what’s under the hood :

input = "P|aavpg23J|f4ev3u|f}w3g{v3u"
unxored = ''.join(chr(ord(lettre) ^0x13) for lettre in input)
print(unxored)
input = "`EXYP"
unxored = ''.join(chr(ord(lettre) ^0x37) for lettre in input)
print(unxored)

There is a Correct! and a Wrong strings.

Second step - find the correct flag

We know, when we execute our binary :

• if we give a false input, the program will display Wrong
• else, with the correct flag, we will have Correct!

Synthetizing the executions paths :

      __ puts('Wrong')
main_/
     \__ puts('Correct!')

Thanks to some researchers from CEA (France), there exist a tool named BINSEC who can explore all the paths and then identify how to follow the paths.

It’s not the only symbolic analysis tool available, but it’s very efficient for our situation.

Third step - configure BINSEC

Now that we know that the code prints “Correct!” via puts when feeding it the flag, we are going to analyse the executable to find path where puts takes “Correct!” as an argument.

With the help of the official documentation website we cooked this initialization file :

#Initialize the stack pointer with a concrete value
starting from core

stdin_p<64> := 0

#skip the syscall not supported by Binsec
replace opcode 0f05 by  
    print rax
    cut
end

#replace the function fgets not supported by Binsec and mimic the user input
replace <fgets>(buffer, size, stdin) by
  for i<64> in 0 to size - 1 do
    @[buffer + i] := stdin[stdin_p]
    stdin_p := stdin_p + 1
  end
  return buffer
end

#replace the function puts and detect when it is used with our target "Correct!" then print what input was used to reach that point
replace <puts>(arg1) by
    reach such that @[arg1, 8] = "Correct!" then print c string stdin
        and print c string @[arg1]
    return
end

#stop the analysis at the exit symbol, we don't need to analyze the exit routine
replace <exit> by
    halt
end

Once this configuration file written, we need to make babyfuscation executable :

$ chmod +x babyfuscation

We also need to generate a snapshot of the memory to have a concrete context for Binsec. This context is generated by executing the file until main is reached and therefore gives a proper initialization. This is done automatically by Binsec with the following command :

$ make_coredump.sh babyfuscation_snapshot babyfuscation.txt

Then start the analysis :

$ binsec -sse-script babyfuscation.ini babyfuscation_snapshot -sse-depth 100000 -smt-multi-checks

Binsec outputs that it can reach the desiered message with the following flag : FCSC{e30f46b147e7a25a7c8b865d0d895c7c7315f69582f432e9405b6d093b6fb8d3}.