Time to start packing those presents for the holidays! We found this packed gift for you to open with the correct passphrase…
Quickly after opening this binary it becomes apparent that it is a VM executing custom bytecode using a central dispatcher loading the next instruction and just using a big jumptable to execute them.
It is a kind of stack-machine but has some “heap” space to save variables.
So time to brew some coffe and get started reversing!
I just stepped through the execution of each VM-instruction writing a dissasembler in python as i went along.
Coloring the dispatcher graph in IDA to keep my sanity and see that i was indeed making progress, this picture is a couple of hours in:
Figure 1 - Reversing the VM instructions
Custom VM analysis with radare2
First disable aslr for ease of revesing with echo 0 | sudo tee /proc/sys/kernel/randomize_va_space.
To start, we analyze the binary, continue until main, then after stack variables are setup and extend the main function to include the blocks executing the VM instructions.
aa
dcu main
dcu 0x555555554752
db 0x555555554752
afb+ 0x5555555546ca 0x555555554782 0x88e
Then we rename the local variables and code locations to make the disassembly more readable.
afvn loc_argc local_174h
afvn loc_argv local_180h
afvn loc_envp local_188h
afvn stackcookie local_8h
afn nopfunc @ 0x555555555010
f glob_argc @ 0x5555557561e0
f glob_argv @ 0x5555557561d8
f glob_envp @ 0x5555557561e8
afvn loc_flag local_164h
afvn loc_stack local_150h
afvn loc_sp local_160h
afvn loc_ip local_158h
f jumptable @ 0x5555555550b0
f continue @ 0x555555555004
f program @ 0x555555756020
Lastly we rename the memory locations used for VM execution
f sp @ rbp-0x160
f ip @ rbp-0x158
f stack @ rbp-0x150
f heap @ rbp-0x50
setup V! mode
What really sped up reversing the VM instructions was a custom panel setup for the visual panel mode V!. The panels show the VM instruction pointer, the next part of the VM program, the VM stack and heap area.
X close current panel - split panel e change name + command use w to into window mode move with hjlkl resize with HJ
VM instruction pointer
?v [ip] - program
Next VM instruction
px 9 @ [ip]
VM Stack area
pxQ 0x60 @ sp
VM heap area
pxQ 0x60 @ heap
This leads to the view shown here:
Figure 2 - Radare2 VM Panels
Break on specific VM instructions
What we can also do to greatly help reversing this kind of VM is breaking on specific VM instructions using radare2 conditional breakpoints We break at the point where the next byte of the VM program is moved into eax and compare the offset used with the VM-instruction we want to break at.
Example: break after first loop
f vm_ip=`?v [ip] - program`
f test=`vi vm_ip-0x89`
e cmd.hitinfo=0
(break_vmip,f vm_ip=`?v [ip] - program`,f test=`?vi vm_ip-0x0a6`,?= test)
db 0x555555554755
dbC 0x555555554755 .(break_vmip)
We got a disassembly!
Finally after reversing every instruction (and too much coffee) we can disassemble the whole program executed by the VM (please excuse my mnemonics):
0x000: cb 18000000 pushvar 0x18
0x005: 15 01000000 pushd 0x1
0x00a: dc signe
0x00b: 14 0800000000000000 pushq 0x8
0x014: 18 mult
0x015: df 01000000 push **argv
0x01a: 13 deref
0x01b: b0 add
0x01c: 13 deref
0x01d: 6f nop
0x01e: 23 storeup
0x01f: 14 0000000000000000 pushq 0x0
0x028: cb 20000000 pushvar 0x20
0x02d: 89 storedn
0x02e: d9 04000000 jump 0x33
0x033: cb 18000000 pushvar 0x18
0x038: 13 deref
0x039: d3 getchar
0x03a: 02 extbd
0x03b: 15 00000000 pushd 0x0
0x040: d6 ne
0x041: e2 0e000000 jnz 0x50
0x046: d9 04000000 jump 0x4b
0x04b: d9 5a000000 jump 0xa6
0x050: cb 20000000 pushvar 0x20
0x055: 52 deref
0x056: cb 20000000 pushvar 0x20
0x05b: 52 deref
0x05c: 15 10000000 pushd 0x10
0x061: 37 shl
0x062: cb 20000000 pushvar 0x20
0x067: 52 deref
0x068: 15 06000000 pushd 0x6
0x06d: 37 shl
0x06e: cb 18000000 pushvar 0x18
0x073: 13 deref
0x074: d3 getchar
0x075: ed extbq
0x076: fd add
0x077: fd add
0x078: c2 sub
0x079: cb 20000000 pushvar 0x20
0x07e: 89 storedn
0x07f: cb 18000000 pushvar 0x18
0x084: 15 01000000 pushd 0x1
0x089: dc signe
0x08a: 14 0100000000000000 pushq 0x1
0x093: 18 mult
0x094: cb 18000000 pushvar 0x18
0x099: 13 deref
0x09a: 24 add
0x09b: 23 storeup
0x09c: d9 96ffffff jump 0x33
0x0a1: d9 91ffffff jump 0x33
0x0a6: 14 0000000000000000 pushq 0x0
0x0af: cb 28000000 pushvar 0x28
0x0b4: 89 storedn
0x0b5: cb 18000000 pushvar 0x18
0x0ba: 15 01000000 pushd 0x1
0x0bf: dc signe
0x0c0: 14 0800000000000000 pushq 0x8
0x0c9: 18 mult
0x0ca: df 01000000 push **argv
0x0cf: 13 deref
0x0d0: b0 add
0x0d1: 13 deref
0x0d2: 6f nop
0x0d3: 23 storeup
0x0d4: d9 04000000 jump 0xd9
0x0d9: cb 18000000 pushvar 0x18
0x0de: 13 deref
0x0df: d3 getchar
0x0e0: 02 extbd
0x0e1: 15 00000000 pushd 0x0
0x0e6: d6 ne
0x0e7: e2 0e000000 jnz 0xf6
0x0ec: d9 04000000 jump 0xf1
0x0f1: d9 53000000 jump 0x145
0x0f6: cb 28000000 pushvar 0x28
0x0fb: 52 deref
0x0fc: 15 05000000 pushd 0x5
0x101: 37 shl
0x102: cb 28000000 pushvar 0x28
0x107: 52 deref
0x108: 15 1b000000 pushd 0x1b
0x10d: 10 shr
0x10e: 9f xor
0x10f: cb 18000000 pushvar 0x18
0x114: 13 deref
0x115: d3 getchar
0x116: ed extbq
0x117: 9f xor
0x118: cb 28000000 pushvar 0x28
0x11d: 89 storedn
0x11e: cb 18000000 pushvar 0x18
0x123: 15 01000000 pushd 0x1
0x128: dc signe
0x129: 14 0100000000000000 pushq 0x1
0x132: 18 mult
0x133: cb 18000000 pushvar 0x18
0x138: 13 deref
0x139: 24 add
0x13a: 23 storeup
0x13b: d9 9dffffff jump 0xd9
0x140: d9 98ffffff jump 0xd9
0x145: cb 20000000 pushvar 0x20
0x14a: 52 deref
0x14b: 14 195e213490d199fa pushq 0xfa99d19034215e19
0x154: 5f cmp
0x155: e2 09000000 jnz 0x15f
0x15a: d9 34000000 jump 0x18f
0x15f: cb 28000000 pushvar 0x28
0x164: 52 deref
0x165: 14 9b62b71f8ee30900 pushq 0x9e38e1fb7629b
0x16e: 5f cmp
0x16f: e2 09000000 jnz 0x179
0x174: d9 1a000000 jump 0x18f
0x179: cb 30000000 pushvar 0x30
0x17e: c1 00000000 loadstr 0x00
0x183: 6f nop
0x184: 23 storeup
0x185: 28 01000000 printf 0x01
0x18a: d9 04000000 jump 0x18f
0x18f: cb 38000000 pushvar 0x38
0x194: 15 00000000 pushd 0x0
0x199: 92 storeupdw
0x19a: d9 04000000 jump 0x19f
0x19f: cb 38000000 pushvar 0x38
0x1a4: 3d derefdw
0x1a5: b5 exit
Decompile the VM program
I then manually translated this program into C and confirmed correcteness of my C version by inspecting the real binary with radare2 We can now see clearly that the program takes our input and computes 2 different hash values from it which both have to match expected values.
#include <stdio.h>
#include <inttypes.h>
int main(int argc, char *argv[]) {
char *input = argv[1];
char *inpt = input;
uint64_t hsh1 = 0x0;
printf("LOOP1\n");
uint64_t shf1;
uint64_t shf2;
uint64_t add1;
uint64_t add2;
while ( *inpt != 0x00) {
printf("inpchar:\t%x\n", inpt[0]);
shf1 = hsh1 << 0x10;
shf2 = hsh1 << 0x06;
add1 = shf1 + shf2;
add2 = add1 + inpt[0];
hsh1 = add2 - hsh1;
inpt++;
printf("hsh1:\t 0x%.16" PRIx64 "\n", hsh1);
}
printf("\nLOOP 2\n");
inpt = input;
uint64_t hsh2 = 0x0;
uint64_t xor;
while ( *inpt != 0x00) {
printf("inpchar:\t%x\n", inpt[0]);
shf1 = hsh2 << 0x05;
shf2 = hsh2 >> 0x1b;
xor = shf1 ^ shf2;
hsh2 = inpt[0] ^ xor;
inpt++;
printf("hsh2:\t 0x%.16" PRIx64 "\n", hsh2);
}
if(hsh1 == 0xfa99d19034215e19) {
if(hsh2 == 0x9e38e1fb7629b) {
printf("You win!\n");
}
}
return 0;
}
Solving the VM program
I did not try to bruteforce this or manually reverse the algorithms but rather translated the pogram into SMT2 and threw it into boolector (the better and faster z3) A little python script was used to generate the solver script for different input lengths even though i was pretty confident the input needed to be 10 characters long judging from how the second hash-function output had a lot of leading zeros.
import sys
header = """
; input bounds
(declare-const lower (_ BitVec 64))
(assert (= lower #x0000000000000020))
(declare-const upper (_ BitVec 64))
(assert (= upper #x000000000000007A))
; start
(declare-const r00 (_ BitVec 64))
(assert (= r00 #x0000000000000000))
(declare-const s00 (_ BitVec 64))
(assert (= s00 #x0000000000000000))
"""
inputvar = "(declare-const i%.2i (_ BitVec 64))\n"
constrainin = "(assert (and (bvule i%.2i upper) (bvuge i%.2i lower)))\n"
inter_s = "(declare-const r%.2i (_ BitVec 64))\n"
inter_r = "(declare-const s%.2i (_ BitVec 64))\n"
compute_s = "(assert (= s%.2i (bvsub (bvadd (bvadd (bvshl s%.2i #x0000000000000010) (bvshl s%.2i #x0000000000000006)) i%.2i) s%.2i) ))\n"
compute_r = "(assert (= r%.2i (bvxor (bvxor (bvshl r%.2i #x0000000000000005) (bvlshr r%.2i #x000000000000001b)) i%.2i)))\n"
result = """
(assert (= s%.2i #xfa99d19034215e19))
(assert (= r%.2i #x0009e38e1fb7629b))
"""
"""
real problem:
(assert (= s%.2i #xfa99d19034215e19))
(assert (= r%.2i #x0009e38e1fb7629b))
AAAAABBBBCCCCDDDD
(assert (= s%.2i #x041981d75e0cc141))
(assert (= r%.2i #x304318ce4210180c))
ABCDEFGH
(assert (= s%.2i #xa4697030240be104))
(assert (= r%.2i #x00000218026390b0))
"""
footer = """
(check-sat)
(get-model)
"""
def genz3(inputlength):
with open("fullgen%s.smt2"%inputlength, "w") as f:
f.write(header)
for i in range(1,inputlength+1):
f.write(inputvar % i)
f.write(constrainin % (i,i))
f.write(inter_r % i)
f.write(inter_s % i)
f.write(compute_r % (i, i-1, i-1, i))
f.write(compute_s % (i, i-1, i-1, i, i-1))
f.write(result % (inputlength, inputlength))
f.write(footer)
if __name__ == "__main__":
if len(sys.argv) == 2:
print("Trying length %.2i" % int(sys.argv[1]))
genz3(int(sys.argv[1]))
else:
print("Usage python genz.py [inputlength]")
The resulting SMT2 script for 10 character input length:
; input bounds
(declare-const lower (_ BitVec 64))
(assert (= lower #x0000000000000020))
(declare-const upper (_ BitVec 64))
(assert (= upper #x000000000000007A))
; start
(declare-const r00 (_ BitVec 64))
(assert (= r00 #x0000000000000000))
(declare-const s00 (_ BitVec 64))
(assert (= s00 #x0000000000000000))
(declare-const i01 (_ BitVec 64))
(assert (and (bvule i01 upper) (bvuge i01 lower)))
(declare-const s01 (_ BitVec 64))
(declare-const r01 (_ BitVec 64))
(assert (= r01 (bvxor (bvxor (bvshl r00 #x0000000000000005) (bvlshr r00 #x000000000000001b)) i01)))
(assert (= s01 (bvsub (bvadd (bvadd (bvshl s00 #x0000000000000010) (bvshl s00 #x0000000000000006)) i01) s00) ))
(declare-const i02 (_ BitVec 64))
(assert (and (bvule i02 upper) (bvuge i02 lower)))
(declare-const s02 (_ BitVec 64))
(declare-const r02 (_ BitVec 64))
(assert (= r02 (bvxor (bvxor (bvshl r01 #x0000000000000005) (bvlshr r01 #x000000000000001b)) i02)))
(assert (= s02 (bvsub (bvadd (bvadd (bvshl s01 #x0000000000000010) (bvshl s01 #x0000000000000006)) i02) s01) ))
(declare-const i03 (_ BitVec 64))
(assert (and (bvule i03 upper) (bvuge i03 lower)))
(declare-const s03 (_ BitVec 64))
(declare-const r03 (_ BitVec 64))
(assert (= r03 (bvxor (bvxor (bvshl r02 #x0000000000000005) (bvlshr r02 #x000000000000001b)) i03)))
(assert (= s03 (bvsub (bvadd (bvadd (bvshl s02 #x0000000000000010) (bvshl s02 #x0000000000000006)) i03) s02) ))
(declare-const i04 (_ BitVec 64))
(assert (and (bvule i04 upper) (bvuge i04 lower)))
(declare-const s04 (_ BitVec 64))
(declare-const r04 (_ BitVec 64))
(assert (= r04 (bvxor (bvxor (bvshl r03 #x0000000000000005) (bvlshr r03 #x000000000000001b)) i04)))
(assert (= s04 (bvsub (bvadd (bvadd (bvshl s03 #x0000000000000010) (bvshl s03 #x0000000000000006)) i04) s03) ))
(declare-const i05 (_ BitVec 64))
(assert (and (bvule i05 upper) (bvuge i05 lower)))
(declare-const s05 (_ BitVec 64))
(declare-const r05 (_ BitVec 64))
(assert (= r05 (bvxor (bvxor (bvshl r04 #x0000000000000005) (bvlshr r04 #x000000000000001b)) i05)))
(assert (= s05 (bvsub (bvadd (bvadd (bvshl s04 #x0000000000000010) (bvshl s04 #x0000000000000006)) i05) s04) ))
(declare-const i06 (_ BitVec 64))
(assert (and (bvule i06 upper) (bvuge i06 lower)))
(declare-const s06 (_ BitVec 64))
(declare-const r06 (_ BitVec 64))
(assert (= r06 (bvxor (bvxor (bvshl r05 #x0000000000000005) (bvlshr r05 #x000000000000001b)) i06)))
(assert (= s06 (bvsub (bvadd (bvadd (bvshl s05 #x0000000000000010) (bvshl s05 #x0000000000000006)) i06) s05) ))
(declare-const i07 (_ BitVec 64))
(assert (and (bvule i07 upper) (bvuge i07 lower)))
(declare-const s07 (_ BitVec 64))
(declare-const r07 (_ BitVec 64))
(assert (= r07 (bvxor (bvxor (bvshl r06 #x0000000000000005) (bvlshr r06 #x000000000000001b)) i07)))
(assert (= s07 (bvsub (bvadd (bvadd (bvshl s06 #x0000000000000010) (bvshl s06 #x0000000000000006)) i07) s06) ))
(declare-const i08 (_ BitVec 64))
(assert (and (bvule i08 upper) (bvuge i08 lower)))
(declare-const s08 (_ BitVec 64))
(declare-const r08 (_ BitVec 64))
(assert (= r08 (bvxor (bvxor (bvshl r07 #x0000000000000005) (bvlshr r07 #x000000000000001b)) i08)))
(assert (= s08 (bvsub (bvadd (bvadd (bvshl s07 #x0000000000000010) (bvshl s07 #x0000000000000006)) i08) s07) ))
(declare-const i09 (_ BitVec 64))
(assert (and (bvule i09 upper) (bvuge i09 lower)))
(declare-const s09 (_ BitVec 64))
(declare-const r09 (_ BitVec 64))
(assert (= r09 (bvxor (bvxor (bvshl r08 #x0000000000000005) (bvlshr r08 #x000000000000001b)) i09)))
(assert (= s09 (bvsub (bvadd (bvadd (bvshl s08 #x0000000000000010) (bvshl s08 #x0000000000000006)) i09) s08) ))
(declare-const i10 (_ BitVec 64))
(assert (and (bvule i10 upper) (bvuge i10 lower)))
(declare-const s10 (_ BitVec 64))
(declare-const r10 (_ BitVec 64))
(assert (= r10 (bvxor (bvxor (bvshl r09 #x0000000000000005) (bvlshr r09 #x000000000000001b)) i10)))
(assert (= s10 (bvsub (bvadd (bvadd (bvshl s09 #x0000000000000010) (bvshl s09 #x0000000000000006)) i10) s09) ))
(assert (= s10 #xfa99d19034215e19))
(assert (= r10 #x0009e38e1fb7629b))
(check-sat)
(get-model)
$ boolector -m -x jackinthebox.smt2 | grep " i"
(define-fun i01 () (_ BitVec 64) #x000000000000004d)
(define-fun i02 () (_ BitVec 64) #x0000000000000040)
(define-fun i03 () (_ BitVec 64) #x0000000000000072)
(define-fun i04 () (_ BitVec 64) #x0000000000000079)
(define-fun i05 () (_ BitVec 64) #x000000000000002d)
(define-fun i06 () (_ BitVec 64) #x0000000000000058)
(define-fun i07 () (_ BitVec 64) #x000000000000006d)
(define-fun i08 () (_ BitVec 64) #x0000000000000061)
(define-fun i09 () (_ BitVec 64) #x0000000000000035)
(define-fun i10 () (_ BitVec 64) #x0000000000000035)
...
Now we just need to translate the values into ascii and wrap it in AOTW{} to get our flag!
In [2]: binascii.unhexlify("4d4072792d586d613535")
Out[2]: b'M@ry-Xma55'
All in all it was very time consuming and there is probably a faster way to solve this but a lot was learned!