# RGNN 
    Reversing, Great. Nunnu Nanna RGNN is a binary that takes in a 50x50 character input and generates the flag out of it if it fulfills the specified constraints.
## Solution
### Looking into the Code
Interestingly the control flow of the binary is a bit weird as the `main` function only contains a check whether an addtional parameter was provided (otherwise it sets `failed = -1`).The actual logic is within the `fini_array` executed after the `main` function.
If a file was provided it starts with reading:
```Cif ( failed != -1 ) { //  if no file was provided don't check if it fulfills the constrains    fd = open(file, 0);    if ( fd >= 0 ) {        for ( i = 0; i < 0x32; i++ ) {            for ( j = 0; j = 0x32; j++ ) {                if ( read(fd, &buf, 1) != 1 || buf < 0x30 || buf > 0x33 )  // read the input                    return;                inputMap[0x32 * i + j] = buf - 0x30;            }            if ( read(fd, &buf, 1) != 1 ) // read the new line                return;        }        close(fd);    }}```
The input has a format of 50 characters that are either 0, 1, 2 or 3 and this for 50 lines (important here is a 1 byte line ending).
Next is the actual task of the challenge:
```Cif ( failed != -1 ) { // if no file was provided don't check if it fulfills the constrains
    for ( i = 0; i < 0x32; i++ )  { // y axis loop         input_j = 0;         for ( j = 0; j < 0x28; j++ ) { // x axis loop             if ( arrayXAxis[2 * (j + 0x28 * i)] == 5 )  break; // Type = 5 Blocks act as ends for the row / column             while ( input_j < 0x32 ) { // iterate until a non-zero is found in the input                if ( inputMap[0x32 * i + input_j] )                    break;                input_j++;            }             // check if the found input is not out of bounds and is equal to the required block type            if ( input_j == 0x32 || inputMap[0x32 * i + input_j] != arrayXAxis[2 * (j + 0x28 * i)] ) {                failed = 0;                return;            }             // iterate until the input type changes or we go out of bounds            old_j = input_j;            while ( input_j < 0x32 && inputMap[0x32 * i + input_j] == arrayXAxis[2 * (j + 0x28 * i)] )                input_j++;             // check if the block size is equal to the required block size             if ( input_j - old_j != arrayXAxis[2 * (j + 0x28 * i) + 1]) {                failed = 0;                return;            }         }    }}```
This is a bit more to digest. The function iterates through a `arrayXAxis` array and the input has to match the values of it.These values have to repeated exactly a specified amount from the `arrayXAxis` array and if for a single array entry this is not true the program fails.Between each loop iteration an arbitrary number of `0` can exist as long as we don't get out of the 50 character bounds.
The same is repeated for the Y-Axis with another array:
```Cif ( failed != -1 ) { // if no file was provided don't check if it fulfills the constrains
    for ( i = 0; i < 0x32; i++ )  { // x axis loop         input_j = 0;         for ( j = 0; j < 0x28; j++ ) { // y axis loop             if ( arrayYAxis[2 * (j + 0x28 * i)] == 5 )  break; // Type = 5 Blocks act as ends for the row / column             while ( input_j < 0x32 ) { // iterate until a non-zero is found in the input                if ( inputMap[0x32 * input_j + i] )                    break;                input_j++;            }             // check if the found input is not out of bounds and is equal to the required block type            if ( input_j == 0x32 || inputMap[0x32 * input_j + i] != arrayYAxis[2 * (j + 0x28 * i)] ) {                failed = 0;                return;            }             // iterate until the input type changes or we go out of bounds            old_j = input_j;            while ( input_j < 0x32 && inputMap[0x32 * input_j + i] == arrayYAxis[2 * (j + 0x28 * i)] )                input_j++;             // check if the block size is equal to the required block size             if ( input_j - old_j != arrayYAxis[2 * (j + 0x28 * i) + 1]) {                failed = 0;                return;            }         }    }}```
This can be modeled as following:
![](img/XAxis.png)
The binary provides for both X-Axis and Y-Axis an amount of `Blocks` which have a `Type` (`1`, `2`, `3`) and a Size.Each Row and Column is `50 Elements` in Size and these `Blocks` are placed in the specified order on them.It is then possible to move these `Blocks` left and right by redistributing the `0`s around.
![](img/YAxis.png)
A small addition to this is that two `Blocks` with the same `Type` may not be directly next to each other as the program would otherwise count them as one `Block` and not multiple, so there must be `0`s between them. 
![](img/XYAxis.png)
The solution to this challenge is a layout that is simultaneously viable for the `X-Axis-Array` of `Blocks` and the `Y-Axis-Array` of `Blocks`.
### Modeling the Problem
![](img/Conv.png)
As a first step to solving this I converted the `X-Axis-Array` and `Y-Axis-Array` from their array of `(Type, Size)` into their `50 x 50 Raster` representation. (See the `createRaster.py` script)
For the X-Axis this looks as following:
![](img/mapX.png)
And for the Y-Axis:
![](img/mapY.png)
The second step was to make `Blocks` out of these `Raster`s again and to define constrains for moving them around.
```pythonglobalBlockNr = 0def blockify(line):    global globalBlockNr    blocks = [] # (blockType, blockSize, blockPostionVar)    lastBlock = None    for c in line:        if lastBlock != None and (ord(c)-ord('0')) == lastBlock[0]:            bT, bS, bV = lastBlock            lastBlock = (bT, bS+1, bV)        else:            if lastBlock != None:                blocks.append(lastBlock)                lastBlock = None            if c != '0':                lastBlock = ((ord(c)-ord('0')), 1, BitVec('block_'+str(globalBlockNr), 8))                globalBlockNr += 1    if lastBlock != None: blocks.append(lastBlock)    return blocks```    
Reversing the above process again and adding the additional position variable is rather easy and could have been probably combined with the `Raster` creation part.
The movement constraints of the `Blocks` can be expressed as following:
```pythondef blockifyConstrains(line):    blocks = blockify(line)    for i in range(len(blocks)):        solver.add(ULE(blocks[i][3],0x32-blocks[i][1])) # A Block may only have a position from 0 to 49 and they may not go out of bounds
    for i in range(len(blocks)):        if i+1 < len(blocks) and blocks[i][0] == blocks[i+1][0]: solver.add(ULT(blocks[i][2]+blocks[i][1], blocks[i+1][2])) # Increasing the boundry box if two same Type Blocks are following each other        elif i+1 < len(blocks): solver.add(ULE(blocks[i][2]+blocks[i][1], blocks[i+1][2])) # No Block may intersect or be more right than their successor Block         if i-1 > 0 and blocks[i][0] == blocks[i-1][0]: solver.add(ULT(blocks[i-1][2]+blocks[i-1][1], blocks[i][2])) # Increasing the boundry box if two same Type Blocks are following each other        elif i-1 > 0: solver.add(ULE(blocks[i-1][2]+blocks[i-1][1], blocks[i][2])) # No Block may intersect or be more left than their predecessor Block     return blocks```
- Each `Block` with their full length must be within the 50 Length Row / Column- As the sequential order of `Blocks` may not be changed, no `Block's` position may be lower than their predecessor or higher then their successor- `Blocks` may not intersect with each other- If two `Same-Type Blocks` are next to each other enforce a gap between them
Now to combine the `X-Axis` and `Y-Axis` contrains on these `Blocks` I project them back again on the `50 x 50 Raster`
```pythondef addLine(line, row):    blocks = blockifyConstrains(line)     for p in range(0x32): # for each pixel in this row        l = []        last = (pixel[row][p] == 0) # if this pixel is in no block then it's value is 0        for i in range(len(blocks)): # check if the pixel is in a block and if not check the next block            last = If(And(ULE(blocks[i][2], p), ULT(p, blocks[i][2]+blocks[i][1])), pixel[row][p] == blocks[i][0], last)        solver.append(last) # add the merged constraint to the solver```
I do this by checking for each pixel in a Row / Column if it's within one of the `Blocks` and if so then adding the `Type` of the `Block` as a constrain for the pixel (or `0` if the pixel is in no `Block`)
The same is of course also done for the `Y-Axis`:
```pythondef addColumn(line, col):     blocks = blockifyConstrains(line)     for p in range(0x32): # for each pixel in this column        l = []        last = (pixel[p][col] == 0) # if this pixel is in no block then it's value is 0        for i in range(len(blocks)): # check if the pixel is in a block and if not check the next block            last = If(And(ULE(blocks[i][2], p), ULT(p, blocks[i][2]+blocks[i][1])), pixel[p][col] == blocks[i][0], last)        s.append(last) # add the merged constraint to the solver```    
(See `solve.py` for the full solution)
### Flag
After a short while of letting `Z3` solve the model we get a solution:
![](img/mapSolution.png)
```1111311112222011210113001333120011113333322110111111132112111223120210333311121301031133301331111120010131102111111231120312223211000331210300333111011121111222123233102303013230113023121112200312013211220220320222031001103311031111112001111210031330302332130110112331011023323111100330011213112311112303023231322202210311213111101302000102202222213112112201110220311121111011122200022121101301223222122033230223003203321220131203222331011213220132222023311120331212031133011012130013320332132221111033020111213333021122132222111013301303003202200113121333133322110202332331133323022111100322221301021323300333323010020003111112233331311233022313111211122233033022321033021111333333022101101120130110201133303011013311323012210030113111320013202333001102312221111202122222022323310312223211120200330130223111212033111013320221200223111230313312233301233331021021012212100332012122213312133123231020230222211312222312111011112111102133110002102312230112130103230112210111111110331122220331120211133312223321333311321001122111111031121112101222111130322212123330211121111122001200131212112233211111003203101331230001123111231213223222301133301122130000331100101113231330322220130022013003311103212302221111121110222311322201311003323101301132331110333212013320200002222222111221103020122233323311132302020221321302233103330301120330223112221133333333332221313322322311033001122033120220322223033123033223313032101011122122220222113123212121333030003310200033332222311221032020112101333212223323300002332212103322123122111222110121123331032220333222202231021101011231111022012301101200112332102312220223112211330112222123231113232321111012133302130212211133301221031010111331111112012113321322110122121111331032213031112211133101000000132333111001212221313301100113233213122012331222331332003012113112230111201032222232133312311222203130211033322011213303202030302202311112110212222221332030333202122302132132003330013111120133322312121320021131132113331111131222112031312231303323113222220001123102321111112311211000002111130303331332023321111112030301111113323302112313123222311210132023011301011313311111232033223333303020103310320330000111130123300111101103302013311122111231111130330131020011233311221111012332020311312033001131112333303222033033333212112203111233113322333333300221021331003333200312112033333110131023223303213132021113013303320322123203021101100211320211131121012312112232012112332021022222311202330131012330213231111022221211132332011333303310033031221123122112033110113113022003```
Using this as the input for the binary provides the flag (again watch out to use 1-Byte Line Breaks):
    $ ./binary input.txt    pbctf{ebbebebtebeertbebbrbbrebbetbttetebrtbbbeeettbbtbbbbteetbrrrbbttb}