VolgaCTF 2015 interstellar

@mrexcessive WHA
& Tom O'Brien WHA

The problem

Just a snall binary from a far-far galaxy
interstellar - binary for download

The solution

Started with readelf -a ./interstellar

Then straced it
Nothing particularly weird

objdump -d ./interstellar >asm.asm

and read through

gdb --args ./interstellar abcd
(gdb) b\*0x400c46            ; hits here first
(gdb) b\*0x400c02
(gdb) b\*0x400af4
(gdb) b\*0x400ab7

There's a sleep(1) call... in the code, just after fork()
Implies perhaps bruting is possible.
Hmmm...
But the main thread just checks for debugger (ptrace), checks that no LD_PRELOAD
The work is probably happening in the other thread

Tried various things, patching around the debugger checks thread...
... stopping it for longer with a huge sleep.
Doesn't seem to object to me patching the binary (with bvi!) and then rerunnning

So I have various versions at this point, with some strange patches.

We have a strcmp() just after this

  400e7a:    48 89 d6                mov    %rdx,%rsi                 
  400e7d:    48 89 c7                mov    %rax,%rdi

Which seems to verify flag.

After a while work out it demands exactly 36 chars.
gdb --args ./jhacked 012345678901234567890123456789012345

Try again with that.
OK better !

This then gets to 0x400dff once... then exits

Process is exiting at 0x400b93
OK... this can maybe be patched..

(gdb) hb *0x400b8e
;when it hits that... 
(gdb) set $pc = 0x400b98
;Now
(gdb) b *0x400e6f
;OK reached the strcmp()
;        012345678901234567890123456789012345
$rdx = "From a seed a mighty trunk may grow.\n"
$rax = "0234b32db9ecd2fde7b4fc03240ab6fbb0844525db477f13251a7ed7134773db8e589f2da7"

But it's a calculated flag... so not much joy.

(gdb) x/36bx $rax
0x7fffffffe2d0:    0x5b    0xe6    0x53    0xf3    0x11    0x29    0xec    0x36
0x7fffffffe2d8:    0xc0    0xd2    0xa2    0x25    0x24    0x36    0x41    0xf1
0x7fffffffe2e0:    0x2b    0x58    0x1a    0xf1    0x23    0x15    0x6d    0xdd
0x7fffffffe2e8:    0x7c    0x6e    0x9c    0xaa    0xde    0xac    0x91    0x79
0x7fffffffe2f0:    0x93    0x60    0x47    0xfa

We need correct input to the algo.
It's using strange floatingpoint math routines, but only as integers.
Don't these people know about Python!

I'm writing it in Python...

def FirstMangle(s):
   v = 0
   for i in xrange(0,len(s)):
      v *= 307
      v += ord(s[i])
   return v

sInput = "012345678901234567890123456789012345"
   assert(len(sInput) == 36)
   v1 = FirstMangle(sInput)
   print bin(v1)     

Check we get same binary output as from the program itself in GDB...

Yes

There is then a Binary XNOR...
The key is found here

(gdb) x/1s0x400f70
0x400f70:     "01111101001000101000000111101001001011111110010011100111010011000010101101110110100001101011100101001110000000001101000110001011011010101001000000010010001100011001100011001011010101111011110110001100101100101000110011101111101101000110110010101001100100110100010101101111101111011001100011111101"

It is fixed position and unchanging content between runs... Hurrah!

Now we have a Python program which can run it... had a few attempts at bruting it backwards from LSB to MSB

   sStartWith = "x12345678901234567890123456789012345"
   sTarget =    "From a seed a mighty trunk may grow."
   charsin = []
   for ch in sStartWith:
      charsin.append(ch)
   # brute it one char at a time, backwards
   # get 3 chars right
   valids = []
   useables = ""
   for i in xrange(0,len(sStartWith)):    # start all sets off as whole set
      valids.append(printables)
   posnA = len(sStartWith) - 3            # initial pos for left hand side
   while posnA >= 0:
      posnB = posnA + 1
      posnC = posnA + 2
      validB = {}
      validC = {}
      for chA in valids[posnA]:
         for chB in valids[posnB]:
            for chC in valids[posnC]:
               charsin[posnA] = chA
               charsin[posnB] = chB
               charsin[posnC] = chC
               (isGood,result) = ComputeFor(''.join(charsin))
               if isGood:
                  result = result[0:36]         # this is what the assembler does...  (drop final byte)
                  if result[posnC] == sTarget[posnC]:      # got one
                     validB[chB] = 1
                     validC[chC] = 1      
      print "All valid B at %i [%s]" % (posnB,validB.keys())
      print "All valid C at %i [%s]" % (posnC,validC.keys())
      # modify the posnB keys... but not the A or C
      valids[posnB] = ''.join(validB.keys())
      # go for next
      posnA -= 1
#      if posnA < len(sStartWith) - 6:      #XXX for debug
#         break      # skip to next part
# Same thing... but using the valids... and only accepting two chars correct as ok ?
   posnA = len(sStartWith) - 4            # initial pos for left hand side
   while posnA >= 0:
      posnB = posnA + 1
      posnC = posnA + 2
      posnD = posnA + 3
      validB = {}
      validC = {}
      validD = {}
      for chA in valids[posnA]:
         sys.stdout.write(".")         # for comfort / sanity
         sys.stdout.flush()
         for chB in valids[posnB]:
            for chC in valids[posnC]:
               for chD in valids[posnD]:
                  charsin[posnA] = chA
                  charsin[posnB] = chB
                  charsin[posnC] = chC
                  charsin[posnD] = chD
                  (isGood,result) = ComputeFor(''.join(charsin))
                  if isGood:
                     result = result[0:36]         # this is what the assembler does...  (drop final byte)
                     if result[posnC] == sTarget[posnC] and result[posnD] == sTarget[posnD]:      # got one
                        validB[chB] = 1
                        validC[chC] = 1
                        validD[chD] = 1      
      print "All valid B at %i [%s]" % (posnB,validB.keys())
      print "All valid C at %i [%s]" % (posnC,validC.keys())
      print "All valid D at %i [%s]" % (posnD,validD.keys())
      # modify the posnC,D keys... but not the A or B
      valids[posnC] = ''.join(validC.keys())
      valids[posnD] = ''.join(validD.keys())
      # go for next
#      exit()      # XXX debug stop after one
      posnA -= 1
   f=open("valids","w+")
   f.write("NEW RUN OF VALIDS---------------------\n")
   f.write("%s" % valids)

>>> Then overnight sleep for 3 hours (3am to 6am... ) <<<

Saturday morning dawns, well grumpily drags itself from a bed,
... remembers there is a CTF and drinks coffee... back at computer...

So... LUCKILY Tom O'Brien is now online, fellow WHA ... !
Tom knows maths... so while I'm forcing in a second coffee... he quickly understands the maths and reverses things from the desired output back to the XNOR and thence to the input required.

So my main contribution was understanding the problem, and failing to brute it.
Tom actually solved it.

and quickly coded up:

def TomWasHere():
    # First python code, don't hate please!
    # We're going to moonwalk through the code...

    # From our initial input we need to reach the target_string.
    target_string = "From a seed a mighty trunk may grow."

    # The step before the final assertion we perform an XNOR on whatever string we have with the hardcoded xnorbits (at the top of this program).
    # As a result, we need the target_string in binary representation.
    target_binary = "010001100111001001101111011011010010000001100001001000000111001101100101011001010110010000100000011000010010000001101101011010010110011101101000011101000111100100100000011101000111001001110101011011100110101100100000011011010110000101111001001000000110011101110010011011110111011100101110"

    # Problem is, the binary taken to form the string is the first 36 bytes of a 37 byte value, so we're missing the bottom 8 bits.
    # We need to guess the bottom 8 bits, (probably by brute force), but lets start off with an initial guess of 00000000
    guessed_bits = "00000000"

    # The 37 byte string to XNOR with the xnorbits
    string_to_xnor = target_binary + guessed_bits

    # XNOR our target_string + guessed 8 bits. StringAnd is Peter Goode's attempt at an XNOR function, so blame him if stuff goes wrong.
    string_after_xnor = StringAnd(string_to_xnor, xnorbits)

    # Ok, so we now have a 37 byte value that the program would calculate when doing some weird additive and multiplicative function.
    # The gist of it is start at 0, add the value of the first byte (most significant), then for every next byte you multiply by 307
    # and add the byte's value. This means that after every iteration we have a value in the form 307*k + x, where 0 <= x < 256. It also
    # means that given a 36 byte input string we would end up calculating a 37 or 38 byte value (37 if the 36 byte value is less than about
    # half its max value).
    # 
    # The plan is to turn our reverse-engineered 37 byte value (technically still a string) into its decimal/hex representation,
    # calculate the largest multiple of 307 below it, and the difference should be 'x', 0 <= x < 256, the value of the last byte of the input
    # string. We should be able to repeat this process for all the remaining bytes to recover the initial input string required.

    # Calculate the value to start unwinding.
    value = int(string_after_xnor, 2)

    initial_string = ""

    while value > 0:
        # We want the difference between the value we calculated and the largest multiple of 307 below it, so take our value modulo 307.
        byte_found = value % 307

        # Make sure it's a valid byte, otherwise bad stuff might happen...
        assert(byte_found < 256)

        # Add the byte onto the string
        initial_string = chr(byte_found) + initial_string

        # Should be numerical!
        value = (value - byte_found) / 307


    return initial_string

result = "@keup@nds0lv3an0ther_ch@113nge"

And we have to fiddle a bit to get the first and last characters...

Flag !!