## Challenge: verifier
Challenge is an interactive shell accessible via TCP/IP using `netcat`.`SyntaxError` after any random input gives as a clue that shell expects someparticular input, maybe commands. Obvious `?`, `help` and `h` have no effect(same `SyntaxError`).
Fortunately, [source code](https://github.com/im-0/ctf/blob/master/2020.02.08-CODEGATE_2020_Quals/verifier/challenge/) in Python is also given to us.
### Source code
Quick look at the source code shows us that service implements an interpreterfor a simple expression language. It uses[PLY (Python Lex-Yacc)](http://www.dabeaz.com/ply/) as a lexer/parser library.
[lexer.py](https://github.com/im-0/ctf/blob/master/2020.02.08-CODEGATE_2020_Quals/verifier/challenge/lexer.py) and [parser.py](https://github.com/im-0/ctf/blob/master/2020.02.08-CODEGATE_2020_Quals/verifier/challenge/parser.py) revealsthat implemented language supports following:
 * variable names (and assignment using `=`); * integer literals (bots positive and negative); * usual binary operations: `+`, `-`, `*`; * comparisons: `==`, `<`, `<=`, etc.; * "if/else":`<condition (comparison)> ? {  } : {  }`; * "while" loop: `[<condition (comparison)> {  }]`; * "print" command: `!<expression>`; * "get random number from interval" expression: `<from int> ~ <to int>`; * semicolon for command sequences.
Maybe I missed some other constructions.
Anyway, this is enough to write simple programs:
```> a=123;!a123
> i=10;[i>0{i=i-(1);x=1~4;!x}]2314411231```
But where is the flag?
```$ git grep -i flagast.py:            with open('./flag') as f:```
```pythonclass Print(Comm):    def __init__(self, expr):        self.expr = expr
    def a_interp(self, env):        a_val = self.expr.a_interp(env)        if a_val.infimum < 0:            raise ValueError("print domain error")        return env
    def interp(self, env):        value = self.expr.interp(env)
        if value < 0:            with open('./flag') as f:                print(f.read())        print(value)        return env```
Ok, it seems that we just need to print negative integer. Easy!
```> x=-1;!xError: print domain error```
Nope! Interpreter has two "modes" of execution for each expression: normal`interp()`, which uses known integer values in obvious way, and `a_interp()`(abstract interpret?), which uses intervals for everything. For example,integer literal `42` maps to interval `[42, 42]`, random number `1 ~ 10` mapsto interval `[1, 10]`, expression `(1 ~ 10) + (4)` results in interval`[5, 14]`.
For any input, challenge service first calls `a_interp()` and onlythen `interp()`. So we need to somehow trick `a_interp()` flow to result inpositive interval (so it will not throw an exception) and `interp()` flow toresult in negative value in the same time.
### Solution
After reading [domain.py](https://github.com/im-0/ctf/blob/master/2020.02.08-CODEGATE_2020_Quals/verifier/challenge/domain.py), I thought that maybe I couldget NaNs using infinity values, and this will lead me somewhere. But no, this isnot possible because of the following line in constructor:
```pythonassert infimum <= supremum```
`NaN` on either side of the expressions leads to `False`, and thus toexception.
Then I started to read [ast.py](https://github.com/im-0/ctf/blob/master/2020.02.08-CODEGATE_2020_Quals/verifier/challenge/ast.py) (the actual interpreter)carefully to find possible bugs. And eventually found following implementationof "while" loop:
```pythonclass While(Comm):    ...
    def a_interp(self, env):        init_env = deepcopy(env)
        for i in range(3):            tenv, _ = self.cond.a_interp(env)            if tenv is not None:                tenv = self.comm.a_interp(tenv)            env = env_join(env, tenv)
        tenv, _ = self.cond.a_interp(env)        if tenv is not None:            tenv = self.comm.a_interp(tenv)        env = env_widen(env, tenv)
        tenv, _ = self.cond.a_interp(env)        if tenv is not None:            tenv = self.comm.a_interp(tenv)        env = env_join(init_env, tenv)        _, fenv = self.cond.a_interp(env)
        if fenv is None:            raise RuntimeError("loop analysis error")
        return fenv
    ...```
`for i in range(3):` looks very suspicious here. Like it uses only fewiterations of loop to calculate intervals for resulting variables.
After some experimenting, I found the right combination of "while" loop andif/else:
```x = 0;i = 20;[i > 0 {    i = i - (1);    i > 15? {        x = x + (1)    } : {        x = x - (1)    }}];x = x + (1);!x```
This code results in value `-11` but positive interval `[0, inf]` for variable`x`.
Sending it (without the whitespace characters) to the challenge server gaveme the flag:
```$ nc 58.229.253.56 7777> x=0;i=20;[i>0{i=i-(1);i>15?{x=x+(1)}:{x=x-(1)}}];x=x+(1);!xCODEGATE2020{4bstr4ct_1nt3rpr3tat10n_f0r_54f3_3v41uat10n}```
Source code containing my local experiments is [here](https://github.com/im-0/ctf/blob/master/2020.02.08-CODEGATE_2020_Quals/verifier/solution.py).