Mine the Gap [Google Ctf 2023]
Challenge Description
Take a break from the other challenges and play a relxing game of Minesweeper I have even solved most of the board for you and marked many of the mines. I am completely sure they are correct so you just need to find the remaining ones.
Intuition
Looking at the minesweeper map, it’s huge, but I noticed that the patterns look like wires and seem to lead to some structure which intuitively resemble logic gates. Even more, there are multiple mentions in the code of circuits. So I searched on the internet for something related to minesweeper and circuits and found a paper from 2015 1 which proves that Minesweeper is np-complete using circuits which look exactly like the ones in the challenge.
An initial idea that results is that we could convert the map to a logic circuit and input it into a sat-solver like z3. Now… that’s kinda complicated.
The map being partially solved, consistent and built like a circuit means that giving in input to each end of the wire (aka putting a bomb or not there), should result in a unique arrangement for the entire map. Intuitively, this means that the whole map can be converted into a logic formula and fed to as sat solver.
Solution
After some more research, I found a github repo with a minesweeper sat solver 2 which structured the map in a very similar way with the one in the given challenge. I modified the code such that it fit the problem:
from pysat.solvers import Solver #for SAT solving
from itertools import combinations #for combinations in a CNF
import itertools
import hashlib
# DIMACS codification
def M(i,j,board_w): return board_w**1 * i + board_w**0 * j + 1
# find unknown cells next to a cell at i,j
def unknown_neighbours(board,i,j):
neighbours=[]
for h in range(i-1,i+2):
for w in range(j-1,j+2):
if h<len(board) and w<len(board[0]) and h>=0 and w>=0 and (board[h][w]>8): neighbours.append((h,w))
return neighbours
# clauses per cell
def cell_clauses(board,i,j):
neighbours=unknown_neighbours(board,i,j)
cell_clauses=[]
#at least n mines
for combination in combinations([M(elem[0],elem[1],len(board[0])) for elem in neighbours],len(neighbours)-board[i][j]+1):
cell_clauses.append(list(combination))
#at most n mines
for combination in combinations([-M(elem[0],elem[1],len(board[0])) for elem in neighbours], board[i][j]+1):
cell_clauses.append(list(combination))
return cell_clauses
# clauses per board
def board_clauses(board,board_h,board_w):
clauses=[]
for i in range(board_h):
for j in range(board_w):
if board[i][j]<9:
#add self as known safe cell
clauses.append([-M(i,j,board_w)])
#add surrounding constraints
clauses+=cell_clauses(board,i,j)
elif board[i][j]==10:
#add self as mine cell
clauses.append([M(i,j,board_w)])
return clauses
#print solution
def show_solution(board,board_h,board_w,model):
bits = []
for i in range(board_h):
for j in range(board_w):
if board[i][j]==9:
board[i][j]='m' if M(i, j,board_w) in model else 's'
if i == 23:
bit = 1 if board[i][j] == 'm' else 0
bits.append(bit)
flag = hashlib.sha256(bytes(bits)).hexdigest()
print(f'Flag: CTF{{{flag}}}')
def solve_board(board,printing=True):
if printing:
print("Legend:\n0-8: mines nearby\n9 : unknown\n10 : known mine")
board_w=len(board[0])
board_h=len(board)
s = Solver(name='cd')
s.append_formula(board_clauses(board,board_h,board_w))
if s.solve():
model=s.get_model()
show_solution(board,board_h,board_w,model)
if printing:
print("\nSAT - consistent")
print("Model:",model)
print("Legend:\n0-8: mines nearby\n9 : unknown\n10 : known mine\nm : found mine\ns : found safe")
return True
else:
print("\nUNSAT - inconsistent")
return False
#board encoding:
#0-8: mines nearby
#9 : unknown space
#10 : known mine
with open('gameboard.txt', 'r') as fin:
circuit = fin.read()
circuit = circuit.replace(' ', '0')
circuit = [list(line) for line in circuit.split('\n') if len(line) > 0]
board_width = len(circuit[0])
board_height = len(circuit)
mine_count=0 #smaller than width*height
unknown_cells=0 #smaller than width*height
board = [[None for x in range(board_width)] for y in range(board_height)]
for i, (x, y) in enumerate(itertools.product(range(board_width), range(board_height))):
val = int(circuit[y][x], 16)
if val == 11:
val = 10
if val == 10:
mine_count += 1
elif val == 9:
unknown_cells += 1
board[y][x] = val
solve_board(board)
Running this for 1 minute gets the flag.
Flag
CTF{d8675fca837faa20bc0f3a7ad10e9d2682fa0c35c40872938f1d45e5ed97ab27}