Minetest (Hardware) - Google CTF Quals 2019

LiveOverflow -

The Google CTF Qualifier 2019 had a hardware category. And there was one challenge that caught my eye - minetest.

Watch on YouTube
I've stumbled upon this weird minetest map, can you make sense out of it? Minetest + mesecons required
Non-standard flag format (enter bits as 0 and 1)

Mintest is an open source voxel game engine, and Mesecons is a mod which adds advanced digital circuitry like logic gates and programmable blocks. Because this challenge is in the hardware category, it totally makes sense that this is about digital circuitry and logic gates.

Minetest - Open Source Minecraft Clone

First we have to setup the game with the Mesecons plugin. But that is pretty simple with the instructions.

Setup Minetest

When we download the challenge files we can find a folder called real which contains various files like a map.sqlite a world.mt and other stuff. So how can we load this into the game?

First I was looking through the folders of the file to see if something looks similar. But only after I had the idea to create a new world and looked at the logs, I found the place where to put the files. The logs showed me that there is now a folder called worlds, which seems like a good place. The challenge file is probably a world!

Load the challenge into mintest

When I loaded into the map I fell down. But like with Minecraft, I assumed there must be features in creative mode to fly and teleport around. And in the keybindings I was able to find shortcuts for flying, noclip and even faster movement. And from the Minetest wiki I learned about the console and the teleport command.

First Look

To get an overview I kept flying up… and was a bit shocked. oof.

First reaction seeing the challenge map

The circuit is huge. Along the way you can see a few gates. Eventually I reach the end - the final output.

The gates

If you have watched my Pwn Adventure series, then you know already the Blocky’s Revenge challenge. It’s basically the same. We have levers as inputs and at the end we have a single output. We just have to find the correct input that leads to a 1 at the output. So minetest is basically Blocky’s Revenge Revenge.

Pwn Adventure's Blocky's Revenge vs. Mintest

But there is one difference. In Pwn Adventure the circuit was fairly small and could be reversed by hands in a matter of a few hours (as have teams done during the original CTF). However this Minetest challenge is insane. No chance to do this by hand.

But this also makes the challenge straight forward and we basically know exactly what we have to do.

  1. We have to extract the circuit - for example from the world map files.
  2. solve it - for example with a SAT solver like z3.

Parsing the World File

Because this is open source, we should find plenty of resources about parsing the world files. For example I was sure people made map tools and to draw a map you have to somehow parse the world file. Eventually we found the official “Mintest World Format” documentation.

Minetest maps consist of MapBlocks, chunks of 16x16x16 nodes.
[...]
map.sqlite is an sqlite3 database, containing a single table, called "blocks". It looks like this [...]

In the SQLite file we can find binary blobs for each chunk, which should match the MapBlock serialization format. I figured somebody must have already written parsers for this to extract the map, so I spent quite some time looking for various GitHub projects and scripts that deal with this file. And I found various things that have helped me to write my code, but nothing really worked for me right away. The main challenge was that we have non-standard blocks from the Mesecons mod. But eventually I got some first script parsing the data running.

I thought it would be a good idea to visualize the map parsing, in order to verify that it works. So I used Pillow, the python image library, to draw pixels for the blocks I’m parsing. Here it is:

First map parsing test

But at some point I noticed that the map seemed small and that the row of levers were not identifiable at all. This really blocked me for a bit. I made a mistake. The crucial line in the documentation is:

Minetest maps consist of MapBlocks, chunks of 16x16x16 nodes.

A block is a chunk. And a node is an actual block. What I thought I was parsing were single blocks, but in fact I was dealing with 16x16 chunks. So inside a chunk we have 16x16 blocks to deal with. Once I realized that I had to extend my parser and once I figured out how the format exactly works, I was able to draw each individual block… It's huge.

Full Map Render

Extract the Circuit

To solve the circuit, I decided to first store the parsed data in a different format. This has the advantage that I don't have to re-parse the SQLite file every time when I want to test my script. So I created a 2d GRID array and just used single characters to differentiate the blocks. For a regular line I used - or |. For a crossover I used a +. And for gates like AND I used A , XOR X and NOT a N. After I have created this 2D array I saved it to a file grid.py. Then I created a new script trace.py and can simply import the grid.

You can find the script here: https://gist.github.com/LiveOverflow/1480ee7e1ffead942063c638d5b66804#file-minetest-py

Solving the Circuit with z3

And now we come to the actual interesting part. How do we solve this? As mentioned in the beginning, we need some kind of SAT solver that can solve the boolean circuit equation for us. I like to use z3 for that, which I have used in previous videos here and here.

I created the function trace() which takes a coordinate and a direction. This is the coordinate of the final output. And we are tracing to the left (in the way I have oriented the grid the circuit goes to the left).

Tracing backwards from the output

trace() is a recursive function that keeps walking down the circuit until it reaches levers. At each gate it will create the Boolean function whose inputs depend on the two new paths which have to be traced as well.

Recursive trace()

At some point a trace() function will find a lever, which will return a boolean variable. This means the whole recursion can return, the whole circuit "collapses". So at some point trace returns THE WHOLE circuit as a boolean formular.

And now we simply ask z3: "We want this whole trace to be true, we want the output to be true. Please solve this."

That’s it!

Z3 will do it’s solving magic and return exactly the value of the boolean variables that make the output true. Just takes a few seconds. Then we can submit it and get the points.

Submitting the Flag

Esoteric Challenge?

As you can see, pretty straight forward challenge. It’s more of a programming challenge because the path is pretty clear. But it’s really fun and you learn a lot about parsing custom file/data formats. It could be frustrating if you didn't know about z3, but that’s a typical CTF tool that you know about if you read writeups. Even if you just watch my videos you would have know about it.

BUT if you happen to be an electrical engineer, you might even know other tools to solve this. For example q3k solved it using a Verilog netlist. I don’t really know how it works, but Verilog is the language you can use to design hardware and program FPGAs. We have also used it before in the video about the hardware fault injection.

The design tools you use for hardware engineering come with tools to optimize and solve circuits like this. And so q3k transformed the data into a netlist usable by such a tool and let it solve it. Super clever usage of what is a normal tool for hardware development.

This also shows you, that there is real-world practical use of these kind of tools. This is not super esoteric or unrealistic. It is gamified with a Minecraft clone, but this challenge taught you a bit about the hardware world.

References