## Back to the Future, pwn 400 (valis)

While you can find all our write-ups from PlaidCTF 2020 in the previous post, we decided this one deserves it's own spotlight.

Ladies and gentlemen, I present to you valis's write-up for the Back to the Future task from PlaidCTF 2020.

I'm actually old enough to have used Netscape (with modem) back in the day, so this challenge was right up my alley.
The first step was to try to find sources on the Internet. It wasn't easy, but eventually I've found this github repo:
https://github.com/vicamo/b2g_mozilla-central

Those sources were for version 4.x, and our target was 0.96 Beta. 4.x is a huge application with html editor, mail client, JavaScript support, etc., while 0.96 barely supports basic HTML with images, so it was far from ideal, but it was still helpful, especially some core libraries were pretty similar on both versions.

Next step was try start reversing and I've soon encountered another issue:
./back_to_the_future: Linux/i386 demand-paged executable (ZMAGIC), stripped

The binary was in an ancient a.out format (zmagic variant).
I've spent some time trying to get it to run in my environment, but eventually gave up - even after adding a.out support to the kernel the binary was segfaulting at the very beginning.
I've decided to do everything at the remote server, giving up the luxury of having a debugger.

Then it was time to reverse the binary and find some vulnerabilities.
I was able to identify some libc functions by comparing strings in the binary with those in sources.
My focus was on risky string functions like strcpy, strcat or scanf (especially with %s).
Finally I've found an sscanf call that looked vulnerable - it was used to parse a date string into components (year, month, etc) with the following format string: "%d %s %d %d:%d:%d".
The ‘%s’ part (month) was stored in a static stack buffer and there was no length checking at all.
Now I had to find all references to this function and figure out how to trigger it.
Luckily, I was able to find this code in the sources - the function was called NET_ParseDate() and belonged to the core libnet library.

The code was pretty similar, but 1998 version had a length check that was missing in our binary:

if(255 < XP_STRLEN(ip))
return(0);

With the help of the sources it was trivial to find how to trigger this code - NET_ParseDate() was used to parse several HTTP headers. I've used Expires in my exploit.

It was time to confirm my suspicions - I wrote a python script to act as a simple HTTP server that will send 300 "A" letters in the Expires header and submitted the URL to the "time machine".

It worked! Connection closed immediately, clearly a different behaviour compared to a response with a standard short header.

The hard part seemed to be over, but there were still some issues:

1. Since I wasn't able to run the binary locally, I had no idea how the memory was mapped and what protections were in place. Is there any ASLR?
Is it all RWX?
2. sscanf stops reading at whitespace, which means I had to avoid several "bad" characters in my payload (most importantly, no null bytes).

Disassembler showed that the code segment starts at a virtual address of 0, but is it true? I've searched the binary for EBFE sequence (jmp .) and used its address to overwrite EIP.
It hung for 10 seconds instead of closing the connection immediately - great, we now have code execution!

But how to get shell? There is no way to interact with stdin, so executing /bin/sh is not enough, we need to be able to run arbitrary commands.
The main issue was lack of any attacker-controlled data at a known address - we don't know where the stack is in memory.

However, looking at libc relative calls it seems that libc is mapped at 0x60000000. I've tested this theory with the help of another EBFE sequence, this time from libc. Another hang - libc found!

Now we can try to do a ROP with libc calls - but only those that passed the "bad character" test.

One easy way to go would be to call read(), to get the next stage from the open socket and place it at a known location - then we could pivot our stack there, or just use it for execve() arguments.

Unfortunately, our socket is at fd 4, which means 3 null bytes that will break our ROP.

One function that was safe to call was strcpy() (provided that both dst and src addresses had no "bad bytes").

I've decided to use strcpy() as a primitive to write arbitrary content by copying sequences of bytes from libc to our destination.

For example, to write "/bin/sleep\x00" to a destination 0x01020304 we need to execute following calls:

strcpy(0x01020304, "/bin/")
strcpy(0x01020304+5, "sl") // There was no "sleep" string in libc
strcpy(0x01020304+7, "ee")
strcpy(0x01020304+9, "p")

In the worst case scenario we need one call per byte, but often we are lucky enough to find longer sequences.
I wrote an encoder to automate this process. Fixing bugs without any debugging feedback except for "hang or crash" was hard, but finally it worked.

My first attempt was to call system() from libc, but it didn't work for some reason (no debugger, so we'll never know).
Then I tried to write to the code segment and it turned out that this memory is mapped RWX, so I just placed my shellcode at a known location and jumped there at the end of the ROP.

Standard shellcraft.i386.linux.dupsh(4) shellcode was enough to get me shell:

[+] Waiting for connections on 0.0.0.0:80: Got connection from 45.63.35.176 on port 34766
[*] GET / HTTP/1.0
User-Agent: Mozilla/0.96 Beta (X11; Linux 5.3.0-46-generic x86_64)
Accept: */*
Accept: image/gif
Accept: image/x-xbitmap
Accept: image/jpeg

[*] Switching to interactive mode
sh: turning off NDELAY mode
$/readflag PCTF{ELFs?__wH3Re_wER3_G01ng___We_d0Nt_n3ed_ELFs__344bc53072811af0} Exploit: https://gist.github.com/valisctf/3f8a73bc1da3a9cd7ccdeb224d385978 ### PlaidCTF 2020 write-ups PlaidCTF is known to be a quality CTF tournament, with the 2020 edition being no different - lots of amazing tasks, lost of teams playing, and fierce competition till the end. And since there were a lot of cool, fun and challenging tasks, and since we solved a lot of them, we were forced to decided completely on our own to write down solutions and share them with you :) Without further ado, the write-ups: Enjoy! ## Monday, November 18, 2019 ### Dragon CTF 2019 - Results and Tasks Explained As last year, Dragon CTF 2019 took place on the Security PWNing Conference. The battle was fierce - as expected when several top teams in the world meet in one place. However, in the end there can be only one. Without further ado, we would like to congratulate the winners of Dragon CTF 2019, the runner-up team and the 3rd place: 1. p4 (198.000 pts to the global ranking and 30000 PLN) 2. PPP (121.423 pts to the global ranking and 15000 PLN) 3. ALLES! (101.538 pts to the global ranking and 8000 PLN) You can find the full scoreboard on CTFtime: https://ctftime.org/event/887. As every year, after the CTF we held a quick talk showcasing the intended solutions. You can find the slides here: https://docs.google.com/presentation/d/12TzHVUc36eOZIZxLtr13YEmHxQS5lBXrWX5jbwMZjC8/edit. That's it for this year - see you on other battlefields and on the Dragon CTF 2020! ## Tuesday, October 8, 2019 ### Dragon CTF 2019 will feature Arcane Sector 2 (if your team is not planning to attend the Dragon CTF 2019 at the Security PWNing Conference - 14-15 Nov 2019 - in Warsaw, Poland, you can safely skip this post) Dear teams and individual players planing to participate in the Dragon CTF 2019, Please be advised that this CTF, as last year, will feature a custom-made multiplayer RPG game called "Arcane Sector". While we don't plan to publish the version we'll use at the CTF ahead of time, we wanted to let you know that it will be based on an upgraded version of last year's code base (so, for all intents and purposes, it will be "Arcane Sector 2"). If you haven't participated in Dragon CTF 2018, please note that you can find the said code base, as well as videos about how it works, here: Consider yourselves warned. ## Wednesday, February 13, 2019 ### CVE-2019-5736: Escape from Docker and Kubernetes containers to root on host ## Introduction The inspiration to the following research was a CTF task called namespaces by _tsuro from the 35C3 CTF. While solving this challenge we found out that creating namespace-based sandboxes which can then be joined by external processes is a pretty challenging task from a security standpoint. On our way back home from the CTF we found out that Docker, with its “docker exec” functionality (which is actually implemented by runc from opencontainers) follows a similar model and decided to challenge this implementation. ## Goal and results Our goal was to compromise the host environment from inside a Docker container running in the default or hardened configuration (e.g. limited capabilities and syscall availability). We considered the two following attack vectors: • a malicious Docker image, • a malicious process inside a container (e.g. a compromised Dockerized service running as root). Results: we have achieved full code execution on the host, with all capabilities (i.e. on the administrative ‘root’ access level), triggered by either: • running “docker exec” from the host, on a compromised Docker container, • starting a malicious Docker image. This vulnerability was assigned CVE-2019-5736 and was officially announced here. ## Default Docker security settings Despite Docker not being marketed as sandboxing software, its default setup is meant to secure host resources from being accessed by processes inside of a container. Although the initial process inside a Docker container is running as root, it has very limited privileges, which is achieved using several mechanisms (this paper describes it thoroughly): ### Linux capabilities Docker containers have a very limited set of capabilities by default, which makes a container root user de facto an unprivileged user. ### seccomp This mechanism blocks container’s processes from executing a subset of syscalls or filters their arguments (thus limiting its impact on the host environment.) ### namespaces This mechanism allows to limit containerized processes’ access to the host filesystem, as well as it limits the visibility of processes across the host/container boundary. ### cgroups The control groups (cgroups) mechanism allows to limit and manage various types of resources (RAM, CPU, ...) of a group of processes. It’s possible to disable all of these mechanisms (for example by using the --privileged command-line option) or to specify any set of syscalls/capabilities/shared namespaces explicitly. Disabling those hardening mechanisms makes it possible to easily escape the container. Instead, we will be looking at Docker containers running the default security configuration. ## Failed approaches Before we ended up finding the final vulnerability we had tried many other ideas, most of which were mitigated by limited capabilities or by seccomp filters. As the whole research was a follow-up to a 35C3 CTF task, we started by investigating what happens when a new process gets started in an existing namespace (a.k.a. “docker exec”). The goal here was to check if we can access some host resources by obtaining them from the newly joined process. Specifically, we looked for ways to access that process from inside the container before it joins all used namespaces. Imagine the following scenario, where a process: • joins the user and PID namespaces, • forks (to actually join the PID namespace), • joins the rest of the namespaces (mount, net etc.). If we could ptrace that process as soon as it visible to us (i.e. right as it joined the PID namespace), we could prevent it from joining the rest of the namespaces, which would in turn enable e.g. host filesystem access. Not having the required capabilities to ptrace could be bypassed by performing an unshare of the user namespace by the container init process (this yields the full set of capabilities in the new user namespace). Then “docker exec” would join our new namespace (obtained via “/proc/pid/ns/”) inside of which we can ptrace (but seccomp limitations would still apply). It turns out that runc joins all of the required namespaces and only forks after having done so, which prevents this attack vector. Additionally, the default Docker configuration also disables all namespace related syscalls within the container (setns, unshare etc.). Next we focused solely on the proc filesystem (more info: proc(5)) as it’s quite special and can often cross namespace boundaries. The most interesting entries are: • /proc/pid/mem - This doesn’t give us much by itself, as the target process needs to already be in the same PID namespace as malicious one. The same applies to ptrace(2). • /proc/pid/cwd, /proc/pid/root - Before a process fully joins a container (after it joins namespaces but before it updates its root (chroot) and cwd (chdir)) these point to the host filesystem, which could possibly allow us to access it - but since the runc process is not dumpable (read more: http://man7.org/linux/man-pages/man2/ptrace.2.html), we cannot use those. • /proc/pid/exe - Not of any use just by itself (same reason as cwd and root), but we have found a way around that and used it in the final exploit (described below). • /proc/pid/fd/ - Some file descriptors may be leaked from ancestor namespaces (especially the mount namespace) or we could disturb parent - child (actually grandchild) communication in runc - we have found nothing of particular interest here as synchronisation was done with local sockets (can’t reuse those). • /proc/pid/map_files/ - A very interesting vector - before runc executes the target binary (but after the process is visible to us, i.e. it joined the PID namespace) all the entries refer to binaries from the host filesystem (since that is there where the process was originally spawned). Unfortunately, we discovered that we cannot follow these links without the SYS_ADMIN capability (source) - even from within the same process. Side note: When executing the following command: /lib/x86_64-linux-gnu/ld-linux-x86-64.so.2 /bin/ls -al /proc/self/exe “/proc/self/exe” points to “ld-linux-x86-64.so.2” (not “/bin/ls”, as one might think) The attack idea was to force “docker exec” to use dynamic loader from host to execute binary inside container (by replacing original target to exec (e.g. “/bin/bash”) with a text file with the first line: #!/proc/self/map_files/address-in-memory-of-ld.so) /evil_binary Then /evil_binary could overwrite /proc/self/exe and thus overwrite the host ld.so. This approach was unsuccessful due to the aforementioned SYS_ADMIN capability requirement. Side note 2: While experimenting with the above we found a deadlock in the kernel: when a regular process tries to execve “/proc/self/map_files/any-existing-entry”, it will deadlock (and then opening “/proc/that-process-pid/maps” from any other process will also hang - probably some lock taken). ## Successful approach The final successful attempts involved an approach very similar to the aforementioned idea with /proc/self/map_files - we execute /proc/self/exe, which is the host's docker-runc binary, while still being able to inject some code (we did that by changing some shared library, like libc.so, to also execute our code e.g. inside libc_start_main or global constructor). This gives us ability to overwrite /proc/self/exe binary which is the docker-runc binary from the host, which in turn gives us full capabilities root access on host next time docker-runc is executed. ### Detailed attack description: Craft a rogue image or compromise a running container: 1. Make the entrypoint binary (or any binary that is likely to be runtime overridden by the user as the entrypoint, or as part of docker exec) be a symlink to /proc/self/exe 2. Replace any dynamic library used by docker-runc with a custom .so that has an additional global constructor. This function opens /proc/self/exe (which points to the host docker-run) for reading (it is impossible to open it for writing, since the binary is being executed right now, see ETXTBSY in open(2)). Then this function executes another binary which opens, this time for write, /proc/self/fd/3 (a file descriptor of docker-runc opened before execve), which succeeds because docker-runc is no longer being executed. The code can then overwrite the host docker-runc with anything - we have chosen a fake docker-runc with an additional global constructor that runs arbitrary code. Thus, when a host user runs the compromised image or “docker exec” on a compromised container : 1. The entrypoint/exec binary that has been symlinked to /proc/self/exe (which in turn points to docker-runc on the host filesystem) begins executing within the container (this will also cause process to be dumpable, as execve sets the dumpable flag). To be clear: this causes the original docker-runc process to re-execute into a new docker-runc running within the container (but using the host binary). 2. When docker-runc begins executing for the second time, it will load .so files from the container, not the host (because this is the visible filesystem now). As a reminder: we control the content of these dynamic libraries. 3. The malicious global constructor function will be executed. It will open /proc/self/exe for reading (let’s say it will have file descriptor 3) and execve()s some attacker controlled binary (let’s say /evil). 4. /evil will overwrite docker-runc on the host filesystem (by reopening fd 3, this time with write access) with a backdoored/malicious docker-runc (e.g. with an additional global constructor). 5. Now when any container is started or another exec is done, the attacker’s fake docker-runc will be executed as root with full capabilities on host filesystem (this binary is responsible for dropping privileges and entering namespaces, so initially it has full permissions). Note that this attack only abuses runc (opencontainers) behavior, so it should work for kubernetes as well, regardless of whether it uses docker or cri-o (both may use runc internally). This attack has serious impact on AWS and GCP cloud services. More information about it can be found at linked security bulletins. ## Responsible disclosure We have reported the vulnerability to security@docker.com the same day we discovered it, including a detailed attack description and a proof of concept exploit. The next day the Docker security team forwarded our email to security@opencontainers.org. We also actively participated in discussions regarding fixing the vulnerability. Communicating with the Docker and OpenContainers security teams was frictionless and pleasant.. ## Rejected fix ideas in runc ### Open the destination binary and compare inode info from fstat(2) with /proc/self/exe and exit if they match, otherwise execveat on destination binary fd. This would detect if destination binary is a symlink to /proc/self/exe. Why execveat? Because we want to avoid the race condition where between comparison at exec some other process will replace destination binary with link to /proc/self/exe. Why wouldn’t this work? This can be bypassed when attacker will not use symlink, but a binary with dynamic loader pointing to “/proc/self/exe”: e.g. text file which has “#!/proc/self/exe” as first line or just an elf file. ### Use a static binary to launch processes within the container The idea of this is to avoid code execution possibility via malicious .so files inside the container (a static binary means no .so files are loaded). Why wouldn’t this work? Replacing .so files was not actually needed for this exploit. After the re-exec of /proc/self/exe (docker-runc), another process can just open /proc/<pid-of-docker-runc>/exe, which is possible because ”dumpable” flag is set on execve. This is a little bit harder to exploit because it requires to race the timing between the re-exec completing and runc process exiting (due to no parameters given). In practice, the race window is so large that we were able to develop a 100% successful exploit for such a scenario. However this would eliminate one of the attack vectors: running a rogue image. ## Final fix applied in runc In the end, the following fix was applied to mitigate the vulnerability: : 1. Create a memfd (a special file which exists only in memory). 2. Copy the original runc binary to this fd. 3. Before entering namespaces re-exec runc from this fd. This fix guarantees that if the attacker overwrites the binary pointed to by /proc/self/exe then it will not cause any damage to the host because it’s a copy of the host binary, stored entirely in memory (tmpfs). ## Mitigations There are several mitigation possibilities when using an unpatched runc: 1. Use Docker containers with SELinux enabled (--selinux-enabled). This prevents processes inside the container from overwriting the host docker-runc binary. 2. Use read-only file system on the host, at least for storing the docker-runc binary. 3. Use a low privileged user inside the container or a new user namespace with uid 0 mapped to that user (then that user should not have write access to runc binary on the host). ## Timeline 1. 1 January 2019 - Vulnerability discovered and PoC created 2. 1 January - Vulnerability reported to security@docker.com 3. 2 January - Report forwarded by docker security team to security@opencontainers.org 4. 3 - 5 January - Discussion about fix ideas 5. 11 February - end of CVE-2019-5736 embargo 6. 13 February - this post publication ## Tuesday, January 1, 2019 ### Dragon Sector wins CTFtime season 2018! CTFtime's 2018 season is now over and for the second time in our team's history we've managed to get the top place! (If you've arrived on this page without context, you might want to check out these two explanations on what a CTF competition is - Wikipedia, CTFtime. But in short: it's an IT security/hacking tournament, with close to a hundred events being played out throughout the year. CTFtime is the main global team ranking and CTF aggregate site.) As you can imagine, we are really happy with this achievement. It has been an extremely busy year for all of our players, our guest players and doubly so for our captain valis and vice-captain Redford, who behind the scenes orchestrated the success.  Insomni'hack CTF 2018 (Copyright SCRT SA) We started the season strongly with winning the Insomni'hack teaser CTF for the fifth (sic!) time in a row. The main Insomni'hack CTF in Geneva, Switzerland - the biggest on-site-only CTF in this part of the world - was less fortunate for us and eventually we were bested by the German powerhouse - the Eat, Sleep, Pwn, Repeat team (top3 in 2017 CTFtime season), with our friends from p4 finishing third. A week later, at the end of March, we qualified from the second place to the 0CTF/TCTF 2018 CTF which was to happen in May in China. And May was a good month for our team. It started with two legendary CTFs - the PlaidCTF organized by one of the world's best teams - the Plaid Parliament of Pwning from Carnegie Mellon University (the only team that was always on the CTFtime season podium in the last 8 years, winning the season 3 times!), and the DEF CON CTF Qualifiers known both for the immense difficulty level and heavy participation from top tier teams - it's basically a battlefield with only a handful of teams qualifying to the offline finals in Las Vegas, US. While we were pretty far from the top places - top6 on PlaidCTF and top10 on DEF CON CTF Quals - we still managed to add a decent amount of points to the global ranking, as well as qualify to the DEF CON CTF finals.  0CTF/TCTF 2018 - note DS emblem on the top right (Photo by Redford) Near the end of May our team went to Szenzhen, China to compete in the 0CTF/TCTF 2018 finals alongside amazing teams like South Korean CyKOR, Russian LC↯BC or Japanese TokyoWesterns to name just a few. Eventually we managed to secure the top place and a hefty amount of points for the global ranking. To complete a good streak, we've also won the online Security Fest CTF at the end of the month. The summer is usually pretty slow on CTFs. We've qualified to Google CTF in June from the second place (finals were in October), as well as the CODE BLUE CTF from the first place. DEF CON CTF finals in Las Vegas went OKish at best with Dragon Sector finishing at 9th place. In the meantime we also traveled to Beijing, China and had (again) the honor of playing the invite-only WCTF 2018, which we eventually finished on the second place!  WCTF 2018 (Copyright 360 Vulcan Team) (DS members from the left: adami, mwk, Redford, q3k, implr) September brought us 3rd place in the online TokyoWesterns 4th CTF, with Plaid Parliament of Pwning winning and Taiwanese 217 (top1 in CTFtime season 2017) as runner-up. Given the high rank of the CTF we still were happy with the results as it increased our overall global score.  Teaser Dragon CTF 2018's website Our own Teaser Dragon CTF 2018 also took place in September and we've received excellent notes from the CTF community. The main Dragon CTF 2018 was to happen in November during the Security PWNing Conference in Warsaw, Poland. (A short note on how the global CTFtime scoring system works: Each tournament has a rating weight from 0 to 100 - the more the better - with both the CTF winning team and CTF organizing team getting double the rating weight in points, and teams on further places getting less and less points (see the formula if you're interested in details). However, the total global score for a team is calculated only from the team's top ten scores in the given year, and this includes the CTF organized by the team. So in case of top teams at some point during the year even winning a lower-tier CTF doesn't necessarily benefit the total score. We started paying more attention to this around late summer limiting our participation and conserving strength for the year's end.) One more CTF to note for September was the small local (and eventually unranked) Security Case Study CTF in Warsaw, Poland, which featured teams limited to 3 people. As such, both p4 and Dragon Sector entered multiple teams to play the CTF (each team competing separately). In the end while DS won the CTF, p4 took both the runner-up and third places (blast, foiled again!).  Security Case Study CTF 2018 (Copyright CyberSecurity Foundation) (DS members from the left: valis, Redford, Gynvael) The last quarter of the year is always pretty hectic - multiple tournaments are scheduled for that part of the year, so it means a lot of traveling and playing for the team. If you add to it the fact that we were in the midst of preparing the Dragon CTF... Yes. Hectic is the right word. We started with getting 2nd place on the online Hack.lu CTF organized by FluxFingers, and then proceeded to win the ultra-high-weight HITCON CTF 2018 (with Plaid Parliament of Pwning as runner-up and BFKinesiS on close third) - this netted us close to 200 points for the global ranking!  Google CTF 2018 Finals venue (Photo by Gynvael) In late October we traveled to London, UK for the Google CTF 2018 Finals, but finished there on 5th place. Early November meant going to Moscow, Russia for the CTFZONE 2018 Finals, however we also fell short there and eventually landed on 6th place with two top-tier teams from Russia taking the top places (Bushwhackers and LC↯BC) and p4 closing the podium. November was also the month when the main Dragon CTF 2018 took place. A lot of preparations happened weeks before the CTF, yet we somehow always end up polishing the details up until the last minute and not really getting too much sleep beforehand (it is then that we've realized that valis is a vampire and doesn't need any rest, and that Gynvael looks like a literal zombie unless he gets his beauty sleep).  Dragon CTF 2018 (Photo by Gynvael) Still, we managed and we were happy with the results (and so were the players)! And we proudly joined the small-yet-growing group of CTFs with custom game hacking challenges (a trend started by the famed Ghost in the Shellcode CTF, and continued by e.g. the aforementioned Insomni'hack CTF).  Arcane Sector Online from Dragon CTF 2018 In December we played only two CTFs: the hxp CTF 2018 and the annual "season finals" in the form of the renowned Chaos Communication Congress (or 35C3 for short) CTF in Leipzig, Germany. The latter was especially important for us, as it's one of the very few CTFs with the ultimate 100 rating weight. Also it was organized by Eat, Sleep, Pwn, Repeat - this basically certifies quality. In the end we've finished 3rd on both CTFs, with pasten one-upping us as every year. The KJC+MHackeroni team from Italy won btw - they are extremely good, but similarly to pasten, play only a few CTFs during the year. And this was enough to keep the first place in the global CTFtime ranking, with Plaid Parliament of Pwning being really close on the second place, and our friends from another Polish team - p4 - taking the 3rd place (it's worth mentioning that multiple other teams were really close to the 3rd place, e.g. TokyoWesterns, 217, 0daysober - organizers of Insomni'hack or dcua - the Ukrainian powerhouse). So GG, WP. For us it's time to rest... ...until January 19th that is, since we have to win Insomni'hack teaser 2019 CTF for the 6th time in a row :) Dragon Sector, Dec 31, 2018 ## Sunday, August 5, 2018 ### CODE BLUE CTF 2018 Quals - watch_cats (solved by q3k)  watch_cats #### 1 - Introduction This was a challenge for the CODE BLUE CTF Quals in 2018. The data given was a binary that would display the above, its source code (220 lines of C++) and 5 text files that looked like stage data. The binary would present a WATCH_DOGS-style minigame style challenges to the user, who would solve them by rotating 'joints' until they guided a signal from a source to a goal (in later stages, multiple goals at once). After solving five stages, the program would display a flag read from a file and exit. The same binary was also running remotely on the organizers' infrastructure, where it contained the same stage data and the actual competition flag. The first two stages (pictured above) are solvable by hand. The first one requires you to just rotate one joint into place, the second requires quite a few more rotations, but is still very easy to solve in the 9 iterations that the binary allows you to perform.  A single joint rotating. When you get to the third stage, however, the binary stops showing you visualizations. It's time to dig deeper.  No image? oh no Thankfully, the source code for the challenge was provided. Reading it, we can deduce that: • The stages are read file-by-file from the local directory. • Each stage is a plain text file composed of the following records: • answer, the number of steps a player can take to solve the stage • num_cables, the number of cables that are between nodes • num_joints, the number of joints that are connected by cables • num_joints x (joint_type, 4x neighbor_cable), where joint_type is one of 8 possible types of joints (each with different connectivity geometry), and neighbor_cables are cable numbers [0..num_cables) into which the joint connects • num_goals, the number of goals that the signal must reach • num_goals x goal_number, a cable number that defines a goal cable • H and W, the height and width (in unicode glyphs) of the stage graphic • H x W of belong data, which defines whether a graphic: • belongs to a cable and should be colored blue when a signal reaches that cable (belong > 0, cable number == belong), and displayed with font[i, j] • belongs to a joint and should be colored blue when a signal rached that joint (belong < 0 joint number == -belong), and should be displayed with the joint type graphic • belongs to neither (belong == 0) and should just be displayed with font[i, j] Quickly auditing the code from a security point of view, I found no obvious bugs triggerable by user interaction (we're basically limited to rotating selected joints). However, it was obvious that if you solved all five stages, you would just get the flag printed to screen. Let's try that? First, let's just write some simple Python to read a stage data into memory and allow us to further process it.  Basic Python to re-implement stage parsing and basic analysis of joints/cables. I also added some networkx based code to create a graph of joints/cables (where each joint, cable, source and goal is a node). This let us quickly visualize the stages, and verify that the Stage 2 visualization corresponds to the level visualization:  Stage 2, as drawn by networkx/graphviz. And if you look closely, it does. Now, let's draw the same style of graphs for the stages we haven't solved yet: Stages 3, 4 and 5.  Stage 3.  Stage 4.  Stage 5 - nope.jpg. By the point I looked at Stage 5, it was clear that the problem was ridiculous enough that I definitely wasn't going to solve it manually - at least not without smarter printing of the graphs so I could see joints and how their rotation changes the signal flow. Let's automate this. #### 2 - Solving the puzzles automatically How do we solve a puzzle like this? It might simply be the case that I'm in the proximity of a mind-altering hammer that makes me hallucinate everything to be a nail... but I chose converting the puzzles to Verilog and using formal methods to find solutions. No, wait! Don't close this tab yet. Hear me out. The theory is simple: let's convert every junction to be a clocked flip-flop that will take on a given cable value as it's new value if a 'joint rotation' register is in the correct position. In other words, the 'signal' propagating in the puzzle will be modeled as a 1 value propagating across joints on positive clock pulses.  Turning a stage into a Verilog module. This will then generate a Verilog module for every stage, looking like this:  Stage 2, as a Verilog module. Now in this current state, this is a decent way of representing a game puzzle in a somewhat esoteric manner. We can run this through a Verilog simulator to replicate the behaviour of the puzzle, but that's somewhat useless. Here's where formal methods come into play. We'll be using 'yosys-smtbmc', which is a flow that involves running the Yosys synthesizer with an SMT2 backend, and then feeding those SMT2 circuit descriptions into SMT2 solvers. These circuit 'models' can be used for different modes of operation of the solver: • BMC - bounded model check. Start from the initial Verilog module state and see if you can get it to trigger an assertion within a given amount of steps. • K-induction. Start from an invalid state, and work backwards to see if that state can be reached from any valid state. • Coverage. Start from the initial Verilog module state and try to reach a valid cover statement. If you want to read more about this, Dan Gisselquist has an excellent series of blogposts about starting with Formal Methods with yosys-smtbmc. We'll be running in Coverage mode, with a cover(goal[0] == 1 && ...) statement. This means that yosys-smtbmc will find how to drive the undriven rotation registers in order to get the source signal to 'reach' all the goals. First order of business is to use assume statements to let the solver know what sort of behaviour is valid. We'll first create a f_past_valid signal that will be 1 from the second cycle of the simulation. This is so that we can use any 'time-travelling' statements like$past(signal), \$stable(signal), ... in our other formal statements. We also add our cover statement for reaching the goals. Finally, we also add an assumption that we need to find a state where the amount of total rotations is less or equal to the amount of steps we can take in a stage.
 Emitting formal assume and cover statements in Verilog module for a stage.
Another thing we want to assume (declare what is a valid state) is that rotation registers are stable across the execution of the proof:
 Emitting formal assume statement to make joint rotation stable across proof.
Now, we're ready to see what the solver can find for us! We re-emit the Verilog module (with formal statements) to s2.v for Stage 2, and write a quick Symbiyosys definition of what we're trying to prove:
 yosys-smtbmc solves Stage 2 of watch_cats.
Status: PASSED! This means that the solver was able to reach the cover statement. We can now inspect the generated .vcd using GTKWave file to see the progressing state of the circuit in the solution:
 Waveform of solution for Stage 2.
I've grouped the signals so it's easy to see the progression of the 'electric signal' across cables (c1,c2,... c8) and joints (s0v, s1v, ...). The s0...s5 signals on the bottom are the joint rotations in which this was possible (2,3,0,1,0,3) - our solution for Stage 2!

We can now write a bit more automation to convert the VCD dumps of the solution into 'rotate' instructions for the challenge binary, and run the same solver succesfully for stages 3 and 4. But for stage 5 (the monster one), we hit a snag:

 Stage 5 impossible to solve.
Seems like Stage 5 is unsolvable!

#### 3 - The Fifth Stage

What do we do now? I'm going to assume that our solver is correct and in fact the fifth stage is not solvable within the confines of just a simple puzzle problem - we need to hack something!

If you look at the stage5 definition from the organizers, you see it has a very large 'answer' value (the number of steps we can take to solve the problem). While in previous stages this was an at most two-digit number, here we're given 114514 steps. So maybe there is something exploitable here?

Let's dive into the C code. Since the only thing we can interact with is the 'direction'/'rotation' of a joint, let's follow that thread of logic. After not too long, we find an interesting bug:

 Challenge code showing how joints are visited by the original 'simulator'.
Turns out the 'direction' of a joint is a char. Any time we 'rotate' it as a user, it just increments by one, without checking for overflows. The modulo operator in the show_circuit function above will seemingly always confine the direction to [0,1,2,3]. But it only does that on joints it's visiting when propagating a 'high' signal.

So if we rotate the joint over 127 times without getting the show_circuit visitor to visit it and sanitize it, we will overflow into -128, -127, -126, -125..., which on first visit and modulo by 4 will turn into [0, -3, -2, -1, 0, -3, ...]. Then, this negative index will be used to acess the available array of the joint definition. This underflow will result in an access to the previous joint type's fonts array.

Since fonts is an array of non-zero character pointers, any check of available that reads a fonts member instead will result in a 'true' availability, so enabled flow for a given direction to a given neighbouring cagle. Thus, if we set the rotation to -127 (-3 after modulo), the new availability will be [1,1,1, original_available[0]]. If we underflow-hack a joint type whose first available array member is a 1 (and is not of type 0, so has a preceding type into which we underflow) we in result get a joint that always connects its 4 cables together (its effective availability is [1,1,1,1]).

 Underflow-hack of available member into previous joint definitions' font member.

So, the plan of action is: find the joint(s) that limit our ability to solve the challenge. Block them off from being visited by show_circuit by rotating joints in front of it to never reach these joints. Then, underflow their direction to -127 (-3 after modulo), so that connectivity is always all-to-all (if the original joint type was [1, x, x, x]).

I played around a bit with the unsolvable generated Verilog model for Stage 5, and found that if I turn Joint 32 into an always-flowing joint, I can solve the stage with the solver. Good news: it's a joint of type 3 (which has its availability[0] set to 1), so we can turn it into an always-flowing joint. It's also directly connected to the source via another joint, Joint 32, that we can close off easily so that the show_circuit visitor never reaches Joint 33.

 Plan of action for hacking Stage 5.
The final 'rotate command' payload will looking something like this:
• Rotate J33 to block it off.
• Rotate  J32 129 times to overflow it to -127 (-3 after modulo), turning it into an always-conducting joint
• Apply rotations from VCD solution for Stage 5, modified to have Joint 33 be always-conducting.
• Rotate J33 to re-enable it.
 Solving the challenge locally.
That's it! The remote flag was CBCTF{Which watchdog watches the watchcats????}.