Tokyowesterns rev_rev_rev

Let's take a look at the binary:

$    file rev_rev_rev-a0b0d214b4aeb9b5dd24ffc971bd391494b9f82e2e60b4afc20e9465f336089f
rev_rev_rev-a0b0d214b4aeb9b5dd24ffc971bd391494b9f82e2e60b4afc20e9465f336089f: ELF 32-bit LSB executable, Intel 80386, version 1 (SYSV), dynamically linked, interpreter /lib/ld-linux.so.2, for GNU/Linux 2.6.32, BuildID[sha1]=e33eb178391bae637823f4645d63d63eac3a8d07, stripped
$    ./rev_rev_rev-a0b0d214b4aeb9b5dd24ffc971bd391494b9f82e2e60b4afc20e9465f336089f
Rev! Rev! Rev!
Your input: gimme that flag
Invalid!

So we are dealing with a 32 bit program that when we run it, it asks for input (and told us it was invalud). My guess is that this program takes input, alters it, and compares it against a string. Looking through the list of functions (or checking the X-References to strings) we find the FUN_080485ab function which looks like where the code we are interested in is:

undefined4 FUN_080485ab(void)

{
  char *bytesRead;
  int check;
  int in_GS_OFFSET;
  char input [33];
  int stackCanary;
 
  stackCanary = *(int *)(in_GS_OFFSET + 0x14);
  puts("Rev! Rev! Rev!");
  printf("Your input: ");
  bytesRead = fgets(input,0x21,stdin);
  if (bytesRead == (char *)0x0) {
    puts("Input Error.");
                    /* WARNING: Subroutine does not return */
    exit(0);
  }
  op0(input);
  op1(input);
  op2(input);
  op3(input);
  check = strcmp(input,PTR_DAT_0804a038);
  if (check == 0) {
    puts("Correct!");
  }
  else {
    puts("Invalid!");
  }
  if (stackCanary != *(int *)(in_GS_OFFSET + 0x14)) {
                    /* WARNING: Subroutine does not return */
    __stack_chk_fail();
  }
  return 0;
}

So we can see this function starts off bys scanning in 0x21 bytes into input. If the fgets call scans in no bytes, it exits with an error message. Then it runs input through 4 different functions (op0-op3). Then it compares our data against PTR_DAT_0804a038 using strcmp, and if it is equivalent then we pass the challenge. We can check what the value of PTR_DAT_0804a038 via clicking on it and checking it's value. What is happening here is it is scanning in input, altering it with the ops functions, then checking it against PTR_DAT_0804a038:

                             DAT_08048870                                    XREF[2]:     FUN_080485ab:08048668(*),
                                                                                          0804a038(*)  
        08048870 41              ??         41h    A
        08048871 29              ??         29h    )
        08048872 d9              ??         D9h
        08048873 65              ??         65h    e
        08048874 a1              ??         A1h
        08048875 f1              ??         F1h
        08048876 e1              ??         E1h
        08048877 c9              ??         C9h
        08048878 19              ??         19h
        08048879 09              ??         09h
        0804887a 93              ??         93h
        0804887b 13              ??         13h
        0804887c a1              ??         A1h
        0804887d 09              ??         09h
        0804887e b9              ??         B9h
        0804887f 49              ??         49h    I
        08048880 b9              ??         B9h
        08048881 89              ??         89h
        08048882 dd              ??         DDh
        08048883 61              ??         61h    a
        08048884 31              ??         31h    1
        08048885 69              ??         69h    i
        08048886 a1              ??         A1h
        08048887 f1              ??         F1h
        08048888 71              ??         71h    q
        08048889 21              ??         21h    !
        0804888a 9d              ??         9Dh
        0804888b d5              ??         D5h
        0804888c 3d              ??         3Dh    =
        0804888d 15              ??         15h
        0804888e d5              ??         D5h
        0804888f 00              ??         00h

So first we take a look at the op0 function and we see this:

void op0(char *input)

{
  char *newLinePos;
 
  newLinePos = strchr(input,10);
  *newLinePos = '\0';
  return;
}

Looking at this function, we can see that it first looks for the character 0xa, which is a newline character. Then it set's that equal to 0x0. So essentially it replaces the newline character with a null byte. Let's take a look at op1:

void op1(char *input)

{
  size_t len;
  char *beg;
  char *end;
  char holder;
 
  beg = input;
  len = strlen(input);
  end = input + (len - 1);
  while (beg < end) {
    holder = *beg;
    *beg = *end;
    *end = holder;
    beg = beg + 1;
    end = end + -1;
  }
  return;
}

This code essentially takes our input (which has had the newline character stripped) and just reverses it. For instance, if we gave the program 1234, it would reverse it to 4321. Now let's look at op2.

void op2(byte *input)

{
  byte x;
  byte y;
  byte *inputCpy;
 
  inputCpy = input;
  while (*inputCpy != 0) {
    x = (char)*inputCpy >> 1 & 0x55U | (*inputCpy & 0x55) * '\x02';
    y = (char)x >> 2 & 0x33U | (byte)(((int)(char)x & 0x33U) << 2);
    *inputCpy = y >> 4 | (byte)((int)(char)y << 4);
    inputCpy = inputCpy + 1;
  }
  return;
}

This function alters the input, by performing various binary operations on our input (and in one case, multiplying it). We can see that it is a for loop that will run once per each character of our input. It will take the hex value of each character of our input and alter it, however it will only take the first 8 bits worth of data (so the least significant bit). This code effectively translates to the following python since this might be a bit easier to understand. Also shifting a value to the right by 2 is the same as multiplying it by 4:

def enc(input):
    output = ""
    for c in input:
        c = ord(c)
        x = (2 * (c & 0x55)) | ((c >> 1) & 0x55)
        print "x is: " + hex(x)
        y = (4 * (x & 0x33)) | ((x >> 2) & 0x33)
        print "y is: " + hex(y)
        z = (16 * y) | ( y >> 4)
        print "z is: " + hex(z)
        output = hex(z).replace("0x", "")[-2:] + output
    return output

With all of that, let's take a look at the final function our input is ran through op3:

void op3(byte *input)

{
  byte *inputCpy;
 
  inputCpy = input;
  while (*inputCpy != 0) {
    *inputCpy = ~*inputCpy;
    inputCpy = inputCpy + 1;
  }
  return;
}

So like the previous function, this runs a loop that iterates for each character of the input. However this time it alters each character by performing a binary not (which it's operator in c is ~). Essentially it takes the binary value of the character, and converts the zeros to ones and ones to zeros. For instance:

0:    0x30:    00110000
NOT 0:         11001111 = 0xcf

it essentially performs the same function as this python script:

def not_inp(inp):
    output = 0x0
    result = ""
    string = bin(inp).replace("0b", "")
    print "Binary string is: " + string
    for s in string:
        if s == "0":
            result += "1"
        if s == "1":
            result += "0"
    print "Binary inverse is: " + result
    output = int(result, 2)
    return output

So we understand what the four functions do. We could have also figured out what some of the functions do by using gdb, and looking at the value of input_buf changes (it's how I figured out what the first two functions did). Set the breakpoints before each of the four functions is called, and the final strcmp:

gdb-peda$ b *0x0804862b
Breakpoint 1 at 0x804862b
gdb-peda$ b *0x0804863a
Breakpoint 2 at 0x804863a
gdb-peda$ b *0x08048649
Breakpoint 3 at 0x8048649
gdb-peda$ b *0x08048658
Breakpoint 4 at 0x8048658
gdb-peda$ b *0x0804866d
Breakpoint 5 at 0x804866d
gdb-peda$ r
Starting program: /Hackery/west/rev/rev_rev_rev-a0b0d214b4aeb9b5dd24ffc971bd391494b9f82e2e60b4afc20e9465f336089f
Rev! Rev! Rev!
Your input: tux

Before op0 is called:

Breakpoint 1, 0x0804862b in ?? ()
gdb-peda$ x/s $eax
0xffffd07b:    "tux\n"
gdb-peda$ c
Continuing.

After op0, before op1:

Breakpoint 2, 0x0804863a in ?? ()
gdb-peda$ x/s $eax
0xffffd07b:    "tux"
gdb-peda$ c
Continuing.

After op1, before op2:

Breakpoint 3, 0x08048649 in ?? ()
gdb-peda$ x/s $eax
0xffffd07b:    "xut"
gdb-peda$ c
Continuing.

After op2, before op3:

Breakpoint 4, 0x08048658 in ?? ()
gdb-peda$ x/x $eax
0xffffd07b:    0x1e
gdb-peda$ x/w $eax
0xffffd07b:    0x002eae1e
gdb-peda$ x/s $eax
0xffffd07b:    "\036\256."
gdb-peda$ c
Continuing.

After op3, before strcmp:

Breakpoint 5, 0x0804866d in ?? ()
gdb-peda$ x/x $eax
0xffffd07b:    0xe1
gdb-peda$ x/w $eax
0xffffd07b:    0x00d151e1

So we can see the text altered as it is passed through the function. Now that we know what happens to the text, we just need to know what it needs to be after all of it. When we see what value desired_output holds, we see this:

.rodata:08048870 desired_output_storage db  41h ; A      ; DATA XREF: .data:desired_outputo
.rodata:08048871                 db  29h ; )
.rodata:08048872                 db 0D9h ; +
.rodata:08048873                 db  65h ; e
.rodata:08048874                 db 0A1h ; í
.rodata:08048875                 db 0F1h ; ±
.rodata:08048876                 db 0E1h ; ß
.rodata:08048877                 db 0C9h ; +
.rodata:08048878                 db  19h
.rodata:08048879                 db    9
.rodata:0804887A                 db  93h ; ô
.rodata:0804887B                 db  13h
.rodata:0804887C                 db 0A1h ; í
.rodata:0804887D                 db    9
.rodata:0804887E                 db 0B9h ; ¦
.rodata:0804887F                 db  49h ; I
.rodata:08048880                 db 0B9h ; ¦
.rodata:08048881                 db  89h ; ë
.rodata:08048882                 db 0DDh ; ¦
.rodata:08048883                 db  61h ; a
.rodata:08048884                 db  31h ; 1
.rodata:08048885                 db  69h ; i
.rodata:08048886                 db 0A1h ; í
.rodata:08048887                 db 0F1h ; ±
.rodata:08048888                 db  71h ; q
.rodata:08048889                 db  21h ; !
.rodata:0804888A                 db  9Dh ; ¥
.rodata:0804888B                 db 0D5h ; +
.rodata:0804888C                 db  3Dh ; =
.rodata:0804888D                 db  15h
.rodata:0804888E                 db 0D5h ; +
.rodata:0804888F                 db    0

So we can see that it is equal to a hex string starting with 0x41 and ending with 0x0. So now that we know what it needs to be equal to we can use the solver z3. Essentially once we define what happens to the input, z3 will tell us what input we need to meet the desired output.

I made two scripts, one to undo the binary not, and one to figure out the input needed to get the desired output out of enc_func. Also to account for op1 (function that reverses our input) I just inputted the hex string backwards. Now for the script to undo the binary not:

#Establish the flag after the binary not
flag = [ 0xd5, 0x15, 0x3d, 0xd5, 0x9d, 0x21, 0x71, 0xf1, 0xa1, 0x69, 0x31, 0x61, 0xdd, 0x89, 0xb9, 0x49, 0xb9, 0x09, 0xa1, 0x13, 0x93, 0x09, 0x19, 0xc9, 0xe1, 0xf1, 0xa1, 0x65, 0xd9, 0x29, 0x41]

#Establish the function to execute the binary not
def not_inp(inp):
    output = 0x0
    result = ""
    string = bin(inp).replace("0b", "")
    #Check if there are less than 8 bits, and if so add zeroes to the front to get 8 bits
    if len(string) < 8:
        diff = 8 - len(string)
        string = diff*"0" + string
    print "Binary string is:  " + string
    
    #Swap the ones with zeroes, and vice versa
    for s in string:
        if s == "0":
            result += "1"
        if s == "1":
            result += "0"
    print "Binary inverse is: " + result
    
    #Convert the binary string to an int, and return it
    output = int(result, 2)
    return output

#Establish the array which will hold the output
out = []
#Iterate through each character of the flag, and undo the binary not
for i in flag:
    x = not_inp(i)
    out.append(x)
    print hex(x)

#Print the flag before the binary not
print "alt_flag = " + str(out)

when we run the script, we see that the hex string before the binary not happens is equal to this:

alt_flag = [42, 234, 194, 42, 98, 222, 142, 14, 94, 150, 206, 158, 34, 118, 70, 182, 70, 246, 94, 236, 108, 246, 230, 54, 30, 14, 94, 154, 38, 214, 190]

With this info, we can just use z3 to figure out the input needed for enc_func to output that. Z3 is a theorem solver by Microsoft (you can find install instructions here https://github.com/Z3Prover/z3). Z3 will allow us to essentially declare the input it has control over, specify the algorithm that it goes through, and then specify what you want the output to be (and any additional constraints you want to have). Then you can check if Z3 can solve it, and if it can it will solve it and print a solution. Checkout the code for more details:

#Import z3
from z3 import *

#Establish the hex array of what the end result should be before the binary not
alt_flag = [42, 234, 194, 42, 98, 222, 142, 14, 94, 150, 206, 158, 34, 118, 70, 182, 70, 246, 94, 236, 108, 246, 230, 54, 30, 14, 94, 154, 38, 214, 190]

#Establish the solving function
def solve(alt_flag):    
    #Establish the solver
    zolv = Solver()

    #Establish the array which will hold all of the integers which we will input
    inp = []
    for i in range(0, len(alt_flag)):
        b = BitVec("%d" % i, 16)
        inp.append(b)

    #Run the same text altering function as enc_func
    for i in range(0, len(alt_flag)):
        x = (2 * (inp[i] & 0x55)) | ((inp[i] >> 1) & 0x55)
        y = (4 * (x & 0x33)) | ((x >> 2) & 0x33)
        z = (16 * y) | ( y >> 4)
        #We need to and it by 0xff, that way we only get the last 8 bits
        z = z & 0xff
        #Add the condition to z3 that we need to end value to be equal to it's corresponding alt_flag value
        zolv.add( z == alt_flag[i])

    #Check if the problem is solvable by z3
    if zolv.check() == sat:
        print "The condition is satisfied, would still recommend crying: " + str(zolv.check())
        #The problem is solvable, model it and print the solution
        solution = zolv.model()
        flag = ""
        for i in range(0, len(alt_flag)):
            flag += chr(int(str(solution[inp[i]])))
        print flag

    #The problem is not solvable by z3    
    if zolv.check() == unsat:
        print "The condition is not satisfied, would recommend crying: " + str(zolv.check())


solve(alt_flag)

Let's try it!

$ python reverent.py
The condition is satisfied, would still recommend crying: sat
TWCTF{qpzisyDnbmboz76oglxpzYdk}
$ ./rev_rev_rev
Rev! Rev! Rev!
Your input: TWCTF{qpzisyDnbmboz76oglxpzYdk}
Correct!

Just like that, we reversed the challenge!