Dragon CTF Writeup

I recently took part in DragonCTF, an awesome CTF run by the Dragon Sector CTF team. The CTF was great and pretty hard (for me at least). Throughout the weekend I managed to get two flags, Babykok and Babyshell, and my solutions can be found below. The CTF was pretty hard and and solving these two flags meant we just missed out on being in the top 10% of the tournament. In brief the CTF was great and I can't wait to take part again next year (and actually tackle some of the harder problems)!

Babykok

When you connect, you hit a server that starts demanding you solve first order logic problems. The name and ascii art is a big giveaway that you might need to use COQ, an academic theorem prover; a bit of testing shows that the command line provides you with an interactive shell for COQ that times out pretty quickly.

Having not touched theorem provers for over 10 years I had to catch up pretty quickly. The best document I found for learning COQ was COQ in a Hurry by Yves Bertot. You also do need to know a little about solving theorems to handle this challenge so if you don’t have experience with first order logic you would need to read up on that first. A very brief introduction to first order logic can be found here.

The challenge starts with six theorems that came at random followed by two bonus ones. For some you could google the answer, for others you could use the COQ “tauto” command (which just declares the problem a tautology) to instantly solve.

The final challenge was the hardest, they had taken a classical List Proof (the original can be found here) and altered the lazy list rules, meaning you couldn’t rely on the original proof and had to solve it from scratch. I have to admit I was severely hampered by trying to solve it at 3 am in the morning.

In order to practice solving the challenges (since the CTF timed out quickly) the COQ Proof Solver was incredibly helpful for practicing solving the problems first before scripting the final solution.

The final solution can be found at: https://gist.github.com/dreadn0ught/27e12747033379827623fc64d7687906

Babyshell

When you connect to the challenge you get a connection to a locked down QEMU alpine linux environment running busybox. You can also download the image to test locally as well.

When I analysed the busybox binary the first thing I noticed was that it had been modified. This however, was a bit of a red herring. All the modification did was remove the “[6m” from the prompt. This, I believe, was actually done to make the challenge easier as it means you can use the terminal for sending raw bytes without having additional bytes accidentally injected by the busybox binary.

Additionally, I noticed that if you reviewed the list of commands busybox accepted, there were a number of commands available within busyox that weren’t accessible within the environment PATH by default. This included commands like netcat which turned out to be useful later.

A variation of nmap was also available on the box. When running it, it revealed that there was also a server running on port 4433. If you netcat to it and send garbled data, the server will response with openssl errors. This implied it was running an SSL server of some sort.

To attempt to connect to the SSL server I wrote a python script that would accept connections locally on my machine and tunnel the TCP connection into a netcat connection on the alpine linux VM. The only problem with this approach was that the SSL version (0x3) is the third byte sent within the console; this is also the equivalent of sending CTRL+C to the terminal and instantly cancels the netcat connection within the VM.

Traditionally, to deal with this, you would use pipes to send the data to a local file and then pipe it into the netcat connection. However, the file system was read only meaning pipes couldn’t be used. The Base64 command was available, which meant we could avoid the CTRL+C problem, but it would only let us send one command at a time. To solve this problem, we needed to perform a full SSL handshake to get a steady connection.

Going back to see what binaries were available on the VM, I noticed we also had microcom available. Microcom is traditionally used for creating serial connections to devices that access raw bytes as commands. This is often used for console connections, especially for embedded/networking devices. We could connect microcom to the netcat connection to pipe our data first into microcom (which did accept 0x3 as a valid input) and then into the netcat binary and onto the SSL server. You did also have to include the -X flag with microcom (this made sure 0x00 bytes weren’t filtered out).

Once this connection was set up, we then needed to make sure our python script providing the local tunnelling worked. In this situation, never try to create your own tunnelling library (believe me I’ve tried!). PwnLib provides an excellent solution by simply creating two remote sessions and connecting the input and output streams together.

The python script used can be found at: https://gist.github.com/dreadn0ught/92f9a8c01183c228338312bb5bc90f03

Once you have done this you will see that curl-ing the connection or using a browser to try to connect to the SSL server doesn’t work. Curling just gets an error, while using a browser gives you all sort of certificate issues. Instead, the best option is to just use the openssl client: openssl s_client -connect 127.0.0.1:<tunnel port>. The openssl client lets you perform telnet like operations on the underlying SSL server. Once connected, if you send any data down the connection you receive the flag.