Write-ups ASIS Final – Fake with Triton

Fake, 150 pts

Get the binary from github.

We will use Triton to do this challenge.

Triton uses PinTools and Z3 to help resolving reverse challenges.

If you have never used Triton, do it ASAP because it is a great tool that use symbolic execution.

Let’s get back to our binary.

When we run it we have nothing displayed.

If we put some string as arguments it doesn’t show anything neither. If we try with numbers it display some encrypted string.

So let’s check in IDA what the code looks like:

Screen Shot 2015-10-13 at 16.54.17

 

It is not very sexy and very interesting to reverse. So let’s call Triton to help.

Triton is useful when you have some string that should be equal to another or have some equity to satisfy.

Here we don’t have anything like that. But we can guess that puts(&v5) will display the 5 variables declared and that it will display the flag.

We know that the flag start with “ASIS{“, which is 5 chars and our variable can contain 8.

We will use Triton (even through it is not really a complicated equation) to solve our problem.

So first we have to find two things:

Where is v5 set and v5 after all the computations done with it.

Screen Shot 2015-10-13 at 17.03.29

We can see at 0x4004AC that we put into r8 the number get from strol.

At 0x4004AF we have done the computation so we have the final value in RAX register.

So to summarize in our first equation we will have:

x = r8 (0x4004AC)

our equation should be equal to 0x???7b53495341 where ??? is our last unknown chars (and we will loop through one of it)

To do that with Triton:

from triton import *

import smt2lib
import os, sys
from elftools.elf.elffile import ELFFile


FILENAME="fake"
def syscallEntry(instruction):


    if 0x4004ac==instruction.getAddress():
        convertRegToSymVar(IDREF.REG.R8,64)

    if 0x4004af==instruction.getAddress():
        symbolicId = getRegSymbolicID(IDREF.REG.RAX)

        raxExpr = getFullExpression(getSymExpr(symbolicId).getAst())
        for i in range(28,120):

            conditions =  list()
            conditions.append(smt2lib.smtAssert(smt2lib.bvugt(raxExpr, smt2lib.bv(32, 64))))
            conditions.append( smt2lib.smtAssert(smt2lib.equal(raxExpr, smt2lib.bv(int("0x"+str(i)+"7b53495341",16), 64))))
            expr = smt2lib.compound(conditions)

            model = getModel(expr)
            try:
                print {k: "0x%x, '%c'" % (v, chr(int(str(hex(v)).rstrip("0"),16))) for k, v in model.items()}
            except :
                print {k: "%s " % (str(hex(v)).rstrip("0")) for k, v in model.items()}




if __name__ == '__main__':
    with open(FILENAME, 'rb') as f:
        elffile = ELFFile(f)
        header = elffile.header
        print hex(header["e_entry"])

    # Start the symbolic analysis from the entry point
    startAnalysisFromAddr(header["e_entry"])

    # Add a callback.
    addCallback(syscallEntry, IDREF.CALLBACK.AFTER)

    # Run the instrumentation - Never returns
    runProgram()


We will explain the important part:

if 0x4004ac==instruction.getAddress():
        convertRegToSymVar(IDREF.REG.R8,64)

Here we define X_initial=R8 for the specific address. So Triton will know that it is our unknown value. (SymVar_0)

if 0x4004af==instruction.getAddress():
        symbolicId = getRegSymbolicID(IDREF.REG.RAX)

Then for the other address we will resolve the equation by saying that RAX is our X_final.

We loop through 28 to 120 to have some data for ?? value and we display result:

# triton fake.py ./fake 123
{'SymVar_0': '0xa4974e05e4d48cc7L '}
{'SymVar_0': '0x545d5505e4d48cc7 '}
{'SymVar_0': '0x22c78605e4d48cc7 '}
{'SymVar_0': '0xd28d8d05e4d48cc7L '}
{'SymVar_0': '0x82539405e4d48cc7L '}
{'SymVar_0': '0x32199b05e4d48cc7 '}
{'SymVar_0': '0xe1dfa205e4d48cc7L '}
{'SymVar_0': '0x91a5a905e4d48cc7L '}
{'SymVar_0': '0x416bb005e4d48cc7 '}
{'SymVar_0': '0xf131b705e4d48cc7L '}
{'SymVar_0': '0xa0f7be05e4d48cc7L '}
{'SymVar_0': '0x50bdc505e4d48cc7 '}
{'SymVar_0': '0x1f27f605e4d48cc7 '}
{'SymVar_0': '0xceedfd05e4d48cc7L '}
{'SymVar_0': '0x7eb40405e4d48cc7 '}
{'SymVar_0': '0x2e7a0b05e4d48cc7 '}
{'SymVar_0': '0xde401205e4d48cc7L '}
{'SymVar_0': '0x8e061905e4d48cc7L '}
{'SymVar_0': '0x3dcc2005e4d48cc7 '}
{'SymVar_0': '0xed922705e4d48cc7L '}
{'SymVar_0': '0x9d582e05e4d48cc7L '}
{'SymVar_0': '0x4d1e3505e4d48cc7 '}
{'SymVar_0': '0x1b886605e4d48cc7 '}
{'SymVar_0': '0xcb4e6d05e4d48cc7L '}
{'SymVar_0': '0x7b147405e4d48cc7 '}
{'SymVar_0': '0x2ada7b05e4d48cc7 '}
{'SymVar_0': '0xdaa08205e4d48cc7L '}
{'SymVar_0': '0x8a668905e4d48cc7L '}
{'SymVar_0': '0x3a2c9005e4d48cc7 '}
{'SymVar_0': '0xe9f29705e4d48cc7L '}
{'SymVar_0': '0x99b89e05e4d48cc7L '}
{'SymVar_0': '0x497ea505e4d48cc7 '}
{'SymVar_0': '0x17e8d605e4d48cc7 '}
{'SymVar_0': '0xc7aedd05e4d48cc7L '}
{'SymVar_0': '0x7774e405e4d48cc7 '}
{'SymVar_0': '0x273aeb05e4d48cc7 '}
{'SymVar_0': '0xd700f205e4d48cc7L '}
{'SymVar_0': '0x86c6f905e4d48cc7L '}
{'SymVar_0': '0x368d0005e4d48cc7 '}
{'SymVar_0': '0xe6530705e4d48cc7L '}
{'SymVar_0': '0x96190e05e4d48cc7L '}
{'SymVar_0': '0x45df1505e4d48cc7 '}
{'SymVar_0': '0x14494605e4d48cc7 '}
{'SymVar_0': '0xc40f4d05e4d48cc7L '}
{'SymVar_0': '0x73d55405e4d48cc7 '}
{'SymVar_0': '0x239b5b05e4d48cc7 '}
{'SymVar_0': '0xd3616205e4d48cc7L '}
{'SymVar_0': '0x83276905e4d48cc7L '}
{'SymVar_0': '0x32ed7005e4d48cc7 '}
{'SymVar_0': '0xe2b37705e4d48cc7L '}
{'SymVar_0': '0x92797e05e4d48cc7L '}
{'SymVar_0': '0x423f8505e4d48cc7 '}
{'SymVar_0': '0x10a9b605e4d48cc7 '}
{'SymVar_0': '0xc06fbd05e4d48cc7L '}
{'SymVar_0': '0x7035c405e4d48cc7 '}
{'SymVar_0': '0x1ffbcb05e4d48cc7 '}
{'SymVar_0': '0xcfc1d205e4d48cc7L '}
{'SymVar_0': '0x7f87d905e4d48cc7 '}
{'SymVar_0': '0x2f4de005e4d48cc7 '}
{'SymVar_0': '0xdf13e705e4d48cc7L '}
{'SymVar_0': '0x8ed9ee05e4d48cc7L '}
{'SymVar_0': '0x3e9ff505e4d48cc7 '}
{'SymVar_0': '0xd0a2605e4d48cc7 '}
{'SymVar_0': '0xbcd02d05e4d48cc7L '}
{'SymVar_0': '0x6c963405e4d48cc7 '}
{'SymVar_0': '0x1c5c3b05e4d48cc7 '}
{'SymVar_0': '0xcc224205e4d48cc7L '}
{'SymVar_0': '0x7be84905e4d48cc7 '}
{'SymVar_0': '0x2bae5005e4d48cc7 '}
{'SymVar_0': '0xdb745705e4d48cc7L '}
{'SymVar_0': '0x8b3a5e05e4d48cc7L '}
{'SymVar_0': '0x3b006505e4d48cc7 '}
{'SymVar_0': '0xf3ad3605e4d48cc7L '}
{'SymVar_0': '0xa3733d05e4d48cc7L '}
{'SymVar_0': '0x53394405e4d48cc7 '}
{'SymVar_0': '0x2ff4b05e4d48cc7 '}
{'SymVar_0': '0xb2c55205e4d48cc7L '}
{'SymVar_0': '0x628b5905e4d48cc7 '}
{'SymVar_0': '0x12516005e4d48cc7 '}
{'SymVar_0': '0xc2176705e4d48cc7L '}
{'SymVar_0': '0x71dd6e05e4d48cc7 '}
{'SymVar_0': '0x21a37505e4d48cc7 '}
{'SymVar_0': '0xf00da605e4d48cc7L '}
{'SymVar_0': '0x9fd3ad05e4d48cc7L '}
{'SymVar_0': '0x4f99b405e4d48cc7 '}
{'SymVar_0': '0xff5fbb05e4d48cc7L '}
{'SymVar_0': '0xaf25c205e4d48cc7L '}
{'SymVar_0': '0x5eebc905e4d48cc7 '}
{'SymVar_0': '0xeb1d005e4d48cc7 '}
{'SymVar_0': '0xbe77d705e4d48cc7L '}
{'SymVar_0': '0x6e3dde05e4d48cc7 '}
{'SymVar_0': '0x1e03e505e4d48cc7 '}
��3

We can see that we always have a static part : 0x05e4d48cc7

We can try to run the program with these argument to see what happens:

# ./fake `rax2 0x05e4d48cc7`
ASIS{f5f7af556bd6973bd6f2687280a243d9}

And you got the flag.

Triton was a bit overkill for this challenge, we could have done it clearly without it but it is still interesting to do it with Triton.

If we have to go through the other variables to find ascii result for example it would have been useful.

Write-ups DefCamp 2015 – r100 with triton

We were given a binary (downloadable from github).

 

Let’s run it:

$ ./r100.bin 
Enter the password: AAAAAA
Incorrect password!

 

We want to check the source code in IDA:

Screen Shot 2015-10-14 at 10.40.06

 

It doesn’t look really complicated but it is a perfect opportunity to have fun with Triton!

To use Triton we need to know two things:

  1. What is my X in the equation? (Obviously it is the input here…)
  2. Where should I need to solve the equation?

So let’s check the disassembly code for that. Below is the loop, where “pass” is our input.

Screen Shot 2015-10-14 at 10.34.57

We can see that our X will be at 0x400781 (RAX value right after the instruction).

Then we want to solve the equation at 0x40078b (you can do it before too, it’s not a static choice…)

So we will use the snapshot features of python to do the following steps:

  1. At 0x40072d (beginning of the loop) : Take a snapshot so we can come back here later and set i value
  2. At 0x400781 : Set RAX as my X in the equation
  3. At 0x40078b: Resolve my equation with Z3. If i < 12, restore the snapshot and increment i. Restoring the snapshot take us back to point 1)

Translating that into python with Triton:

from triton import *

import smt2lib
import os, sys
from elftools.elf.elffile import ELFFile

FILENAME = 'r100'

password  = ""
i=0

def callbackBefore(instruction):
    global password

    global i
    if instruction.getAddress()==0x40072d and isSnapshotEnabled()==False:
        print "[+] Take Snapshot"
        takeSnapshot()
    if instruction.getAddress()==0x40072d:
        setMemValue(instruction.getOperands()[1].getMem().getAddress(),1,i)
    if instruction.getAddress()==0x4007a7:
        print "[+]Password: %s" %(password)


def syscallEntry(instruction):
    global i
    global password

    if instruction.getAddress()==0x400781:
        convertRegToSymVar(IDREF.REG.RAX,64)


    if instruction.getAddress()==0x40078b:
        operandR = instruction.getOperands()[1]
        operandL = instruction.getOperands()[0]
        equalTo = 0x00
        equalTo=operandR.getImm().getValue()

        symbolicId = getRegSymbolicID(operandL.getReg().getId())
        raxExpr = getFullExpression(getSymExpr(symbolicId).getAst())
        conditions =  list()
        conditions.append( smt2lib.smtAssert(smt2lib.equal(raxExpr, smt2lib.bv(equalTo, 64))))
        expr = smt2lib.compound(conditions)

        model = getModel(expr)
        print {k: "0x%x, '%c'" % (v, chr(int(str(hex(v)).rstrip("0"),16))) for k, v in model.items()
}
        for k, v in model.items():
            c = chr(int(str(hex(v)).rstrip("0"),16))
            print "[+] Adding %c to password" %(c)
            password += c
            i += 1
            if i<12:
                print "[+] Restore snapshot"
                restoreSnapshot()


if __name__ == '__main__':
    with open(FILENAME, 'rb') as f:
        elffile = ELFFile(f)
        header = elffile.header

    # Start the symbolic analysis from the entry point
    startAnalysisFromAddr(header["e_entry"])

    # Add a callback.
    addCallback(syscallEntry, IDREF.CALLBACK.AFTER)
    addCallback(callbackBefore, IDREF.CALLBACK.BEFORE)

    # Run the instrumentation - Never returns
    runProgram()

Let’s run it. One detail, we didn’t set a static value for our input so we need to manually give an input of at least 11 chars:

 

$ echo "11111111111111"|triton r100.blog.py ./r100
[+] Take Snapshot
{'SymVar_0': "0x43, 'C'"}
[+] Adding C to password
[+] Restore snapshot
{'SymVar_0': "0x6f, 'o'"}
[+] Adding o to password
[+] Restore snapshot
{'SymVar_0': "0x64, 'd'"}
[+] Adding d to password
[+] Restore snapshot
{'SymVar_0': "0x65, 'e'"}
[+] Adding e to password
[+] Restore snapshot
{'SymVar_0': "0x5f, '_'"}
[+] Adding _ to password
[+] Restore snapshot
{'SymVar_0': "0x54, 'T'"}
[+] Adding T to password
[+] Restore snapshot
{'SymVar_0': "0x61, 'a'"}
[+] Adding a to password
[+] Restore snapshot
{'SymVar_0': "0x6c, 'l'"}
[+] Adding l to password
[+] Restore snapshot
{'SymVar_0': "0x6b, 'k'"}
[+] Adding k to password
[+] Restore snapshot
{'SymVar_0': "0x65, 'e'"}
[+] Adding e to password
[+] Restore snapshot
{'SymVar_0': "0x72, 'r'"}
[+] Adding r to password
[+] Restore snapshot
{'SymVar_0': "0x73, 's'"}
[+] Adding s to password
[+]Password: Code_Talkers
Enter the password: Incorrect password!

$ echo "Code_Talkers" | ./r100
Enter the password: Nice!

We could do the script more specific and more “automatic” with the taint system of triton.

I will try to do that in another write-ups.