marx
/
gctf-2023-retro


			
							123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271
							<!DOCTYPE html>
<html lang="en">
    <head>
        <meta charset="utf-8">
        <meta http-equiv="X-UA-Compatible" content="IE=edge">
        <meta name="viewport" content="width=device-width, initial-scale=1.0">
        
        
        <link rel="canonical" href="http://127.0.0.1/mind-the-gap/">
        <link rel="shortcut icon" href="../img/favicon.ico">
        <title>Mind the gap - Google CTF 2023 | Retrospective</title>
        <link href="../css/bootstrap.min.css" rel="stylesheet">
        <link href="../css/font-awesome.min.css" rel="stylesheet">
        <link href="../css/base.css" rel="stylesheet">
        <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/10.5.0/styles/github.min.css">

        <script src="../js/jquery-1.10.2.min.js" defer></script>
        <script src="../js/bootstrap.min.js" defer></script>
        <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/10.5.0/highlight.min.js"></script>
        <script>hljs.initHighlightingOnLoad();</script> 
    </head>

    <body>
        <div class="navbar fixed-top navbar-expand-lg navbar-dark bg-primary">
            <div class="container">
                <a class="navbar-brand" href="..">Google CTF 2023 | Retrospective</a>
                <!-- Expander button -->
                <button type="button" class="navbar-toggler" data-toggle="collapse" data-target="#navbar-collapse">
                    <span class="navbar-toggler-icon"></span>
                </button>

                <!-- Expanded navigation -->
                <div id="navbar-collapse" class="navbar-collapse collapse">
                        <!-- Main navigation -->
                        <ul class="nav navbar-nav">
                            <li class="navitem">
                                <a href=".." class="nav-link">Home</a>
                            </li>
                            <li class="dropdown active">
                                <a href="#" class="nav-link dropdown-toggle" data-toggle="dropdown">misc <b class="caret"></b></a>
                                <ul class="dropdown-menu">
                                    
<li>
    <a href="./" class="dropdown-item active">Mind the gap</a>
</li>
                                </ul>
                            </li>
                            <li class="dropdown">
                                <a href="#" class="nav-link dropdown-toggle" data-toggle="dropdown">pwn <b class="caret"></b></a>
                                <ul class="dropdown-menu">
                                    
<li>
    <a href="../write-flag-where/" class="dropdown-item">Write flag where</a>
</li>
                                </ul>
                            </li>
                        </ul>

                    <ul class="nav navbar-nav ml-auto">
                        <li class="nav-item">
                            <a href="#" class="nav-link" data-toggle="modal" data-target="#mkdocs_search_modal">
                                <i class="fa fa-search"></i> Search
                            </a>
                        </li>
                            <li class="nav-item">
                                <a rel="prev" href=".." class="nav-link">
                                    <i class="fa fa-arrow-left"></i> Previous
                                </a>
                            </li>
                            <li class="nav-item">
                                <a rel="next" href="../write-flag-where/" class="nav-link">
                                    Next <i class="fa fa-arrow-right"></i>
                                </a>
                            </li>
                    </ul>
                </div>
            </div>
        </div>

        <div class="container">
            <div class="row">
                    <div class="col-md-3"><div class="navbar-light navbar-expand-md bs-sidebar hidden-print affix" role="complementary">
    <div class="navbar-header">
        <button type="button" class="navbar-toggler collapsed" data-toggle="collapse" data-target="#toc-collapse" title="Table of Contents">
            <span class="fa fa-angle-down"></span>
        </button>
    </div>

    
    <div id="toc-collapse" class="navbar-collapse collapse card bg-secondary">
        <ul class="nav flex-column">
            
            <li class="nav-item" data-level="1"><a href="#mind-the-gap" class="nav-link">Mind the gap</a>
              <ul class="nav flex-column">
              </ul>
            </li>
        </ul>
    </div>
</div></div>
                    <div class="col-md-9" role="main">

<h1 id="mind-the-gap">Mind the gap</h1>
<p>You are given a script <code>minesweeper.py</code> and text file <code>gameboard.txt</code>. Invoking the python script requires <code>pygame</code> to be installed.</p>
<pre><code>pip install pygame
</code></pre>
<p>It takes several seconds to load. After loading we get a minesweeper game</p>
<p><img alt="minesweeper" src="../images/mine-the-gap.png" /></p>
<p>Inspect the script and search for CTF / FLAG etc.</p>
<p>We see this part of the code</p>
<pre><code class="language-python">    if len(violations) == 0:
        bits = []
        for x in range(GRID_WIDTH):
            bit = 1 if validate_grid[23][x].state in [10, 11] else 0
            bits.append(bit)
        flag = hashlib.sha256(bytes(bits)).hexdigest()
        print(f'Flag: CTF{{{flag}}}')

    else:
        print(violations)
</code></pre>
<p>Basically we need to solve it, and the we will be able to reconstruct the flag from the solution.</p>
<p>Inspect <code>gameboard.txt</code> -- it looks like the board in a simple text format.</p>
<p>The board seems very structured. It looks like putting one mine will collapse a lot of other cells, but not all.</p>
<pre><code class="language-bash">❯ wc gameboard.txt
    1631  198991 5876831 gameboard.txt
</code></pre>
<p>The board is 1600 x 3600 cels. It is huge. It is not possible to solve it by hand.</p>
<p>We need to solve the board with code.</p>
<p>Idea 1 use backtracking, and pray to be fast enough.</p>
<p>Idea 2 skip backtracking and use SAT solver (Z3). This is what we did.</p>
<p>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.</p>
<p>Check the code to generate the solution. With the solution we can easily generate the flag by using the code from the game.</p>
<pre><code class="language-python">import z3

with open('gameboard.txt') as f:
    data = f.read().split('\n')


rows = len(data)
cols = len(data[0])
print(rows, cols, flush=True)

solver = z3.Solver()

vars = {}

def get_var(i, j):
    assert data[i][j] == '9'
    if (i, j) not in vars:
        vars[i, j] = z3.Int(f'var_{i}_{j}')
        solver.add(0 &lt;= vars[i, j])
        solver.add(vars[i, j] &lt;= 1)
    return vars[i, j]


for i in range(rows):
    for j in range(cols):
        if data[i][j] in '12345678':
            flags_on = 0
            pending = []

            for dx in [-1, 0, 1]:
                for dy in [-1, 0, 1]:
                    if dx == 0 and dy == 0:
                        continue

                    nx = i + dx
                    ny = j + dy

                    if 0 &lt;= nx &lt; rows and 0 &lt;= ny &lt; cols:
                        if data[nx][ny] == 'B':
                            flags_on += 1
                        elif data[nx][ny] == '9':
                            pending.append(get_var(nx, ny))

            if not pending:
                continue

            solver.add(z3.Sum(pending) + flags_on == int(data[i][j]))

print(len(vars))

for i in range(rows):
    for j in range(cols):
        if data[i][j] == '9':
            assert (i, j) in vars

print(&quot;Solving...&quot;)
print(solver.check())

for (i, j), v in vars.items():
    if solver.model()[v] == 1:
        print(i, j)
</code></pre></div>
            </div>
        </div>

        <footer class="col-md-12">
            <hr>
            <p>Documentation built with <a href="https://www.mkdocs.org/">MkDocs</a>.</p>
        </footer>
        <script>
            var base_url = "..",
                shortcuts = {"help": 191, "next": 78, "previous": 80, "search": 83};
        </script>
        <script src="../js/base.js" defer></script>
        <script src="../search/main.js" defer></script>

        <div class="modal" id="mkdocs_search_modal" tabindex="-1" role="dialog" aria-labelledby="searchModalLabel" aria-hidden="true">
    <div class="modal-dialog modal-lg">
        <div class="modal-content">
            <div class="modal-header">
                <h4 class="modal-title" id="searchModalLabel">Search</h4>
                <button type="button" class="close" data-dismiss="modal"><span aria-hidden="true">&times;</span><span class="sr-only">Close</span></button>
            </div>
            <div class="modal-body">
                <p>From here you can search these documents. Enter your search terms below.</p>
                <form>
                    <div class="form-group">
                        <input type="search" class="form-control" placeholder="Search..." id="mkdocs-search-query" title="Type search term here">
                    </div>
                </form>
                <div id="mkdocs-search-results" data-no-results-text="No results found"></div>
            </div>
            <div class="modal-footer">
            </div>
        </div>
    </div>
</div><div class="modal" id="mkdocs_keyboard_modal" tabindex="-1" role="dialog" aria-labelledby="keyboardModalLabel" aria-hidden="true">
    <div class="modal-dialog">
        <div class="modal-content">
            <div class="modal-header">
                <h4 class="modal-title" id="keyboardModalLabel">Keyboard Shortcuts</h4>
                <button type="button" class="close" data-dismiss="modal"><span aria-hidden="true">&times;</span><span class="sr-only">Close</span></button>
            </div>
            <div class="modal-body">
              <table class="table">
                <thead>
                  <tr>
                    <th style="width: 20%;">Keys</th>
                    <th>Action</th>
                  </tr>
                </thead>
                <tbody>
                  <tr>
                    <td class="help shortcut"><kbd>?</kbd></td>
                    <td>Open this help</td>
                  </tr>
                  <tr>
                    <td class="next shortcut"><kbd>n</kbd></td>
                    <td>Next page</td>
                  </tr>
                  <tr>
                    <td class="prev shortcut"><kbd>p</kbd></td>
                    <td>Previous page</td>
                  </tr>
                  <tr>
                    <td class="search shortcut"><kbd>s</kbd></td>
                    <td>Search</td>
                  </tr>
                </tbody>
              </table>
            </div>
            <div class="modal-footer">
            </div>
        </div>
    </div>
</div>

    </body>
</html>