# PlaidCTF 2020 : reee
### Reversing (150 pts) > __Story__>> Tired from all of the craziness in the Inner Sanctum, you decide to venture out to the beach to relax. You doze off in the sand only to be awoken by the loud “reee” of an osprey. A shell falls out of its talons and lands right where your head was a moment ago. No rest for the weary, huh? It looks a little funny, so you pick it up and realize that it’s backwards. I guess you’ll have to reverse it.> > __Problem details__>> Hint: The flag format is `pctf{$FLAG}`. This constraint should resolve any ambiguities in solutions.
## Act 1 — Reverse engineeringWe are given a x64 stripped ELF:```reee: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 2.6.32, BuildID[sha1]=3ccec76609cd013bea7ee34dffc8441bfa1d7181, stripped```
Opening it with IDA we can see that its code is quite simple.```Cunsigned char[551] = { /* a few numbers here */ };int main(int argc, char** argv, char** envp){    int result; // eax    int j; // [rsp+18h] [rbp-28h]    int i; // [rsp+1Ch] [rbp-24h]
    if(argc <= 1)        puts("need a flag!");    for(i = 0; i <= 31336; ++i)    {      for(j = 0; j <= 551; ++j)          code[j] = decrypt(code[j]);    }    if(((long long (*)(void))code)())        result = puts("Correct!");    else        result = puts("Wrong!");    return result;}
unsigned char bss1, bss2;unsigned char data1[256] = { /* some more data */ }; // Size guessed by IDAunsigned char decrypt(unsigned char c){    bss2 += data1[++bss1];    data1[bss1] ^= data1[bss2];    data1[bss2] ^= data1[bss1];    data1[bss1] ^= data1[bss2];    return data1[(unsigned char)(data1[bss1] + data1[bss2])] + c;}```It looks like it _decrypts_ some data from `0x400526` and then executes it. I honestly couldn't care less about how this _decipher_ works, I need flaaaaggggssss!
This code returns a value which, in case it is `0`, `main()` will print a `"Wrong!"` string, otherwise a `"Correct!"` string.
Let's see... the call is made in```.text:00000000004006DB                 call    near ptr code```so```gef➤  b*0x4006dbBreakpoint 1 at 0x4006db```and then```gef➤  r flagplzzzzzzzzzzStarting program: /home/arget/reee flagplzzzzzzzzzz
Breakpoint 1, 0x00000000004006db in ?? ()gef➤  si0x00000000004006e5 in ?? ()gef➤  x/11i $pc=> 0x4006e5:    push   rbp   0x4006e6:    mov    rbp,rsp   0x4006e9:    call   0x400702   0x4006ee:    mov    cl,al   0x4006f0:    mov    eax,0xae5fe432   0x4006f5:    add    eax,0x51a01bce   0x4006fa:    inc    eax   0x4006fc:    jae    0x400706               # Ignore   0x4006fe:    mov    al,cl   0x400700:    leave     0x400701:    ret    ```So here we have a C function, which basically calls another function, makes a nonsense operation, and returns the result of the function previously called. Nonsense operations like that are going to be something usual along all this code, none of those jumps is ever taken because of the flags left by the mentioned nonsense operations, they are there just to tease. [I usually prefer the static analysis, but in this case it is going to be so much easier and quicker the dynamic analysis].
Now let's step into that function```gef➤  x/10i $pc=> 0x400702:    push   rbx   0x400703:    push   rdi   0x400704:    push   rbp   0x400705:    mov    rbp,rsp   0x400708:    mov    rdx,rax   0x40070b:    dec    eax   0x40070d:    jmp    0x40070e   0x40070f:    ror    BYTE PTR [rax-0x75],0xfa   0x400713:    xor    al,al   0x400715:    xor    ecx,ecxgef➤  ```We can see another standard prologue, copies the content of `rax`  to `rdx`, decrements `rax` and jumps somewhere, and the last three instructions doesn't look like they are going to be executed ever... um btw,`rax` contains `argv[1]`. And, just so you know, from now on I'm going to snip the instructions after a `jmp`.```gef➤  x/s $rax0x7fffffffe4b6: "flagplzzzzzzzzzz"gef➤  si 70x000000000040070e in ?? ()gef➤  x/10i $rip=> 0x40070e:    inc    eax   0x400710:    mov    rdi,rdx   0x400713:    xor    al,al   0x400715:    xor    ecx,ecx   0x400717:    dec    rcx   0x40071a:    repnz scas al,BYTE PTR es:[rdi]   0x40071c:    not    ecx   0x40071e:    dec    ecx   0x400720:    mov    eax,0x92185987   0x400725:    xor    eax,0x32963a85gef➤     0x40072a:    jns    0x4006b7               # Ignore   0x40072c:    mov    eax,0xc3bc42d9   0x400731:    xor    eax,0x1ed2c907   0x400736:    jns    0x400742               # Ignore   0x400738:    push   0x50   0x40073a:    pop    r9   0x40073c:    xor    r8d,r8d   0x40073f:    cmp    r8d,0x539   0x400746:    jl     0x400763   0x400748:    jmp    0x400774```Ok, here happens something. First, the `dec eax` performed earlier is undone (this is also very usual in this challenge, `dec; jmp; inc`). The next seven instructions correspond to an optimized call to `strlen(argv[1])` —if you need further explaination [here you go](https://stackoverflow.com/questions/26783797/repnz-scas-assembly-instruction-specifics)—, the result is hold in `ecx`. Then we have another nonsense set of instructions (the `jns` is never going to happen because that `xor` sets `SF=1`), after this the program moves with `push;pop` the value `0x50` to the register `r9` and set to zero the lower dword of `r8`. Afterwards we have an `if`, or, more likely (because of the previous `xor`),  a `for(r8d = 0; r8d < 1337; ++r8d)`. The `jl` would jump to the body of the alleged `for`.
    gef➤  si 16+19    0x0000000000400763 in ?? ()    gef➤  x/10i $pc    => 0x400763:    mov    eax,0xe72b5c52       0x400768:    add    eax,0x18d4a3ae       0x40076d:    jne    0x400747               # Ignore       0x40076f:    xor    r11d,r11d       0x400772:    jmp    0x4007acJust ignore the `mov;add;jne`.  Now it makes zero the lower dword of the `r11` register. Another `for` is incoming? This xor must mean that `r11` is another counter...
    gef➤  si 5    0x00000000004007ac in ?? ()    gef➤  x/10i $pc    => 0x4007ac:    dec    eax       0x4007ae:    jmp    0x4007af    gef➤  si 2    0x00000000004007af in ?? ()    gef➤  x/10i $pc    => 0x4007af:    inc    eax       0x4007b1:    cmp    r11d,ecx       0x4007b4:    jl     0x4007b8       0x4007b6:    jmp    0x40074aThere! We have another (presumably) `for` loop, we only have to find the two `jmp`'s that jump backwards to make both suspected loops. In this case we would have a `for(r11d = 0; r11d < arglen; ++r11d)` (remember we have in `ecx` the length of our argument).
    gef➤  si 3    0x00000000004007b8 in ?? ()    gef➤  x/10i $pc    => 0x4007b8:    mov    eax,0x2b71234a       0x4007bd:    add    eax,0xd48edcb6       0x4007c2:    inc    eax       0x4007c4:    jae    0x400774       0x4007c6:    movsxd r10,r11d       0x4007c9:    mov    eax,0xef8ac85b       0x4007ce:    xor    eax,0xe71ae312       0x4007d3:    js     0x4007ff       0x4007d5:    mov    rbx,rdx       0x4007d8:    add    rbx,r10    gef➤         0x4007db:    mov    eax,0x46d3a79d       0x4007e0:    add    eax,0xb92c5863       0x4007e5:    jne    0x4007ee       0x4007e7:    movsxd r10,r11d       0x4007ea:    mov    eax,0xf45102a7       0x4007ef:    xor    eax,0xae9accbc       0x4007f4:    js     0x40085f       0x4007f6:    mov    rax,rdx       0x4007f9:    add    rax,r10       0x4007fc:    mov    al,BYTE PTR [rax]    gef➤         0x4007fe:    xor    al,r9b       0x400801:    mov    BYTE PTR [rbx],al       0x400803:    movsxd r10,r11d       0x400806:    mov    rax,rdx       0x400809:    add    rax,r10       0x40080c:    mov    al,BYTE PTR [rax]       0x40080e:    xor    r9b,al       0x400811:    mov    eax,0x91ecf78       0x400816:    add    eax,0xf6e13088       0x40081b:    inc    eax    gef➤         0x40081d:    jae    0x4007be       0x40081f:    add    r11d,0x1       0x400823:    mov    eax,0x15690edd       0x400828:    xor    eax,0xd68c1903       0x40082d:    jns    0x400888       0x40082f:    jmp    0x4007acI will now comment the code ignoring the (not so) teasing instructions. The final `jmp` jumps to the `dec eax` we have seen in the previous to the last snippet of asm, completing that way the loop we were looking for.```   0x4007c6:    movsxd r10,r11d   0x4007d5:    mov    rbx,rdx   0x4007d8:    add    rbx,r10````rbx = &argv[1][r11d]`, where `r11d` is our counter (did you remember that `rdx` had `argv[1]`?).```   0x4007e7:    movsxd r10,r11d   0x4007f6:    mov    rax,rdx   0x4007f9:    add    rax,r10   0x4007fc:    mov    al,BYTE PTR [rax]```Almost same procedure, but this time the pointer gets dereferenced, performing `al = argv[1][r11d]`.```   0x4007fe:    xor    al,r9b   0x400801:    mov    BYTE PTR [rbx],al```Thereupon, xor that value with `r9` (which cointained `0x50`) and save it back to `&argv[1][r11d]````   0x400803:    movsxd r10,r11d   0x400806:    mov    rax,rdx   0x400809:    add    rax,r10   0x40080c:    mov    al,BYTE PTR [rax]   0x40080e:    xor    r9b,al````r9b ^= argv[1][r11d]`,  now `r9` has the original value (before the xor) of `argv[1][r11d]`.```   0x40081f:    add    r11d,0x1   0x40082f:    jmp    0x4007ac```Increment the counter and loop back.
Now, how is the path followed when the program finishes this loop? We are here again, but now we will follow the other way.```gef➤  x/2i 0x4007ac   0x4007ac:    dec    eax   0x4007ae:    jmp    0x4007afgef➤  x/4i 0x4007af   0x4007af:    inc    eax   0x4007b1:    cmp    r11d,ecx   0x4007b4:    jl     0x4007b8   0x4007b6:    jmp    0x40074a```If the counter has reached the length of our string the `jl` doesn't jump and the `jmp 0x40074a` is taken instead.```gef➤  tb *0x4007b6Temporary breakpoint 3 at 0x4007b6gef➤  cContinuing.
Temporary breakpoint 3, 0x00000000004007b6 in ?? ()gef➤  i r ecx r11decx            0x10                0x10r11d           0x10                0x10gef➤  x/i $pc=> 0x4007b6:    jmp    0x40074agef➤  si0x000000000040074a in ?? ()gef➤  x/10i $pc=> 0x40074a:    dec    eax   0x40074c:    jmp    0x40074dgef➤  si 20x000000000040074d in ?? ()gef➤  x/10i $pc=> 0x40074d:    inc    eax   0x40074f:    add    r8d,0x1   0x400753:    mov    eax,0x669ec28e   0x400758:    add    eax,0x99613d72   0x40075d:    inc    eax   0x40075f:    jae    0x400724               # Ignore   0x400761:    jmp    0x40073f````r8d` incremented and umm `0x40073f`, that address, we have seen it before. Yes, we have now the backward jump for the outer `for`. Now we have checked that this is a `for` too, and `r8d` is its counter.```gef➤  si 70x000000000040073f in ?? ()gef➤  x/10i $pc=> 0x40073f:    cmp    r8d,0x539   0x400746:    jl     0x400763   0x400748:    jmp    0x400774
```The counter `r8d` is incremented and compared against `1337`, when this value is reached the execution will flow to `0x400774`, outside —finally— of these almost endless loops. The C code for this loop would be something like this```Cr9d = 0x50;for(r8d = 0; r8d < 1337; ++r8d){    for(r11d = 0; r11d < arglen; ++r11d)    {        argv[1][r11d] ^= r9d;        r9d ^= argv[1][r11d];    }}```Now with the things a lot clearer we can proceed with the rest of the code.```gef➤  tb*0x400748Temporary breakpoint 4 at 0x400748gef➤  cContinuing.
Temporary breakpoint 4, 0x0000000000400748 in ?? ()gef➤  i r r8r8             0x539               0x539gef➤  si0x0000000000400774 in ?? ()gef➤  x/10i $pc=> 0x400774:    mov    eax,0xea3e6566   0x400779:    xor    eax,0x5f69faeb   0x40077e:    jns    0x4007b6               # Ignore   0x400780:    lea    rax,[rip+0x164]        # 0x4008eb   0x400787:    lea    r8,[rax]   0x40078a:    mov    eax,0xb5de3358   0x40078f:    xor    eax,0x459f236e   0x400794:    jns    0x400797               # Ignore   0x400796:    dec    eax   0x400798:    jmp    0x400799```The program gets in `r8` the address of some data in `.data` (addr `0x4008eb`)```gef➤  si 100x0000000000400799 in ?? ()gef➤  x/10i $pc=> 0x400799:    inc    eax   0x40079b:    push   0x1   0x40079d:    pop    r10   0x40079f:    dec    eax   0x4007a1:    jmp    0x4007a2```Set `r10 = 1````gef➤  si 50x00000000004007a2 in ?? ()gef➤  x/10i $pc=> 0x4007a2:    inc    eax   0x4007a4:    xor    r9d,r9d   0x4007a7:    jmp    0x400834```I can see another loop, using `r9d` as counter, coming.
    => 0x400834:    mov    eax,0x4759bfd0       0x400839:    add    eax,0xb8a64030       0x40083e:    inc    eax       0x400840:    jae    0x400847               # Ignore       0x400842:    cmp    r9d,ecx       0x400845:    jl     0x400849       0x400847:    jmp    0x400850We can see an `if(r9d < arglen)`, which will in all likelihood be, from a loop `for(r9d = 0; r9d < arglen; ++r9d)`. ```gef➤  si 60x0000000000400849 in ?? ()gef➤  x/10i $pc=> 0x400849:    test   r10b,r10b   0x40084c:    jne    0x400857   0x40084e:    jmp    0x40089f```An `if(r10b)`? Well, we are going straight into it because `r10b == 1 != 0````gef➤  si 20x000000000040085a in ?? ()gef➤  x/10i 0x400857=> 0x400857:    movsxd r11,r9d   0x40085a:    mov    eax,0x5f9c75ce   0x40085f:    xor    eax,0x5d98bd96   0x400864:    js     0x4008a0               # Ignore   0x400866:    mov    r10,rdx   0x400869:    add    r10,r11   0x40086c:    dec    eax   0x40086e:    jmp    0x40086fef➤  si 80x000000000040086f in ?? ()gef➤  x/10i $pc=> 0x40086f:    inc    eax   0x400871:    mov    r11b,BYTE PTR [r10]   0x400874:    mov    eax,0xf8eca7d8   0x400879:    add    eax,0x7135828   0x40087e:    jne    0x40081c               # Ignore   0x400880:    movsxd rax,r9d   0x400883:    mov    r10,r8   0x400886:    add    r10,rax   0x400889:    mov    eax,0x3b4ad836   0x40088e:    xor    eax,0xf1d7dbeagef➤     0x400893:    jns    0x400818               # Ignore   0x400895:    mov    al,BYTE PTR [r10]   0x400898:    cmp    r11b,al   0x40089b:    je     0x4008c3   0x40089d:    jmp    0x4008da```Ok, I will remove the incoherences and conditional jumps to see it clearer```   0x400857:    movsxd r11,r9d   0x400866:    mov    r10,rdx   0x400869:    add    r10,r11   0x400871:    mov    r11b,BYTE PTR [r10]   0x400880:    movsxd rax,r9d   0x400883:    mov    r10,r8   0x400886:    add    r10,rax   0x400895:    mov    al,BYTE PTR [r10]   0x400898:    cmp    r11b,al   0x40089b:    je     0x4008c3   0x40089d:    jmp    0x4008da```We can see it obtains `argv[1][r9d]`, and then `*(r8 + r9d)` (`r8` contains the address of some place in `.data`, the program `LEA`'d that address earlier, as you can see scrolling up), and compares them. If they are equal jumps to `0x4008c3`, if not, to `0x4008da`.```gef➤  x/10 0x4008c3   0x4008c3:    mov    eax,0x451c2342   0x4008c8:    add    eax,0xbae3dcbe   0x4008cd:    jne    0x400901               # Ignore   0x4008cf:    push   0x1   0x4008d1:    pop    r10   0x4008d3:    dec    eax   0x4008d5:    jmp    0x4008d6gef➤  x/10 0x4008d6   0x4008d6:    inc    eax   0x4008d8:    jmp    0x4008ddgef➤  x/10 0x4008dd   0x4008dd:    mov    eax,0x5e82d693   0x4008e2:    add    eax,0xa17d296d   0x4008e7:    jne    0x40090a               # Ignore   0x4008e9:    jmp    0x4008a2gef➤  x/10 0x4008a2   0x4008a2:    mov    eax,0x2e4ef210   0x4008a7:    add    eax,0xd1b10df0   0x4008ac:    jne    0x40087e               # Ignore   0x4008ae:    mov    eax,0x1bff10d0   0x4008b3:    xor    eax,0x9dd00315   0x4008b8:    jns    0x40091d               # Ignore   0x4008ba:    add    r9d,0x1   0x4008be:    jmp    0x400834```This is executed in case both values `argv[1][r9d]` and `*(r8 + r9d)` are the same. Let me clean it up for you [so much rubbish...].```   0x4008cf:    push   0x1   0x4008d1:    pop    r10   0x4008ba:    add    r9d,0x1   0x4008be:    jmp    0x400834```And this is just `r10 = 1; r9d++;`, and that `jmp` goes back to the condition checking of what I predicted a `for`.
Now the other path:```gef➤  x/10i 0x4008da   0x4008da:    xor    r10b,r10b   0x4008dd:    mov    eax,0x5e82d693   0x4008e2:    add    eax,0xa17d296d   0x4008e7:    jne    0x40090a               # Ignore   0x4008e9:    jmp    0x4008a2gef➤  x/10i 0x4008a2   0x4008a2:    mov    eax,0x2e4ef210   0x4008a7:    add    eax,0xd1b10df0   0x4008ac:    jne    0x40087e               # Ignore   0x4008ae:    mov    eax,0x1bff10d0   0x4008b3:    xor    eax,0x9dd00315   0x4008b8:    jns    0x40091d               # Ignore   0x4008ba:    add    r9d,0x1   0x4008be:    jmp    0x400834```Which translates into```gef➤  x/10i 0x4008da   0x4008da:    xor    r10b,r10b   0x4008ba:    add    r9d,0x1   0x4008be:    jmp    0x400834```This is executed in case they are not the same value. Let me point out that both paths get to `0x4008ba`, only changes that the bad path (with the `if` false) makes `0` the `r10b` register, while the other makes it `1`. 
So for this `for` —haha— we have this impression right now.```Cr8 = 0x4008eb;r10b = 1;for(r9d = 0; r9d < arglen; ++r9d){    if(r10b)    {        if(argv[1][r9d] == *(r8 + r9d))            r10b = 1;        else            r10b = 0;    }    else    {        /* Something, maybe nothing, who knows? Fate knows. */    }}```Nothing too weird. Now we have to explore the `else` path. But, first. a throwback.```gef➤  x/2i $pc=> 0x40086f:    inc    eax   0x400871:    mov    r11b,BYTE PTR [r10]```We are still here, in the first few steps inside the `if(r10b)`, all the previous analysis since almost `if(r10b)` was indeed static. Now, taking into account that we haven't used as argument the flag, the modified `argv[1]` won't match the data pointed by r8, and therefore we will execute the `xor r10b, r10b` at some iteration (almost certainly sure the first one) and the next iteration `if(r10b)` will be false and the program flow will go through the `else`, so I am setting a breakpoint there```gef➤  tb*0x40084eTemporary breakpoint 6 at 0x40084egef➤  cContinuing.
Temporary breakpoint 6, 0x000000000040084e in ?? ()gef➤  si0x000000000040089f in ?? ()gef➤  x/10i $pc=> 0x40089f:    xor    r10b,r10b   0x4008a2:    mov    eax,0x2e4ef210   0x4008a7:    add    eax,0xd1b10df0   0x4008ac:    jne    0x40087e               # Ignore   0x4008ae:    mov    eax,0x1bff10d0   0x4008b3:    xor    eax,0x9dd00315   0x4008b8:    jns    0x40091d               # Ignore   0x4008ba:    add    r9d,0x1   0x4008be:    jmp    0x400834```Which pretty much does nothing xd. Sets to `0` the `r10b` (although if we are here is, in theory, because `r10b` is already `0`), increments the counter and goes back to the top of the `for`. We could preferably write the `for` this way```Cr8 = 0x4008eb;r10b = 1;for(r9d = 0; r9d < arglen; ++r9d){    if(!r10b) continue;    if(argv[1][r9d] == *(r8 + r9d))        r10b = 1;    else        r10b = 0;}```Let's finish this loop.```   0x400847:    jmp    0x400850gef➤  tb *0x400847Temporary breakpoint 7 at 0x400847gef➤  cContinuing.
Temporary breakpoint 7, 0x0000000000400847 in ?? ()gef➤  si0x0000000000400850 in ?? ()gef➤  x/10i $pc=> 0x400850:    mov    al,r10b   0x400853:    leave     0x400854:    pop    rdi   0x400855:    pop    rbx   0x400856:    ret```Ahhh we can see the light at the end of the tunnel. This is just a `return r10b;`, which turns out to be `1` if the modified `argv[1]` is equal to the bytestring in the binary, or `0` otherwise.```gef➤  si 50x00000000004006ee in ?? ()gef➤  x/10 $pc=> 0x4006ee:    mov    cl,al   0x4006f0:    mov    eax,0xae5fe432   0x4006f5:    add    eax,0x51a01bce   0x4006fa:    inc    eax   0x4006fc:    jae    0x400706               # Ignore   0x4006fe:    mov    al,cl   0x400700:    leave     0x400701:    ret```And back to the first function of the _decrypted_ code. A `return cl;` where `cl` holds the value returned from the other function. After the `ret`, `main()` prints one string or another depending on the value that this function returned.
## Act 2 — Z3 The Theorem ProverNow that we know how the program behaves, we need to know the result that our string must have after all the alterations that the program makes on it in order to get a desired `"Correct!"`. The aforementioned result is stored in `0x4008eb` in the data segment.```gef➤  x/40bx 0x4008eb0x4008eb:   0x48    0x5f    0x36    0x35    0x35    0x25    0x14    0x2c0x4008f3:   0x1d    0x01    0x03    0x2d    0x0c    0x6f    0x35    0x610x4008fb:   0x7e    0x34    0x0a    0x44    0x24    0x2c    0x4a    0x460x400903:   0x19    0x59    0x5b    0x0e    0x78    0x74    0x29    0x130x40090b:   0x2c    0x00    0x48    0x89    0xc2    0x48    0x89    0x55```The problem is that we don't know how long our chain should be. Here we see a `0x00`, but it could be just a coincidence `¯\_(ツ)_/¯`. Well, what do we have after this data? If there is other data stored after this maybe we could make a guess.```.text:0000000000400907                 db 0E5h.text:0000000000400908                 db 8Dh.text:0000000000400909                 db 0DDh.text:000000000040090A                 db  57h ; W.text:000000000040090B                 db 0D1h.text:000000000040090C                 db 0F2h.text:000000000040090D ; ---------------------------------------------------------------------------.text:000000000040090D.text:000000000040090D loc_40090D:                             ; CODE XREF: main+92↑j.text:000000000040090D                 mov     rdx, rax.text:0000000000400910                 mov     [rbp-18h], rdx.text:0000000000400914                 cmp     qword ptr [rbp-18h], 0.text:0000000000400919                 jz      short loc_400927.text:000000000040091B                 mov     edi, offset aCorrect ; "Correct!".text:0000000000400920                 call    _puts.text:0000000000400925                 jmp     short loc_400931```Ok, so we have, not so much farder, a chunk of `main()` (ironically the one we want to reach). Therefore we can say that the length of the bytestring can't be greater than `0x40090d − 0x4008eb = 0x22 = 34`. Besides```gef➤  x/34bx 0x4008eb0x4008eb:   0x48    0x5f    0x36    0x35    0x35    0x25    0x14    0x2c0x4008f3:   0x1d    0x01    0x03    0x2d    0x0c    0x6f    0x35    0x610x4008fb:   0x7e    0x34    0x0a    0x44    0x24    0x2c    0x4a    0x460x400903:   0x19    0x59    0x5b    0x0e    0x78    0x74    0x29    0x130x40090b:   0x2c    0x00```it has the nullbyte right at the end!! The length of the bytestring must be, with all certainty, `34 - 1 = 33`.
Now we just need someone who can solve problems this hard. Someone who... who... umm I don't know, I just broke the epic moment... It's Z3, just Z3, *The Theorem Prover*.```pythonfrom z3 import *
# How the result must be after all the modificationsflag = [0x48, 0x5f, 0x36, 0x35, 0x35, 0x25, 0x14, 0x2c, \        0x1d, 0x01, 0x03, 0x2d, 0x0c, 0x6f, 0x35, 0x61, \        0x7e, 0x34, 0x0a, 0x44, 0x24, 0x2c, 0x4a, 0x46, \        0x19, 0x59, 0x5b, 0x0e, 0x78, 0x74, 0x29, 0x13, 0x2c]
# This array holds all the variables that z3 must deal withasd = []for c in "pctf{": # Making use of the hint to set constraints    asd.append(BitVecVal(ord(c), 8))for i in range(len(flag) - 6):    asd.append(BitVec("%d" % i, 8))asd.append(BitVecVal(ord('}'), 8))
# Perform the same operations as the binaryr9 = 0x50for i in range(1337):    for j in range(len(asd)):        asd[j] ^= r9        r9 ^= asd[j]
# Impose conditionszolv = Solver()for i in range(len(asd)):    zolv.add(asd[i] == flag[i])
# Get the solutionassert zolv.check() == sat, "Can't find a solution"m = zolv.model()# Figure out how to print the model in order was the hardest partl = [(d, m[d]) for d in m]l.sort(key=lambda x:int(str(x[0])))print("pctf{", end="")for i in range(len(flag) - 6):    print(chr(int(str(l[i][1]))), end="")print("}")``````$ time python reee.py pctf{ok_nothing_too_fancy_there!}
real    1m32,830suser    1m31,872ssys     0m0,475s
$ ./reee pctf{ok_nothing_too_fancy_there!}Correct!```If the exclamation sign gives you problems in bash, just turn off the history substitution: `set +H`
