CTFtime.org / 2020 Defenit CTF / Minesweeper / Writeup

[original](https://gist.github.com/cwgreene/e4ca5404db149eb76afe0b3d804c738c)
# Defenit 2020: minesweeper

So we're given a 16x16 minesweepr map, and need to beat it in
under a minute. Time to use z3!

Z3 is a Symmetric Modulo Theory (SMT) solver. Essentially, it
is able to solve logic puzzles. Our approach is to parse the map,
and for each number encode that as a constraint.

Parsing the map, we first

```python
def parse_map(grid, bombmap):
rows = bombmap.split("\n")
rows = rows[2::2]
counts = []
empties = []
for i, row in enumerate(rows[:-1]):
row = row[row.index('|'):]
rowcounts = row.split('|')[1:-1]
for j, count in enumerate(rowcounts):
if re.match(" *[0-9]+ *", count):
# Numbers are not mines, direct z3 constraint
BASE_CONSTRAINTS.append(grid[(i,j)]==0)
# Constraints
counts.append((i, j, int(count)))
elif count == " ":
empties.append((i,j))
return counts, empties
```

Here we also state that if you are a number, than you're automatically
not a mine (encoded as '0'). Setting the BASE_CONSTRAINTS here is a bit
of a hack. It would have been better to do it in the construct_constraints,
but I had forgotten to do it the first time round and I just wanted to
ensure that it was done.

The `counts` later get transformed into z3 constraints

```python
def construct_constraint(grid, i, j, count):
neighbor_sum = 0
for neighbor in neighbors(i,j):
ix, jx = neighbor
neighbor_sum += grid[(ix,jx)]
return neighbor_sum == count
```

We then need to find a safe square to choose. We pick one of the
perimeter squares that is adjacent, and we test it. If we mark it
as a mine, and it can't be, z3 will tell us this isn't satisfiable.
This becomes one of our choices. Likewise, if it *must* be mine, we mark it
as such. We track the known flags in a separate array FLAGGED.

```python
def make_choice(grid, counts, empties):
constraints = BASE_CONSTRAINTS[:]
counted = set()
for (i,j,count) in counts:
counted.add((i,j))
constraints.append(construct_constraint(grid, i, j, count))

choices = []
safe = []
for e in empties:
if not set(neighbors(*e)).intersection(counted):
continue
s = z3.Solver()
s.add(*constraints)
s.add(*FLAGGED)
s.add(*safe)
s.add(grid[e] == 1)
check = s.check()
if check == z3.unsat:
choices.append(e)
safe.append(grid[e]==0)

flaggable = []
for e in empties:
if not set(neighbors(*e)).intersection(counted):
continue
s = z3.Solver()
s.add(*constraints)
s.add(*FLAGGED)
s.add(grid[e] == 0)
check = s.check()
if check == z3.unsat:
flaggable.append(e)
FLAGGED.append(grid[e] == 1)
return choices, set(flaggable)
```

Then we just loop until victory.
```python
while True:
print("Parsing...")
counts, empties = parse_map(grid, bombmap)
if not empties:
break
print("Thinking...")
choices, flaggable = make_choice(grid, counts, empties)
print("Thought!")
for bomb in flaggable:
print(convert(*bomb)+"f")
r.sendline(convert(*bomb)+"f")
bombmap = recv_map()
print(bombmap)
for choice in choices:
print(convert(*choice))
r.sendline(convert(*choice))
bombmap = recv_map()
print(bombmap)
if not choices:
print("Done!")
break
```

The first time I did this, I forgot the BASE_CONSTRAINTS. Surprisingly,
the solver was still able to work out safe moves. However, it was much
slower. Putting the BASE_CONSTRAINTS in resulted in much faster solve times.

## Appendix A: Full code

```python
from pwn import *

import re
import z3

r = remote("minesweeper.ctf.defenit.kr", 3333)

BASE_CONSTRAINTS = []
FLAGGED = []

def init_grid():
grid = {}
for i in range(16):
for j in range(16):
grid[(i,j)] = z3.Int("({},{})".format(i,j))
BASE_CONSTRAINTS.append(grid[(i,j)] >= 0)
BASE_CONSTRAINTS.append(grid[(i,j)] <= 1)
return grid

def recv_map():
print(r.recvuntil(' a'))
bombmap = b" a"+ r.recvuntil('-\n\n')
if b'X' in bombmap:
print(str(bombmap, 'ascii'))
print(str(r.recv(), 'ascii'))
return str(bombmap, 'ascii')

def parse_map(grid, bombmap):
rows = bombmap.split("\n")
rows = rows[2::2]
counts = []
empties = []
for i, row in enumerate(rows[:-1]):
row = row[row.index('|'):]
rowcounts = row.split('|')[1:-1]
for j, count in enumerate(rowcounts):
if re.match(" *[0-9]+ *", count):
BASE_CONSTRAINTS.append(grid[(i,j)]==0)
counts.append((i, j, int(count)))
elif count == " ":
empties.append((i,j))
return counts, empties

def convert(row, column):
c = "abcdefghijklmnopqrst"[column]
r = [str(i) for i in range(1,17)][row]
return c+r

def neighbors(i,j):
result = []
for x in [1,0,-1]:
for y in [1,0,-1]:
if x == 0 and y == 0:
continue
if (i + x >= 16) or (i + x < 0) or (j + y >= 16) or (j + y < 0):
continue
result.append((i+x, j+y))
return result

def construct_constraint(grid, i, j, count):
neighbor_sum = 0
for neighbor in neighbors(i,j):
ix, jx = neighbor
neighbor_sum += grid[(ix,jx)]
return neighbor_sum == count

def make_choice(grid, counts, empties):
constraints = BASE_CONSTRAINTS[:]
counted = set()
for (i,j,count) in counts:
counted.add((i,j))
constraints.append(construct_constraint(grid, i, j, count))

def main():
grid = init_grid()

bombmap = recv_map()
# choose 3 random spots to kick off.
r.sendline("a5")
bombmap = recv_map()
r.sendline("n5")
bombmap = recv_map()
r.sendline("j12")
bombmap = recv_map()
print(bombmap)
# main loop
flagged = set()
while True:
print("Parsing...")
counts, empties = parse_map(grid, bombmap)
if not empties:
break
print("Thinking...")
choices, flaggable = make_choice(grid, counts, empties)
print("Thought!")
for bomb in flaggable:
print(convert(*bomb)+"f")
r.sendline(convert(*bomb)+"f")
bombmap = recv_map()
print(bombmap)
for choice in choices:
print(convert(*choice))
r.sendline(convert(*choice))
bombmap = recv_map()
print(bombmap)
if not choices:
print("Done!")
break
#for empty in (set(empties) - flaggable):
# r.sendline(convert(*empty)+"f")
#break
r.interactive()

main()
```

# References
1. https://yurichev.com/blog/minesweeper/

Minesweeper

Comments

Sign in with