## Reverse - EmojiVM
We are given a virtual machine interpreter and a bytecode file. Running thebytecode results in a password prompt. The goal appears to be to figure out thepassword.
Let's dig into the interpreter:
```__int64 __fastcall main(__int64 argc, char **argv, char **envp){  ...  locale_unbuffer_timeout();  init_emoji_tables();  read_bytecode(&bytecode, argv[1]);  execute_bytecode(&bytecode);  ...}```
There are four functions involved:
* `locale_unbuffer_timeout` configures the terminal.* `init_emoji_tables` is a giant wall of text that goes like this:
```v1 = 0x1F233;*(_DWORD *)std_map_operator[](&emoji_code_table, &v1) = 1;...v1 = 0x1F600;*(_DWORD *)std_map_operator[]v2(&emoji_data_table, &v1) = 0;```
All the hex values are emoji encodings, as can be easily verified with python's`chr` function.
* `read_bytecode` reads bytecode into an `std::string`.* `execute_bytecode` is an interpreter loop.
Inspecting `execute_bytecode` reveals the following:
* EmojiVM has only two registers: program counter and stack pointer. Program  counter counts characters, not bytes.* There is a stack which can contain up to 1024 qwords. The granularity is 1  qword.* There are 10 so-called gptrs, which are dynamically sized buffers of up to  1500 bytes. The granularity is 1 byte.* 23 emojis are mapped to the following commands:  * `0x01`: no-op.  * `0x02`: addition: pop two elements, push their sum.  * `0x03`: subtraction.  * `0x04`: multiplication.  * `0x05`: remainder.  * `0x06`: bitwise xor.  * `0x07`: bitwise and.  * `0x08`: less-than comparison: pop two elements, push 1 if the first one is  less than the second one, push 0 otherwise.  * `0x09`: equality comparison.  * `0x0A`: jump: pop an element, set pc to its value.  * `0x0B`: jump if not zero: pop two elements, jump to the first one if the    second one is not zero, jump to the next instruction otherwise.  * `0x0C`: jump if zero.  * `0x0D`: push a value in range 0-10. The value is encoded as a smiley using    a separate table, and follows the opcode.  * `0x0E`: pop.  * `0x0F`: load from allocated gptr: pop two elements, use the first one as  gptr index, use the second one as offset into gptr, push the corresponding  byte.  * `0x10`: store to allocated gptr.  * `0x11`: allocate gptr: pop an element, find an unallocated gptr slot,  allocate gptr of that size.  * `0x12`: unallocate gptr.  * `0x13`: read from stdin to gptr.  * `0x14`: write gptr to stdout.  * `0x15`: write LSBs of stack values to stdout as characters until 0 is  encountered.  * `0x16`: write stack top to stdout as a decimal number, this will not pop the  value.  * `0x17`: exit.
Now it's not so hard to write an emulator in python. By running the program andinspecting the trace we find out the following:
* That's how numbers larger than 10 are normally made:
```0x00003 PUSH 60x00005 PUSH 100x00007 MUL [10 6]0x00008 PUSH 0      # what a lazy codegen :P0x0000A ADD [0 60]```
* The password is read into gptr 0.* The sequence at `0x01A9E` is essentially `strlen()`, the length must be 24  characters.* The sequence at `0x02166` prints a crying face. That's where we end up when  we fail length and other checks.* Each input character is checked differently. For example, that's the condition  for the 11th character: `(4 ^ 101 ^ flag[11]) & 255 == 4`.
We're too lazy for this, aren't we? Symbolic execution with `z3` to the rescue!Let's modify the interpreter to keep track of 24 symbolic characters and feedthem in when asked:
```predefined_inputs = [[z3.BitVec(f'flag[{i}]', 8) for i in range(24)]]...if code == 0x13:    gptr_element = gptr[stack.pop()]    if len(predefined_inputs) == 0:        gptr_element[:len(raw)] = input().encode()    else:        gptr_element[:len(raw)] = predefined_inputs.pop(0)```
Now fix up a few operations to deal with the symbolic world, e.g. replace `==`,which would otherwise end up doing comparison of Python objects, with a littlebit more elaborate
```def eq(a, b):    if type(a) is int:        cond = b == a    else:        cond = a == b    if type(cond) is bool:        return 1 if cond else 0    else:        return z3.If(cond, 1, 0)```
This would keep us in the concrete world as long as possible, slipping intosymbolic world only when necessary. What to do with `jnz`? Well, the propersolution would be to fork two symbolic states and explore them both. But the`chal.evm` logic is too simple for that. Let's just ask z3 to produce two samplevalues for "then" and "else" branches:
```can_be_0 = check(arg1 == 0)if str(can_be_0) == 'unsat':    pc = arg0else:    m0 = model(can_be_0)    cannot_be_0 = check(arg1 != 0)    if str(cannot_be_0) == 'unsat':        pc += 1    else:        m1 = model(cannot_be_0)        print(m0)        print(m1)        raise Exception('Too dumb to fork')```
We get:
```{flag[11]: '\x80', flag[12]: '\x01', ...}{flag[11]: 'e', flag[12]: '\x01', ...}Exception: Too dumb to fork```
Well, now we know 11th character is `e` (no way it's `\x80`). Now let's go backto symbolic value initialization, set
```predefined_inputs[0][11] = ord(b'e')```
and repeat this manually 23 more times. Of course a more elegant solution, whichwould involve determining which of the two sets of possible values contains justone element, is possible, but we just want to solve the goddamn riddle, aren'twe?
Filling all 24 array entries reveals the password, and said password makes thebytecode print the flag!