# TJCTF 2024 Reverse Engineer Writeup In this write-up, I will discuss my solutions for two reversing challenges: [cagnus-marlsen](##cagnus-marlsen) and [slider](##slider). Unfortunately, I didn't have enough time to solve more challenges, but I made significant progress with these two. ![image](https://hackmd.io/_uploads/BJHid5uXA.png) ## cagnus-marlsen There's just one attachment `endgamemaker.py`, running the script we could see a GUI game. ![image](https://hackmd.io/_uploads/HJeMK5_m0.png) Based on the name it suppose to tell use which side will gonna win, we could fill black or fill white then the program will printed out which side is win, but what is the objective for us to get the holy moly `flag`. Since it's just a python script we could directly read the source, so open up your favorite code editor we could see this. ```python!= import tkinter global root, myCanvas root = tkinter.Tk() myCanvas = tkinter.Canvas(root, bg="white", height=320, width=320) turn = 0 grid = [0]*64 def selectWhite(): global turn turn = 1 L3.config(text="Filling white") def selectBlack(): global turn turn = 0 L3.config(text="Filling black") def verify(): b0 = int(''.join(str(i) for i in grid[0:8]), 2) b1 = int(''.join(str(i) for i in grid[8:16]), 2) b2 = int(''.join(str(i) for i in grid[16:24]), 2) b3 = int(''.join(str(i) for i in grid[24:32]), 2) b4 = int(''.join(str(i) for i in grid[32:40]), 2) b5 = int(''.join(str(i) for i in grid[40:48]), 2) b6 = int(''.join(str(i) for i in grid[48:56]), 2) b7 = int(''.join(str(i) for i in grid[56:64]), 2) b8 = int(''.join(str(i) for i in grid[0:64:8]), 2) b9 = int(''.join(str(i) for i in grid[1:64:8]), 2) b10 = int(''.join(str(i) for i in grid[2:64:8]), 2) b11 = int(''.join(str(i) for i in grid[3:64:8]), 2) b12 = int(''.join(str(i) for i in grid[4:64:8]), 2) b13 = int(''.join(str(i) for i in grid[5:64:8]), 2) b14 = int(''.join(str(i) for i in grid[6:64:8]), 2) b15 = int(''.join(str(i) for i in grid[7:64:8]), 2) b16 = int(''.join(str(i) for i in grid[0:64:9]), 2) b17 = int(''.join(str(i) for i in grid[7:63:7]), 2) touchesgrass = True touchesgrass &= grid[1]+grid[10]+grid[62] == 2 touchesgrass &= (grid[15] > grid[23]) touchesgrass &= grid[9]+grid[10]+grid[14] == 2 touchesgrass &= grid[26] << 3 == grid[43]+grid[44] touchesgrass &= (grid[32]+grid[33] < grid[1] + grid[62]) touchesgrass &= (sum(int(i)==int(j) for i,j in [*zip(format(b2,"#010b"),format(b4,"#010b"))][2:]))==3 touchesgrass &= bin(b6).count('1') == 5 touchesgrass &= grid[61] + grid[42] + grid[43] == grid[25] + grid[26] + grid[27] touchesgrass &= grid[38]+grid[46]+grid[54]+grid[62]+grid[39]+grid[47]+grid[55]+grid[63] == 5 touchesgrass &= (grid[14]^1!=grid[15]) touchesgrass &= grid[57] + grid[59] + grid[60] == 3 touchesgrass &= grid[18] != grid[23] touchesgrass &= grid[11]^grid[19]==1 touchesgrass &= grid[50]==grid[51] touchesgrass &= grid[20]^grid[7]==1 touchesgrass &= (grid[63]>>1 != grid[63]<<1) touchesgrass &= (sum(int(i)!=int(j) for i,j in [*zip(format(b9,"#010b"),format(b1,"#010b"))][2:]))==2 touchesgrass &= grid[57] + grid[58] + grid[59] == 2 touchesgrass &= grid[37]|grid[38] == grid[2] touchesgrass &= grid[4]==grid[48]==grid[49] touchesgrass &= grid[17] >=grid[30] touchesgrass &= (grid[0] == grid[19]) touchesgrass &= grid[26] + grid[28] + grid[29] == grid[51] << 1 touchesgrass &= grid[3] + grid[5] + grid[55] == 1 touchesgrass &= (grid[30]==grid[34]) touchesgrass &= sum(grid[14:17]) > grid[56] + grid[30] + grid[47] touchesgrass &= grid[7]!=grid[52] touchesgrass &= (b16//4)%2==0 touchesgrass &= grid[8] == grid[9] touchesgrass &= (sum(int(i)!=int(j) for i,j in [*zip(format(b16,"#010b"),format(b15,"#010b"))][2:]))==3 touchesgrass &= grid[6]^grid[56]==0 touchesgrass &= (sum(grid[30:36])==3) touchesgrass &= grid[24]+grid[40] == grid[2] touchesgrass &= ~(grid[27]^grid[22])==-1 touchesgrass &= grid[11]^grid[12]^grid[13]==grid[12]==grid[4] touchesgrass &= grid[31] == grid[47] touchesgrass &= grid[47]^grid[46] == 1 touchesgrass &= grid[10] * 2 == grid[25] * 2 + grid[41] if(touchesgrass): return 'tjctf{'+chr(b2)+chr(b9)+chr(b15)+chr(b16)+chr(b7)+chr(b4)+chr(b10)+chr(b12)+'}' else: return touchesgrass def clicked(event): row = max(0,min(320,event.y))//40 col = max(0,min(320,event.x))//40 grid[row*8+col] = turn myCanvas.create_oval(40*col+5, 40*row+5, 40*(col+1)-5, 40*(row+1)-5, fill=("white" if turn==1 else "black")) L2.config(text=f"{'Black wins' if grid.count(0)>grid.count(1) else 'White wins' if grid.count(0)<grid.count(1) else 'Tie' } {grid.count(0)}-{grid.count(1)}") if((thefunny:=verify())): print("yay you're a winner") print(thefunny) # exit() print(grid, verify()) def makeCanvas(root, myCanvas): global L2, L3 L1 = tkinter.Label(root, text="Othello endgame generator") L1.config(font=("Courier",20)) L1.pack() btn = tkinter.Button(root, text="Fill black", height=25, bd='5',command=selectBlack) btn.pack(side='left') btn = tkinter.Button(root, text="Fill white", height=25, bd='5',command=selectWhite) btn.pack(side='right') for r in range(0,8): for c in range(0,8): myCanvas.create_rectangle(r*40, c*40, (r+1)*40, (c+1)*40, fill='green') myCanvas.create_oval(40*r+5, 40*c+5, 40*(r+1)-5, 40*(c+1)-5, fill="black") myCanvas.bind("<Button-1>", clicked) myCanvas.pack() L2= tkinter.Label(root, text="Black wins 64-0") L2.config(font=("Courier",20)) L2.pack() L3= tkinter.Label(root, text="Filling black") L3.config(font=("Courier",20)) L3.pack() makeCanvas(root, myCanvas) root.mainloop() ``` The python code wasn't obfuscated as we see, so it easier for us to look around and wondering how we could get the flag. To sumarry the code it using `tkinter` for its GUI framework, skip that part we could see an array called grid that has 64 integer all initialized to 0, this catch up what we see before, we see all black circles so we may recognize that `black` is 0 and `white` is 1, and we know that somehow it's represented as 8x8 matrix, there're some other functions but what catch our eyes is `verify` function. Reading verify function is easy, first it initialize b-series variable that uses row, column, and diagonal value from our 8x8 matrix, treat it as a binary data and converting it to integer value. Then we could see `touchesgrass` initialize with `True` then there're some condition to satisfy so it will printed us the `flag`. My first thought reading this function was, this is easy with `z3` (efficient SMT solver from Microsoft Research). But there's some funny condition that i found hard to convert as `z3` constraint, yes definitely a skill issue stuff going here. Before going directly to `z3` solver, i tried to simplify the condition, for example like this condition ```python! touchesgrass &= (grid[63]>>1 != grid[63]<<1) ``` i turned it into ```python touchesgrass &= (grid[63] == 1) ``` since `1 >> 1 ! = 1 << 1`. after playing around with the condition myself, this is the final simplified condition. ```python!= # one operand touchesgrass &= grid[14] == 1 touchesgrass &= grid[15] == 1 touchesgrass &= grid[18] == 1 touchesgrass &= grid[23] == 0 touchesgrass &= grid[26] == 0 touchesgrass &= grid[43] == 0 touchesgrass &= grid[44] == 0 touchesgrass &= grid[57] == 1 touchesgrass &= grid[58] == 0 touchesgrass &= grid[59] == 1 touchesgrass &= grid[60] == 1 touchesgrass &= grid[63] == 1 # two operand touchesgrass &= grid[7]!=grid[52] touchesgrass &= grid[20]!=grid[7] touchesgrass &= grid[11]!=grid[19] touchesgrass &= grid[47]!=grid[46] touchesgrass &= grid[4]==grid[48] touchesgrass &= grid[4]==grid[49] touchesgrass &= grid[4]==grid[12] touchesgrass &= (grid[0] == grid[19]) touchesgrass &= (grid[30]==grid[34]) touchesgrass &= grid[27] == grid[22] touchesgrass &= grid[50]==grid[51] touchesgrass &= grid[8] == grid[9] touchesgrass &= grid[6]==grid[56] touchesgrass &= grid[31] == grid[47] touchesgrass &= grid[17] >=grid[30] # 3 operands touchesgrass &= grid[1]+grid[10]+grid[62] == 2 touchesgrass &= grid[9]+grid[10]+grid[14] == 2 touchesgrass &= grid[37]|grid[38] == grid[2] touchesgrass &= grid[24]+grid[40] == grid[2] touchesgrass &= grid[3] + grid[5] + grid[55] == 1 touchesgrass &= (grid[32]+grid[33]) < (grid[1] + grid[62]) touchesgrass &= (grid[10] * 2) == (grid[25] * 2 + grid[41]) # more than 3 operands touchesgrass &= (grid[61] + grid[42] + grid[43]) == (grid[25] + grid[26] + grid[27]) touchesgrass &= grid[11]^grid[12]^grid[13]==grid[12] touchesgrass &= grid[26] + grid[28] + grid[29] == grid[51] << 1 touchesgrass &= (grid[38]+grid[46]+grid[54]+grid[62]+grid[39]+grid[47]+grid[55]+grid[63])==5 touchesgrass &= (grid[14] + grid[15] + grid[16]) > (grid[56] + grid[30] + grid[47]) touchesgrass &= grid[30] + grid[31] + grid[32] + grid[33] + grid[34] + grid[35] == 3 touchesgrass &= (((grid[0]<<7)+(grid[9]<<6)+(grid[18]<<5)+(grid[27]<<4)+(grid[36]<<3)+(grid[45]<<2)+(grid[54]<<1)+grid[63])//4)%2==0 touchesgrass &= (grid[48]+grid[49]+grid[50]+grid[51]+grid[52]+grid[53]+grid[54]+grid[55])== 5 touchesgrass &= ((grid[16]==grid[32])+(grid[17]==grid[33])+(grid[18]==grid[34])+(grid[19]==grid[35])+(grid[20]==grid[36])+(grid[21]==grid[37])+(grid[22]==grid[38])+(grid[23]==grid[39]))==3 touchesgrass &= ((grid[1]!=grid[8])+(grid[9]!=grid[9])+(grid[17]!=grid[10])+(grid[25]!=grid[11])+(grid[33]!=grid[12])+(grid[41]!=grid[13])+(grid[49]!=grid[14])+(grid[57]!=grid[15]))==2 touchesgrass &= ((grid[0]!=grid[7])+(grid[9]!=grid[15])+(grid[18]!=grid[23])+(grid[27]!=grid[31])+(grid[36]!=grid[39])+(grid[45]!=grid[47])+(grid[54]!=grid[55])+(grid[63]!=grid[63]))==3 ``` let's shove this condition to z3 and get the result! <div style="width:100%;height:0;padding-bottom:100%;position:relative;"><iframe src="https://giphy.com/embed/Q8IYWnnogTYM5T6Yo0" width="100%" height="100%" style="position:absolute" frameBorder="0" class="giphy-embed" allowFullScreen></iframe></div> ``` tjctf{ö3׳_ lÁ} ``` And i got a funny flag, but apparently there's more than 1 solution, i don't know the exact amount of solution it has, but i think there's just one that will printed all ascii chars. And the author also said this. ![image](https://hackmd.io/_uploads/SkQ_fjdXA.png) So let's make a `z3` solver that will printed all possible values. Here's the final solve script. ```python!= from z3 import * # Create the Z3 solver instance solver = Solver() # Define the grid as an array of Z3 integer variables grid = [BitVec(f'grid_{i}',8) for i in range(64)] for i in range(64): solver.add(Or(grid[i] == 0, grid[i] == 1)) # Add constraints based on the provided Python conditions solver.add(grid[14] == 1) solver.add(grid[15] == 1) solver.add(grid[18] == 1) solver.add(grid[23] == 0) solver.add(grid[26] == 0) solver.add(grid[43] == 0) solver.add(grid[44] == 0) solver.add(grid[57] == 1) solver.add(grid[58] == 0) solver.add(grid[59] == 1) solver.add(grid[60] == 1) solver.add(grid[63] == 1) # Two operand constraints solver.add(grid[7] != grid[52]) solver.add(grid[20] != grid[7]) solver.add(grid[11] != grid[19]) solver.add(grid[47] != grid[46]) solver.add(grid[4] == grid[48]) solver.add(grid[4] == grid[49]) solver.add(grid[12] == grid[4]) solver.add(grid[0] == grid[19]) solver.add(grid[30] == grid[34]) solver.add(grid[27] == grid[22]) solver.add(grid[50] == grid[51]) solver.add(grid[8] == grid[9]) solver.add(grid[6] == grid[56]) solver.add(grid[31] == grid[47]) # solver.add(grid[17] >= grid[30]) solver.add(UGE(grid[17], grid[30])) # Three operand constraints solver.add(grid[1] + grid[10] + grid[62] == 2) solver.add(grid[9] + grid[10] + grid[14] == 2) solver.add(grid[37] | grid[38] == grid[2]) solver.add(grid[24] + grid[40] == grid[2]) solver.add(grid[3] + grid[5] + grid[55] == 1) solver.add(grid[32] + grid[33] < grid[1] + grid[62]) solver.add(grid[10] * 2 == grid[25] * 2 + grid[41]) # More than three operand constraints solver.add(grid[61] + grid[42] + grid[43] == grid[25] + grid[26] + grid[27]) solver.add(grid[11] ^ grid[12] ^ grid[13] == grid[12]) solver.add(grid[26] + grid[28] + grid[29] == (grid[51] << 1)) solver.add((grid[14] + grid[15] + grid[16]) > (grid[56] + grid[30] + grid[47])) solver.add(grid[30] + grid[31] + grid[32] + grid[33] + grid[34] + grid[35] == 3) solver.add(grid[38] + grid[46] + grid[54] + grid[62] + grid[39] + grid[47] + grid[55] + grid[63] == 5) solver.add((grid[48] + grid[49] + grid[50] + grid[51] + grid[52] + grid[53] + grid[54] + grid[55]) == 5) solver.add((LShR(((grid[0]<<7)+(grid[9]<<6)+(grid[18]<<5)+(grid[27]<<4)+(grid[36]<<3)+(grid[45]<<2)+(grid[54]<<1)+grid[63]), 2) & 1) == 0) # Complex constraints solver.add(Sum([If(grid[16] == grid[32], 1, 0), If(grid[17] == grid[33], 1, 0), If(grid[18] == grid[34], 1, 0), If(grid[19] == grid[35], 1, 0), If(grid[20] == grid[36], 1, 0), If(grid[21] == grid[37], 1, 0), If(grid[22] == grid[38], 1, 0), If(grid[23] == grid[39], 1, 0)]) == 3) solver.add(Sum([If(grid[1] != grid[8], 1, 0), If(grid[9] != grid[9], 1, 0), If(grid[17] != grid[10], 1, 0), If(grid[25] != grid[11], 1, 0), If(grid[33] != grid[12], 1, 0), If(grid[41] != grid[13], 1, 0), If(grid[49] != grid[14], 1, 0), If(grid[57] != grid[15], 1, 0)]) == 2) solver.add(Sum([If(grid[0] != grid[7], 1, 0), If(grid[9] != grid[15], 1, 0), If(grid[18] != grid[23], 1, 0), If(grid[27] != grid[31], 1, 0), If(grid[36] != grid[39], 1, 0), If(grid[45] != grid[47], 1, 0), If(grid[54] != grid[55], 1, 0), If(grid[63] != grid[63], 1, 0)]) == 3) def verify(grid): b0 = int(''.join(str(i) for i in grid[0:8]), 2) b1 = int(''.join(str(i) for i in grid[8:16]), 2) b2 = int(''.join(str(i) for i in grid[16:24]), 2) b3 = int(''.join(str(i) for i in grid[24:32]), 2) b4 = int(''.join(str(i) for i in grid[32:40]), 2) b5 = int(''.join(str(i) for i in grid[40:48]), 2) b6 = int(''.join(str(i) for i in grid[48:56]), 2) b7 = int(''.join(str(i) for i in grid[56:64]), 2) b8 = int(''.join(str(i) for i in grid[0:64:8]), 2) b9 = int(''.join(str(i) for i in grid[1:64:8]), 2) b10 = int(''.join(str(i) for i in grid[2:64:8]), 2) b11 = int(''.join(str(i) for i in grid[3:64:8]), 2) b12 = int(''.join(str(i) for i in grid[4:64:8]), 2) b13 = int(''.join(str(i) for i in grid[5:64:8]), 2) b14 = int(''.join(str(i) for i in grid[6:64:8]), 2) b15 = int(''.join(str(i) for i in grid[7:64:8]), 2) b16 = int(''.join(str(i) for i in grid[0:64:9]), 2) b17 = int(''.join(str(i) for i in grid[7:63:7]), 2) touchesgrass = True touchesgrass &= grid[1]+grid[10]+grid[62] == 2 touchesgrass &= (grid[15] > grid[23]) touchesgrass &= grid[9]+grid[10]+grid[14] == 2 touchesgrass &= grid[26] << 3 == grid[43]+grid[44] touchesgrass &= (grid[32]+grid[33] < grid[1] + grid[62]) touchesgrass &= (sum(int(i)==int(j) for i,j in [*zip(format(b2,"#010b"),format(b4,"#010b"))][2:]))==3 touchesgrass &= bin(b6).count('1') == 5 touchesgrass &= grid[61] + grid[42] + grid[43] == grid[25] + grid[26] + grid[27] touchesgrass &= grid[38]+grid[46]+grid[54]+grid[62]+grid[39]+grid[47]+grid[55]+grid[63] == 5 touchesgrass &= (grid[14]^1!=grid[15]) touchesgrass &= grid[57] + grid[59] + grid[60] == 3 touchesgrass &= grid[18] != grid[23] touchesgrass &= grid[11]^grid[19]==1 touchesgrass &= grid[50]==grid[51] touchesgrass &= grid[20]^grid[7]==1 touchesgrass &= (grid[63]>>1 != grid[63]<<1) touchesgrass &= (sum(int(i)!=int(j) for i,j in [*zip(format(b9,"#010b"),format(b1,"#010b"))][2:]))==2 touchesgrass &= grid[57] + grid[58] + grid[59] == 2 touchesgrass &= grid[37]|grid[38] == grid[2] touchesgrass &= grid[4]==grid[48]==grid[49] touchesgrass &= grid[17] >=grid[30] touchesgrass &= (grid[0] == grid[19]) touchesgrass &= grid[26] + grid[28] + grid[29] == grid[51] << 1 touchesgrass &= grid[3] + grid[5] + grid[55] == 1 touchesgrass &= (grid[30]==grid[34]) touchesgrass &= sum(grid[14:17]) > grid[56] + grid[30] + grid[47] touchesgrass &= grid[7]!=grid[52] touchesgrass &= (b16//4)%2==0 touchesgrass &= grid[8] == grid[9] touchesgrass &= (sum(int(i)!=int(j) for i,j in [*zip(format(b16,"#010b"),format(b15,"#010b"))][2:]))==3 touchesgrass &= grid[6]^grid[56]==0 touchesgrass &= (sum(grid[30:36])==3) touchesgrass &= grid[24]+grid[40] == grid[2] touchesgrass &= ~(grid[27]^grid[22])==-1 touchesgrass &= grid[11]^grid[12]^grid[13]==grid[12]==grid[4] touchesgrass &= grid[31] == grid[47] touchesgrass &= grid[47]^grid[46] == 1 touchesgrass &= grid[10] * 2 == grid[25] * 2 + grid[41] if(touchesgrass): return 'tjctf{'+chr(b2)+chr(b9)+chr(b15)+chr(b16)+chr(b7)+chr(b4)+chr(b10)+chr(b12)+'}' else: return touchesgrass def extract_model(m): return [m.eval(grid[i]).as_long() for i in range(64)] i = 0 solutions = [] while solver.check() == sat: model = solver.model() solutions.append(extract_model(model)) # Add a constraint to block the current solution solver.add(Or([grid[i] != model[grid[i]] for i in range(64)])) i+= 1 print(i) for solution in solutions: print(verify(solution)) ``` then search for the one that print all ascii chars. ![image](https://hackmd.io/_uploads/rkzq-ouQR.png) we got the flag : `tjctf{n1C3_0n3}` ## slider This one is my favourite, given 2 files, `save.dat` and `slider`, `save.dat` is just a binary data, while `slider` is the real deal. directly running the binary we could see this. ![image](https://hackmd.io/_uploads/rkyEdiOmA.png) but it get randomized each time we run it. ![image](https://hackmd.io/_uploads/r1Jsdi_QR.png) since it looks like a game we can move the blurry block with wasd or arrow key. yeah this definitely a sliding puzzle, i directly search on how to solve a 5x5 sliding puzzle and i got this https://www.wikihow.com/Solve-Slide-Puzzles (at the end i don't even use it to solve this chall). the movement is pretty anoyying since for me it's kinda flipped, like when i press `w` the block goes down, so i need to patch this shit. Okay, we know it's a puzzle, but which block goes where?, it's a sign to open up our decompiler, i'll use binary ninja, but towards the solve i use ghidra more, later about it. quick see the flow of main function. ![image](https://hackmd.io/_uploads/ryp6is_70.png) reading it a bit, we could see the corelation between `slider` binary and the `save.dat`, looks like all the important data is in `save.dat`. ![image](https://hackmd.io/_uploads/SJQmnoOXC.png) it read and then there's a check for `isSolved`, when it's solved they `shuffled` our data, i continue reading the function and i don't see any other call for `shuffled` other than when it's solved or when we press `l`, so what's the meaning of our randomized block each time we start the binary?? you guess it. and indeed i check it with gdb if our `save.dat` is already in solved condition. ![image](https://hackmd.io/_uploads/rJ7IpouQC.png) so forget about patching the movement key, we got bigger fish to catch here, why not just patch the `shuffled` so we don't get shuffled for the first time. and now it's time for ghidra to shine, i like patching binary in ghidra, because i don't know how to do it in ida free or binary ninja free, wait is that even possible in the first place?? skill issue? yes. to patch in ghidra is pretty simple, u just need to open up ur ghidra and right click and select patch instruction. ![image](https://hackmd.io/_uploads/B1BkkhdX0.png) this were i patched the binary so if 1 (solved) we got shuffled then i'll just reverse the logic, and now let's see the result. ![image](https://hackmd.io/_uploads/ryu-k3d70.png) oh yeah hidden flag is showed up in the corner, but something is a bit off, because you see the blurry block is still there, and our cat is gone, and when i try to run it again. ![image](https://hackmd.io/_uploads/SJzDy3_XA.png) like what just happen, didn't i patched the shuffled thing, let's step aback and search what causes it. there's a funny story actually, at first i think this is the culprit ![image](https://hackmd.io/_uploads/BypqM2O7C.png) i think sort was messing with the data from `save.dat`, so it makes my program funny, so i think i need to patch it, but my dumb ass misclick a function and patched `isSolved` instead, i see a call instruction and thought that it's call for sort, but actually it's this ![image](https://hackmd.io/_uploads/S1iuX3dmC.png) this is the function to get data from vector, and then the value got compared, i `nop`-ed it so it makes my `isSolved` always return false. Here's the binary when we run it. ![image](https://hackmd.io/_uploads/rylLWHn_QA.png) it's looks like in correct order, i guess misspatch for the win?? there's silly little chars that actually a flag, it's not just `slider like` and the `514a` is the flag, but as u can see those little chars forming `do you mean` string. `tjctf{do_you_mean_slider_like_the_burger_or_like_you_hardly_know_er_514a5f61}`