|
|
@@ -1,16 +1,16 @@
|
|
|
-# Mind the gap
|
|
|
+# Mine the gap
|
|
|
|
|
|
-You are given a script `minesweeper.py` and text file `gameboard.txt`. Invoking the python script requires `pygame` to be installed.
|
|
|
+You are given a script `minesweeper.py`, and a text file, `gameboard.txt`. Invoking the python script requires `pygame` to be installed.
|
|
|
|
|
|
pip install pygame
|
|
|
|
|
|
-It takes several seconds to load. After loading we get a minesweeper game
|
|
|
+It takes several seconds to load. After loading, we get a minesweeper game
|
|
|
|
|
|
|
|
|
|
|
|
Inspect the script and search for CTF / FLAG etc.
|
|
|
|
|
|
-We see this part of the code
|
|
|
+We see this part of the code:
|
|
|
|
|
|
```python
|
|
|
if len(violations) == 0:
|
|
|
@@ -25,28 +25,28 @@ We see this part of the code
|
|
|
print(violations)
|
|
|
```
|
|
|
|
|
|
-Basically we need to solve it, and the we will be able to reconstruct the flag from the solution.
|
|
|
+We need to solve it, and then we can reconstruct the flag from the solution.
|
|
|
|
|
|
-Inspect `gameboard.txt` -- it looks like the board in a simple text format.
|
|
|
+Inspect `gameboard.txt` -- it looks like the board is in a simple text format.
|
|
|
|
|
|
-The board seems very structured. It looks like putting one mine will collapse a lot of other cells, but not all.
|
|
|
+The board looks pretty structured. Putting one mine will collapse many other cells, but not all.
|
|
|
|
|
|
```bash
|
|
|
❯ wc gameboard.txt
|
|
|
1631 198991 5876831 gameboard.txt
|
|
|
```
|
|
|
|
|
|
-The board is 1600 x 3600 cels. It is huge. It is not possible to solve it by hand.
|
|
|
+The board is 1600 x 3600 cells. It is huge. It is not possible to solve it by hand.
|
|
|
|
|
|
We need to solve the board with code.
|
|
|
|
|
|
-Idea 1 use backtracking, and pray to be fast enough.
|
|
|
+Idea 1 use backtracking and pray to be fast enough.
|
|
|
|
|
|
Idea 2 skip backtracking and use SAT solver (Z3). This is what we did.
|
|
|
|
|
|
-With Z3 we can create variables and create constraints on the values they can get, then ask for a solution. If there is a solution, Z3 will give us the values for the variables. Z3 will find a solution in a reasonable™️ time.
|
|
|
+With Z3, we can create variables and constraints on the values they can get, then ask for a solution. If there is a solution, Z3 will give us the values for the variables. Z3 will find an answer in a reasonable™️ time.
|
|
|
|
|
|
-Check the code to generate the solution. With the solution we can easily generate the flag by using the code from the game.
|
|
|
+Check the code to generate the solution. With the answer, we can easily recover the flag using the game's code.
|
|
|
|
|
|
```python
|
|
|
import z3
|
