Write-up Parking (Google CTF 2021)

User1 Thu, Jul 22, 2021 7:37 PM

"It's dangerous to go alone! Take this @ch4nnel1.

Original write-up: https://hackmd.io/@osogi/parking_writeup

Russian version: https://hackmd.io/@osogi/parking_writeup_ru

Story + analysis

This task(https://capturetheflag.withgoogle.com/challenges/hw-parking or https://github.com/google/google-ctf/tree/master/2021/quals/hw-parking)

Prologue

Download the zip archive, open it, it contains 4 files

We will forget about run.sh almost immediately, because all it does is launch the game along with the first level and tell it that now it is not necessary to give the flag + just starts the second level. (I hope Google will not ban me for using the code from their task. There was just some kind of license and all that, but I was lazy to read it).

echo "Welcome to our game. You need to enter the red vehicle into a crowded parking lot."
echo "There are two levels: the first is introductory, just so you know the rules; the second, when solved, will reveal the flag. Good luck!"
FLAG=0 python3 game.py level1
echo "Good job! Now that you know the rules, let's move to the real level. Note that it is quite large, so allow some loading time."
python3 game.py level2

Well, of course, let's run the program, to start with the first level, we will see something like this

From the text that the game broadcasts to us, we understand that we need to move the red car + that the final position of the green car (as it turns out later cars) encodes the flag. After spending five minutes, with difficulty I solved the first level (I will not give tips on how to solve it). We can see the following, we got a flag.

Ok Google, I expected something more from you. I know I’m a genius, but I didn't think, that I would solve the task in 5 minutes. Ahh, the flag doesn’t right.

Exposition (solution idea)

Okay, I was insolently deceived and palmed off the wrong flag. Let's try to open the second level. Even it takes a long time to load …

Oh my god, can I go out the window? After that, no one saw the author of the write-up All right, maybe not everything is so bad there, and there is already an empty cell next to the red car? (After I couldn't find the red car) Every normal person would ask such a question, but I am a mega reverser immediately got into the source code of the game.

There could be a part about what I was stupid and trying to change the coordinates of one green car to get a flag. But that won't apply to the current solution, so I'll just mention it.

Having slightly analyzed the code + poking through the level files.

Let's roughly understand the structure of the levels: the first line is the size of the field, then there are objects in the format x, y, width, height, type (if type: 0 - wall; 1 - normal, gray car; -1 - green car; -2 - red car). The game itself is written in python and everything is quite clear in it, but I will note some useful things that will be used in the further solution.

board #dictionary matching: (x, y) -> the object at this position
blocks #list matching "number", car index with its x, y, width, height, type
target #variable containing the number of the red car 
def redraw(): #the function responsible for redrawing the field + on the first run saves the result of the initial position to a file 
def printflag(): #function that prints the flag, the output depends on the position of the green cars (if they changed position, then the flag bit corresponding to this car will be 1, otherwise 0) 

Knowing how the structure of the level file works, we will find in the figure red and green cars.

In the green sections (there are 64 of them) there are green cars, the red arrow (lower right corner) is pointing to the red car

Let's zoom to see it all closer

Okay, you know what? This all resembles logic circuits (+ hw after all). From the liveoverflow's video I remembered that they can be solved through z3 (mega solver of equations, inequalities and etc.), but I did not know how, so I decided to revise it.

https://www.youtube.com/watch?v=nI8Q1bqT8QU

P.S. As a result, I didn't even use it, but the video is still cool and useful. By the way, it is also about hardware Google ctf, only 2019.

Mini-task 1

Let's look at the simplest tasks with cars and understand our actions.

We need to move the red car, for this we:

1. we determine its possible directions of movement (horizontally / vertically).
2. where it can advance in theory, that is, where it is not the wall that prevents it from moving.
3. if a car prevents it from moving there, repeat everything for this car

Using such an algorithm, we can solve this task.

Mini-task 2

Let's look at a more difficult task

For it, we will have to slightly modify our algorithm, because if we just move the orange car to the right (as it should be according to the previous algorithm), then it will not clear the way. Therefore, we add 1 step to our algorithm

1. we determine its possible directions of movement (horizontally / vertically).
2. where it can advance in theory, that is, where it is not the wall that prevents it from moving.
3. see what prevents it from moving to the "possible position".
4. repeat for interfering machines, passing them the position to be cleared.

Mini-task 3

And consider the last example, in which we will discuss one subtlety of the algorithm.

In step 4, we have to do logical disjunction ('or', '|') for all the results of possible positions (this task will only contain 1-2).And logical conjunction ('and', '&') within the results themselves.

Better to explain with an example. For example, in mini-task 2, in order to move the red car, as a result, we need to move the blue AND purple car. Right there (mini-task 3), in order to move the red car we need to move the green OR blue one.

Uhhh, all that's left is to code this and give to z3.

Climax (coding)

Most of my bad are omitted in this part, as there were too many of them.

some_foo()

First, I'll make a function some_foo(), and place a call to it before drawing the initial field.

def some_foo():
    print("Yep i'm work")
    print(blocks[target])

Boom, it works.

get_obj(x, y)

Let's add:

• function get_obj(x, y), which will return what is at position x, y
• a function defining (isHorizintal(which)) how the car can move (horizontally / vertically)
• an important array that will contain the indices of the green cars.

SPACE=-2
important = []

def get_obj(x, y):
    if (x,y) in board:
        return board[(x, y)]
    else:
        return SPACE
        
def isHorizintal(which): #horiz==x vertical==y
    h=blocks[which][3]
    if(h == 1):
        return True
    else:
        return False
        
def some_foo():
    print("Yep i'm work") 
    for i in important:
        print(isHorizintal(i))
    print(getObj(3, 5))
    
[...]
walls = []
for line in boardfile.splitlines():
    if not line.strip(): continue
    x,y,w,h,movable = [int(x) for x in line.split()]
    if movable == -1:
        important.append(len(blocks)) #add
        flagblocks[len(blocks)] = (x,y)
[...]

Looks working

getMoveDir

There have been many attempts to add / modify the getMoveDir () function, but let's pretend that it was written correctly the first time Let's add some bad code and a function that will "test" our algorithm

• getMoveDir(which, free_x, free_y) - a recursive function that determines where the car can move
• MvDict - dictionary containing "machine index" -> direction
• MyTestBlocks - list containing numbers of "parsed" cars
• putparsecar(x,y,w,h,m) - the function that paints the cars from MyTestBlocks in blue, made to understand where getMoveDir() breaks
• also added sys.setrecursionlimit(150000), so that python doesn't break when parsing the second level

import sys
sys.setrecursionlimit(150000)

MvDict={}
MyTestBlocks=[]
def getMoveDir(which, free_x, free_y):
    x,y,w,h,mv=blocks[which]
    res=""
    if(isHorizintal(which)):
        check=1
        buf=[]
        for i in range(free_x+1, free_x+w+1):
            obj=getObj(i, y)
            if(obj != which):
                if((obj==WALL)):
                    check=0
                    break
                elif(obj!=SPACE):
                    buf.append([obj, i, y])
        if(check):
            res+="Right"
            for l in buf:
                getMoveDir(l[0], l[1], l[2])
        check=1
        buf=[]
        for i in range(free_x-w, free_x):
            obj=getObj(i, y)
            if(obj != which):
                if((obj==WALL)):
                    check=0
                    break
                elif(obj!=SPACE) :
                    buf.append([obj, i, y])
        if(check):
            res+="Left"
            for l in buf:
                getMoveDir(l[0], l[1], l[2])
    else:
        check=1
        buf=[]
        for i in range(free_y+1, free_y+h+1):
            obj=getObj(x, i)
            if(obj != which):
                if((obj==WALL)):
                    check=0
                    break
                elif(obj!=SPACE) :
                    buf.append([obj, x, i])
        if(check):
            res+="Down"
            for l in buf:
                getMoveDir(l[0], l[1], l[2])
        check=1
        buf=[]
        for i in range(free_y-h, free_y):
            obj=getObj(x, i)
            if(obj != which):
                if((obj==WALL)):
                    check=0
                    break
                elif(obj!=SPACE) :
                    buf.append([obj, x, i])
        if(check):
            res+="Up"
            for l in buf:
                getMoveDir(l[0], l[1], l[2])
    print(f"{which}: {blocks[which]}| {free_x}, {free_y} |{res}")
    return res

def putparsecar(x,y,w,h,m):
    x0 = x*SZ
    x1 = (x+w)*SZ
    y0 = y*SZ
    y1 = (y+h)*SZ
    color = (0, 0, 128)
    draw.rectangle((x0+1,y0+1,x1-2,y1-2), fill=color)


def some_foo():
    print("Yep i'm work") 
    x,y,w,h,mv=blocks[target]
    print(getMoveDir(target, x+w-1, y))
    

def redraw():
    [...]
    for block in blocks:
        putcar(*block)
    for block in MyTestBlocks: #add
        putparsecar(*block)
    [...]

Checking at level 1:

Checking at level 2 (had to be transferred to a file for more convenient analysis), reached all (64) green machines - success:

getBranch

Many attempts have been made here to get the getBranch() function to work properly, but I will talk about only one of them.

So now you need to rewrite the getMoveDir() function in getBranch(), changing its functionality to get under what conditions (with respect to green cars) the machine can free the given coordinates.

For this was added:

• inputs - list with variables (associated with green cars) for z3
• inp_dict - a dictionary that links the "green car index" -> its corresponding inputs[i]
• BranchDict - replacement of MvDict + was a bug. To eliminate infinite recursions, I forbade finding new directions for cars, which are in MvDict -> (see the picture) when the purple machine told blue to move, it "blocked" access to it. And after the yellow car thought that the blue == wall. And as a consequence, BranchDict matches not just which, but f" {which}_{free_x}_{free_y} " with the result of getBranch(which, free_x, free_y)

• function get_green_by_head() and workaround GREENHEAD - it marks the square above the green car to understand that the car can move into it only if the green one does not move
• the parseBranch function is applied to a branch and if it has several conditions, it connects them using AND

from z3 import *
s=Solver()
c_OR="Or("
c_NOT="Not("
c_AND="And("
GREENHEAD=-3

BranchDict={}#MvDict={}
inp_dict={}
inputs=[]

def get_green_by_head(x, y):
    return getObj(x, y+1)
    
def parseBranch(branch):
    if(len(branch)>0):
        if(len(branch)==1):
            res=branch[0]
        else:
            res=c_AND
            for s in branch:
               res+=s+", "
            res=res[0:-2]+")" 
    else:
        res=""
    return res

def getBranch(which, free_x, free_y):
    res=""
    #GREENHEAD
    if(which==GREENHEAD):
        res= c_NOT+getBranch( get_green_by_head(free_x,free_y),free_x,free_y)+")"
    else:
        x,y,w,h,mv=blocks[which]
        #Gree car
        if(mv==-1):
            if(inp_dict.get(which)==None):
                inputs.append(Bool('inputs[%s]' % len(inputs)))
                inp_dict.update({which: f"inputs[{len(inputs)-1}]"})
            res = inp_dict[which]
        #common car
        else:
            dictbuf=f"{which}_{free_x}_{free_y}"
            if(BranchDict.get(dictbuf)!=None):
                res=BranchDict.get(dictbuf)
                if(res==""):
                    res="False"
            else:
                branches=[[], []]
                BranchDict.update({dictbuf:res})
                if(isHorizintal(which)):
                    check=1
                    buf=[]
                    for i in range(free_x+1, free_x+w+1):
                        obj=getObj(i, y)
                        if(obj != which):
                            if((obj==WALL)):
                                check=0
                                break
                            elif(obj!=SPACE):
                                buf.append([obj, i, y])
                    if(check):
                        for l in buf:
                            branches[0].append(getBranch(l[0], l[1], l[2]))
                        if(len(buf)==0):
                            branches[0].append("True")
                    check=1
                    buf=[]
                    for i in range(free_x-w, free_x):
                        obj=getObj(i, y)
                        if(obj != which):
                            if((obj==WALL)):
                                check=0
                                break
                            elif(obj!=SPACE) :
                                buf.append([obj, i, y])
                    if(check):
                        for l in buf:
                            branches[1].append(getBranch(l[0], l[1], l[2]))
                        if(len(buf)==0):
                            branches[1].append("True")
                else:
                    check=1
                    buf=[]
                    for i in range(free_y+1, free_y+h+1):
                        obj=getObj(x, i)
                        if(obj != which):
                            if((obj==WALL)):
                                check=0
                                break
                            elif(obj!=SPACE) :
                                buf.append([obj, x, i])
                    if(check):
                        for l in buf:
                            branches[0].append(getBranch(l[0], l[1], l[2]))
                        if(len(buf)==0):
                            branches[0].append("True")
                    check=1
                    buf=[]
                    for i in range(free_y-h, free_y):
                        obj=getObj(x, i)
                        if(obj != which):
                            if((obj==WALL)):
                                check=0
                                break
                            elif(obj!=SPACE) :
                                buf.append([obj, x, i])
                    if(check):
                        for l in buf:
                            branches[1].append(getBranch(l[0], l[1], l[2]))
                        if(len(buf)==0):
                            branches[1].append("True")
                print(f"{which}: {blocks[which]}| {branches[0]}, {branches[1]}")
                if((len(branches[0])+len(branches[1]))==0):
                    res="False"
                elif (len(branches[0])>0 and len(branches[1])>0):
                    res+=c_OR
                    res+=parseBranch(branches[0])+","
                    res+=parseBranch(branches[1])+")"
                else:
                    for i in range(2):
                        res+=parseBranch(branches[i])

                MyTestBlocks.append(blocks[which])
                BranchDict.update({dictbuf:res})
    return res
    
def some_foo():
    
    print("Yep i'm work")
    x,y,w,h,mv=blocks[target]
    #print(getMoveDir(target, x+w-1, y))
    qua=getBranch(target, x+w-1, y)
    s.add(eval(qua))
    print(s.check())
    print("Bits of flag:")
    flag=""
    for ind in important:
        var=eval(inp_dict[ind])
        bit=str(int(s.model()[var].__bool__()))
        print(bit, end="")
    print()

walls = []
for line in boardfile.splitlines():
    [...]
    if movable==-1: #add
        board[(x,y-1)] = GREENHEAD
    if movable:
        blocks.append([x,y,w,h, movable])
    [...]

Yuhu, it was able to solve the first level:

But with the second, some problems occur (of course, if at first your computer is not dead from the amount of garbage that the script throws out):

z3.simplify()

Ok, maybe it should have been done at beginning, but I just thought of it now - add simplify(). Deal with everything at once. Just condition on True, False been added, otherwise it breaks.

def getBranch(which, free_x, free_y):
    [...]
    if(res!="True") and (res!="False"):
        return str(simplify(eval(res)))
    return res

… I'll just keep silent, and note that now the program crashes due to the fact that eval cuts long lines (~10k characters) using ... and z3 breaks when trying to parse them.

main_dots

As a result, it was decided to create such a thing as a list of control points main_dots, and write there z3's variables that would be equal to formulas, the length of which is more than 1000.

def getBranch(which, free_x, free_y):
    [...]
                if(len(res)>1000):
                    ln=len(main_dots)
                    main_dots.append(Bool('main_dots[%s]' % ln))
                    s.add(eval(f'main_dots[{ln}]=={res}'))
                    res=f'main_dots[{ln}]'
                MyTestBlocks.append(blocks[which])
                BranchDict.update({dictbuf:res})
    if(res!="True") and (res!="False"):
        return str(simplify(eval(res)))
    return res

Launch it, wait and get the necessary bits (0100110000101010000101101010011001000010010011101000110010110110).

Resolution (getting the flag)

Go to cyberchef. We shove the bits …

And we don't get the flag. Dead end. Let's start to reverse engineering

Ooh, understandable letters, only meaningless, but okay, let's try to pass CTF{m1rBehT2}.

Doesn't pass( Let's try to reverse further

Uh-huh, it sounds and looks cool, pass CTF{2TheBr1m}

Easy game, easy life Easy flag, hard CTF

Solution

• understand that there is no way to cheat and what needs to be solved level2
• understand that level2 is like a logic circuit -> can be solved by z3
• convert level2 to logic circuit
• give it to z3
• get flag bits -> get flag

Solver script

Usage: python3 solver.py level2 and go and have some tea (wait about 10-20 minutes or more).

from z3 import *
import sys
sys.setrecursionlimit(150000)

WALL = -1
SPACE=-2
GREENHEAD=-3

blocks = []
board = {}

s=Solver()
c_OR="Or("
c_NOT="Not("
c_AND="And("


BranchDict={}
inp_dict={}
inputs=[]
MyTestBlocks=[]
main_dots=[]
important = []

def Myprintflag(bits):
    flag = b"CTF{"
    while bits:
        byte, bits = bits[:8], bits[8:]
        flag += bytes([ int(byte[::-1], 2) ])
    flag += b"}"
    print(flag)

def getObj(x, y):
    if (x,y) in board:
        return board[(x, y)]
    else:
        return SPACE
        
def isHorizintal(which): #horiz==x vertical==y
    h=blocks[which][3]
    if(h == 1):
        return True
    else:
        return False

def get_green_by_head(x, y):
    return getObj(x, y+1)

def parseBranch(branch):
    if(len(branch)>0):
        if(len(branch)==1):
            res=branch[0]
        else:
            res=c_AND
            for s in branch:
               res+=s+", "
            res=res[0:-2]+")" 
    else:
        res=""
    return res


def getBranch(which, free_x, free_y):
    res=""
    #GREENHEAD
    if(which==GREENHEAD):
        res= c_NOT+getBranch( get_green_by_head(free_x,free_y),free_x,free_y)+")"
    else:
        x,y,w,h,mv=blocks[which]
        #Gree car
        if(mv==-1):
            if(inp_dict.get(which)==None):
                inputs.append(Bool('inputs[%s]' % len(inputs)))
                inp_dict.update({which: f"inputs[{len(inputs)-1}]"})
            res = inp_dict[which]
        #common car
        else:
            dictbuf=f"{which}_{free_x}_{free_y}"
            if(BranchDict.get(dictbuf)!=None):
                res=BranchDict.get(dictbuf)
                if(res==""):
                    res="False"
            else:
                branches=[[], []]
                BranchDict.update({dictbuf:res})
                if(isHorizintal(which)):
                    check=1
                    buf=[]
                    for i in range(free_x+1, free_x+w+1):
                        obj=getObj(i, y)
                        if(obj != which):
                            if((obj==WALL)):
                                check=0
                                break
                            elif(obj!=SPACE):
                                buf.append([obj, i, y])
                    if(check):
                        for l in buf:
                            branches[0].append(getBranch(l[0], l[1], l[2]))
                        if(len(buf)==0):
                            branches[0].append("True")
                    check=1
                    buf=[]
                    for i in range(free_x-w, free_x):
                        obj=getObj(i, y)
                        if(obj != which):
                            if((obj==WALL)):
                                check=0
                                break
                            elif(obj!=SPACE) :
                                buf.append([obj, i, y])
                    if(check):
                        for l in buf:
                            branches[1].append(getBranch(l[0], l[1], l[2]))
                        if(len(buf)==0):
                            branches[1].append("True")
                else:
                    check=1
                    buf=[]
                    for i in range(free_y+1, free_y+h+1):
                        obj=getObj(x, i)
                        if(obj != which):
                            if((obj==WALL)):
                                check=0
                                break
                            elif(obj!=SPACE) :
                                buf.append([obj, x, i])
                    if(check):
                        for l in buf:
                            branches[0].append(getBranch(l[0], l[1], l[2]))
                        if(len(buf)==0):
                            branches[0].append("True")
                    check=1
                    buf=[]
                    for i in range(free_y-h, free_y):
                        obj=getObj(x, i)
                        if(obj != which):
                            if((obj==WALL)):
                                check=0
                                break
                            elif(obj!=SPACE) :
                                buf.append([obj, x, i])
                    if(check):
                        for l in buf:
                            branches[1].append(getBranch(l[0], l[1], l[2]))
                        if(len(buf)==0):
                            branches[1].append("True")
                #print(f"{which}: {blocks[which]}| {branches[0]}, {branches[1]}")
                if((len(branches[0])+len(branches[1]))==0):
                    res="False"
                elif (len(branches[0])>0 and len(branches[1])>0):
                    res+=c_OR
                    res+=parseBranch(branches[0])+","
                    res+=parseBranch(branches[1])+")"
                else:
                    for i in range(2):
                        res+=parseBranch(branches[i])
                if(len(res)>1000):
                    ln=len(main_dots)
                    main_dots.append(Bool('main_dots[%s]' % ln))
                    s.add(eval(f'main_dots[{ln}]=={res}'))
                    res=f'main_dots[{ln}]'
                MyTestBlocks.append(blocks[which])
                BranchDict.update({dictbuf:res})
    if(res!="True") and (res!="False"):
        return str(simplify(eval(res)))
    return res

def some_foo():
    print("You should wait!")
    x,y,w,h,mv=blocks[target]
    qua=getBranch(target, x+w-1, y)
    s.add(eval(qua))
    print(s.check())
    flag=""
    for ind in important:
        var=eval(inp_dict[ind])
        bit=str(int(s.model()[var].__bool__()))
        flag+=bit
    Myprintflag(flag)


boardfile = open(sys.argv[1]).read()
header, boardfile = boardfile.split("\n", 1)
W, H = [int(x) for x in header.split()]
target = -1

walls = []
for line in boardfile.splitlines():
    if not line.strip(): continue
    x,y,w,h,movable = [int(x) for x in line.split()]

    if movable == -1: #add
        important.append(len(blocks)) 
    elif movable == -2:
        target = len(blocks)

    for i in range(x, x+w):
        for j in range(y, y+h):
            if movable != 0:
                if (i,j) in board:
                    print("Car overlap at %d, %d" % (i,j))
                    #assert False
                board[(i,j)] = len(blocks)
            else:
                if (i,j) in board and board[i,j] != WALL:
                    print("Wall-car overlap at %d, %d" % (i,j))
                    #assert False
                board[(i,j)] = WALL
    if movable==-1:#add
        board[(x,y-1)] = GREENHEAD
    if movable:
        blocks.append([x,y,w,h, movable])
    else:
        walls.append([x,y,w,h])

some_foo()

Epilogue

While making the script more beautiful, freed from unnecessary functions, accidentally removed s.check(). I started it to check, but it crashes. I was already panic that while I was writing the write-up I messed up something in the script, and as a result I also put the crooked code somewhere here, and I would have to rewrite it almost from scratch. And also, when I was rewriting the code, I somehow missed the GREENHEADs, which again made me nervous, because it led to the wrong flag. Yes, in general I shouldn't be allowed to code and everything connected with it, if I make such mistakes while rewriting my code. Sorry me for my english