> 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:
![Reversing the VM instructions](https://www.sigflag.at/assets/posts/jackinthebox/halfway.png)
## 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.
```aadcu maindcu 0x555555554752db 0x555555554752afb+ 0x5555555546ca 0x555555554782 0x88e```Then we rename the local variables and code locations to make the disassembly more readable.
```afvn loc_argc local_174hafvn loc_argv local_180hafvn loc_envp local_188hafvn stackcookie local_8h
afn nopfunc @ 0x555555555010
f glob_argc @ 0x5555557561e0f glob_argv @ 0x5555557561d8f glob_envp @ 0x5555557561e8
afvn loc_flag local_164hafvn loc_stack local_150hafvn loc_sp local_160hafvn loc_ip local_158h
f jumptable @ 0x5555555550b0f continue  @ 0x555555555004f program   @ 0x555555756020```
Lastly we rename the memory locations used for VM execution 
```f sp @  rbp-0x160f ip @ rbp-0x158f stack @ rbp-0x150f heap @ rbp-0x50```
### setup `V!` modeWhat 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 + commanduse `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:
![Radare2 VM Panels](https://www.sigflag.at/assets/posts/jackinthebox/vm-radare2.png)
### 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](https://github.com/radare/radare2/blob/master/doc/debug.md)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 0x555555554755dbC 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	0x180x005:	 15  01000000           pushd  	0x10x00a:	 dc                     signe0x00b:	 14  0800000000000000   pushq  	0x80x014:	 18                     mult0x015:	 df  01000000           push   	**argv0x01a:	 13                     deref0x01b:	 b0                     add0x01c:	 13                     deref0x01d:	 6f                     nop0x01e:	 23                     storeup0x01f:	 14  0000000000000000   pushq  	0x00x028:	 cb  20000000           pushvar	0x200x02d:	 89                     storedn0x02e:	 d9  04000000           jump   	0x330x033:	 cb  18000000           pushvar	0x180x038:	 13                     deref0x039:	 d3                     getchar0x03a:	 02                     extbd0x03b:	 15  00000000           pushd  	0x00x040:	 d6                     ne0x041:	 e2  0e000000           jnz    	0x500x046:	 d9  04000000           jump   	0x4b0x04b:	 d9  5a000000           jump   	0xa60x050:	 cb  20000000           pushvar	0x200x055:	 52                     deref0x056:	 cb  20000000           pushvar	0x200x05b:	 52                     deref0x05c:	 15  10000000           pushd  	0x100x061:	 37                     shl0x062:	 cb  20000000           pushvar	0x200x067:	 52                     deref0x068:	 15  06000000           pushd  	0x60x06d:	 37                     shl0x06e:	 cb  18000000           pushvar	0x180x073:	 13                     deref0x074:	 d3                     getchar0x075:	 ed                     extbq0x076:	 fd                     add0x077:	 fd                     add0x078:	 c2                     sub0x079:	 cb  20000000           pushvar	0x200x07e:	 89                     storedn0x07f:	 cb  18000000           pushvar	0x180x084:	 15  01000000           pushd  	0x10x089:	 dc                     signe0x08a:	 14  0100000000000000   pushq  	0x10x093:	 18                     mult0x094:	 cb  18000000           pushvar	0x180x099:	 13                     deref0x09a:	 24                     add0x09b:	 23                     storeup0x09c:	 d9  96ffffff           jump   	0x330x0a1:	 d9  91ffffff           jump   	0x330x0a6:	 14  0000000000000000   pushq  	0x00x0af:	 cb  28000000           pushvar	0x280x0b4:	 89                     storedn0x0b5:	 cb  18000000           pushvar	0x180x0ba:	 15  01000000           pushd  	0x10x0bf:	 dc                     signe0x0c0:	 14  0800000000000000   pushq  	0x80x0c9:	 18                     mult0x0ca:	 df  01000000           push   	**argv0x0cf:	 13                     deref0x0d0:	 b0                     add0x0d1:	 13                     deref0x0d2:	 6f                     nop0x0d3:	 23                     storeup0x0d4:	 d9  04000000           jump   	0xd90x0d9:	 cb  18000000           pushvar	0x180x0de:	 13                     deref0x0df:	 d3                     getchar0x0e0:	 02                     extbd0x0e1:	 15  00000000           pushd  	0x00x0e6:	 d6                     ne0x0e7:	 e2  0e000000           jnz    	0xf60x0ec:	 d9  04000000           jump   	0xf10x0f1:	 d9  53000000           jump   	0x1450x0f6:	 cb  28000000           pushvar	0x280x0fb:	 52                     deref0x0fc:	 15  05000000           pushd  	0x50x101:	 37                     shl0x102:	 cb  28000000           pushvar	0x280x107:	 52                     deref0x108:	 15  1b000000           pushd  	0x1b0x10d:	 10                     shr0x10e:	 9f                     xor0x10f:	 cb  18000000           pushvar	0x180x114:	 13                     deref0x115:	 d3                     getchar0x116:	 ed                     extbq0x117:	 9f                     xor0x118:	 cb  28000000           pushvar	0x280x11d:	 89                     storedn0x11e:	 cb  18000000           pushvar	0x180x123:	 15  01000000           pushd  	0x10x128:	 dc                     signe0x129:	 14  0100000000000000   pushq  	0x10x132:	 18                     mult0x133:	 cb  18000000           pushvar	0x180x138:	 13                     deref0x139:	 24                     add0x13a:	 23                     storeup0x13b:	 d9  9dffffff           jump   	0xd90x140:	 d9  98ffffff           jump   	0xd90x145:	 cb  20000000           pushvar	0x200x14a:	 52                     deref0x14b:	 14  195e213490d199fa   pushq  	0xfa99d19034215e190x154:	 5f                     cmp0x155:	 e2  09000000           jnz    	0x15f0x15a:	 d9  34000000           jump   	0x18f0x15f:	 cb  28000000           pushvar	0x280x164:	 52                     deref0x165:	 14  9b62b71f8ee30900   pushq  	0x9e38e1fb7629b0x16e:	 5f                     cmp0x16f:	 e2  09000000           jnz    	0x1790x174:	 d9  1a000000           jump   	0x18f0x179:	 cb  30000000           pushvar	0x300x17e:	 c1  00000000           loadstr	0x000x183:	 6f                     nop0x184:	 23                     storeup0x185:	 28  01000000           printf 	0x010x18a:	 d9  04000000           jump   	0x18f0x18f:	 cb  38000000           pushvar	0x380x194:	 15  00000000           pushd  	0x00x199:	 92                     storeupdw0x19a:	 d9  04000000           jump   	0x19f0x19f:	 cb  38000000           pushvar	0x380x1a4:	 3d                     derefdw0x1a5:	 b5                     exit```
## Decompile the VM programI 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`](https://boolector.github.io/) (the better and faster `z3`) 
```; 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!