Rating:
# SECCON CTF Quals - 2019
## Rev / 225 - follow-me
> I have an execution trace of calc, but I forgot what I inputted. Can you submit the input (formula) which follows my execution trace to my server?
>
> Challenge server
>
> Server compares branch instructions' behavior of your input's and original execution traces, and gives you flag if these are the same.
>
> NOTE: You MUST NOT attack challenge server (including too frequent access).
>
> Location: http://follow-me.chal.seccon.jp/
>
> Sample curl command to submit formula: curl -q -H 'Content-Type:application/json' -d "{\"input\": \"your formula comes here\"}" http://follow-me.chal.seccon.jp/submit/quals/0
>
> Attached files
>
> * Executed binary (excluding dynamic libraries): [calc](calc)
> * Execution trace generated by tracer: [calc.trace](./calc.trace)
> * Source code of tracer developed on the top of Pin: [branchtrace.cpp](./branchtrace.cpp)
### Solution
By [@jaidTw](https://github.com/jaidTw)
Credits to [@raagi](https://github.com/nashi5566)
Three files were given：
* Executable
* Source code of trace using Pin framework
* Output of the tracer
We must craft the input to make the program generate a same trace as the one given to get the flag.
Here' s the format of the output trace：
```json
[
{"event": "image_load", "image_name": "/home/tomori/follow-me/build/sample/calc", "image_id": 1, "base_addr": "0x55f6b4d44000", "image_size": "0x1377"},
{"event": "image_load", "image_name": "/lib64/ld-linux-x86-64.so.2", "image_id": 2, "base_addr": "0x7f13ae220000", "image_size": "0x26c23"},
{"event": "image_load", "image_name": "[vdso]", "image_id": 3, "base_addr": "0x7ffc2b775000", "image_size": "0x100a"},
{"event": "image_load", "image_name": "/lib/x86_64-linux-gnu/libc.so.6", "image_id": 4, "base_addr": "0x7f1399a39000", "image_size": "0x3f0adf"},
{"event": "branch", "inst_addr": "0x55f6b4d445de", "next_inst_addr": "0", "branch_taken": true},
{"event": "branch", "inst_addr": "0x55f6b4d44f44", "next_inst_addr": "0", "branch_taken": false},
{"event": "branch", "inst_addr": "0x55f6b4d44765", "next_inst_addr": "0", "branch_taken": true},
...
{"event": "exit", "exit_code": 0}
]
```
All branches were recorded, thus out input should make program run in an identical control flow.
First, by reversing the binary, we know it's a simple calculator, which input is a postfix expression, functions including `+`, `-`, `*`, `m`(min), `M`(max) and `C`(combination).
Then, we have to find out the meaning of those addresses. Find the instruction in the binary by using last 12 bits of address (didn't affected by ASLR), wrtie down their branch type and whether if they were taken.
We use this [script](./trans.py) to translate the output into a more readable form.
```
# main if ( argc <= 1 ) False
# malloc@plt True
# calloc@plt True
# Unconditional
# formula_parse while( *f ) True
# formula_parse if ( *f == ',' ) False
# formula_parse if ( chr <= '/' ) False
# formula_parse if ( chr > '9' ) False
# Unconditional
# formula_parse while( *f ) True
# formula_parse if ( *f == ',' ) False
# formula_parse if ( chr <= '/' ) False
# formula_parse if ( chr > '9' ) False
# Unconditional
# formula_parse while( *f ) True
# formula_parse if ( *f == ',' ) False
# formula_parse if ( chr <= '/' ) False
# formula_parse if ( chr > '9' ) False
# Unconditional
# formula_parse while( *f ) True
# formula_parse if ( *f == ',' ) True
# formula_parse ( type == 1 ) True
# push if ( s->len > 999u ) True
# Unconditional
```
We split the trace by the main `while` loop in `formula_parse`, now each block stands for an iteration, and there are many same blocks. Each type of block stands for a character (e.g. the block in the code above stands for digit, digit, digit, comma, respectively.), which means we can substitute these block with characters after we find their mapping.
By checking those branch, finnaly we get the format of input:
```
DDD,DDD,DDD,DDD,DDD,DDDD,DDD,mm-mM-DDD,DDD,DDD,mm-DDD,DDD,DDD,DDD,DDD,-+(4)-M+(8)DDD,DDD,DDD,mm*(1:6)
D : digit
+(n) : +, iterates n times
*(n:m) *, add inside the n-th iteration of the outer loop iterates m times
```
We have to fill in the numbers, to make it satisfy the constraints related to the repetition times in `add` and `mul`.
* Iterations of the loop in `add` equals the ones digit of the second parameter.
* Iterations of the outer loop in `mul` equals the value of the second parameter. The first parameter of `mul` is pass to second parameter of `add` in the inner loop, thus the iterations of the innter loop equals to the ones digit of the first parameter of `mul`.
It's not hard to satisfy these constaints, here's our solution(with indentation and parentheses)
```
[
[
[
[
008,[
000,[
000,[
000,[
000,[
0000,000,m
]m
]-
]m
]M
]-
]
[
000,[
000,000,m
]m
]
]-
[
000,[
011,[
000,[
004,001,-
]+(4)
]-
]M
]+(8)
]
[
001,[
001,001,m
]m
]*(1:6)
]
```
Get rid of the parentheses：
```
008,000,000,000,000,0000,000,mm-mM-000,000,000,mm-000,011,000,004,001,-+-M+001,001,001,mm*
```
```
$ curl -q -H 'Content-Type:application/json' -d "{\"input\": \"008,000,000,000,000,0000,000,mm-mM-000,000,000,mm-000,011,000,004,001,-+-M+001,001,001,mm*\"}" http://follow-me.chal.seccon.jp/submit/quals/0
{"error":false,"flag":"SECCON{Is it easy for you to recovery input from execution trace? Keep hacking:)}","message":"Thanks! I'll give you a flag as a thank you."}
```
