the cr0wn

The UK’s Top Competitive Cyber Security Team

hxp 36C3 CTF

Nacht

Description: Our yearly misusing-the-unmisusable challenge.

Download: nacht-d2584f79058ea013.tar.xz (760 Bytes)

Connection: nc 88.198.156.141 2833

NaCl, short for “Networking and Cryptography Library” is a collection of easy-to-use cryptography primitives based on Daniel Bernstein et al.’s schemes, including Ed25519, Salsa20, and Poly1305. These schemes are growing in popularity due to their high performance, resistance to strong attacks so far, and Bernstein’s excellent reputation. They are finally making it into widespread protocols like TLS, which from v1.3 requires support of Ed25519 as a key agreement scheme.

TweetNaCl is a tiny implementation of all 25 main NaCl functions written in C, so-called because the entire thing can fit into 100 tweets—and that’s before Twitter doubled the limit to 280 characters!

In this challenge we are given a Python script that interfaces with a TweetNaCl shared object which we must compile from sources. The provided Makefile simply downloads the official sources from https://tweetnacl.cr.yp.to, throws in a definition of randombytes to give the library a CSRNG source, and builds the shared object using GCC.

The Python script comprises:

  1. a method to produce a MAC/tag of a message.
  2. a method to verify that a tag corresponds to a message.
  3. a loop that creates 32 tags of 32 random 32-byte messages, using (what appears to be) the same randomly-generated key.
  4. a challenge which sends us a message and asks us to provide the correct tag for it under the same key.

ctypes is employed to plug the Python methods directly into the TweetNaCl Poly1305 functions:

lib = ctypes.CDLL('./tweetnacl.so')

def mac(key, msg):
    tag = ctypes.create_string_buffer(16)
    lib.crypto_onetimeauth_poly1305_tweet(tag, key, len(msg), msg)
    return bytes(tag)

def chk(key, tag, msg):
    return not lib.crypto_onetimeauth_poly1305_tweet_verify(tag, key, len(msg), msg)

Due to the challenge description, we immediately searched for information on these functions’ signatures to check they are being called properly. According to the documentation, they are not! The key and msg parameters are incorrectly switched around. Note the mlen parameter is irrelevant as both key and msg are 32-bytes long.

To understand the implications of these misused parameters, we found a lightweight Python implementation of Poly1305 to help us dig into the guts of algorithm. Filippo Valsorda also has a very clear explanation along with annotated Go code. The algorithm turned out to be a lot more simple than we expected.

Essentially a Poly1305 tag over a 32-byte message can be expressed as the following equation:

Where and are each half of the key, and are successive 16-byte chunks of the message. is a prime number cleverly chosen to make modular reduction more efficient. There are details about this and other implementation choices here, but they weren’t critical for solving the challenge.

Since we are (mistakenly) given the key, we know and , and the only unknowns in the equation are and , which are the same for all 32 messages we have been sent. Thus we need just a few messages to be able to solve for those values.

However, there is a small complication. To guard against messages with variable numbers of trailing zeroes having the same tag, Poly1305 adds an \x01 byte to the end of each message chunk. Further, although the algorithm works in a field, the final output is 16-bytes long. Therefore, the highest three bits get truncated in the tag, as the algorithm uses little-endian integers <==> bytes conversions. Some information gets lost, but it’s no big deal to just bruteforce these high bits for each chunk.

Overall this looked like a job for Sage, and our resident Sage artisan v01d whipped up a solution script. Wikipedia has an article about solving systems of polynomial equations: we are constructing the ideal of the system and getting the solutions with an algebraic variety of zero, which Sage easily calculates for us.

from chacha20poly1305 import *
from pwn import *

R.<m0, m1> = PolynomialRing(GF(2**130 - 5))


class P1305(Poly1305):
    """overriding some methods so they work in sage/python2
       and for testing and illustrative purposes"""
    @staticmethod
    def le_bytes_to_num(data):
        ret = 0
        for i in range(len(data) - 1, -1, -1):
            ret <<= 8
            ret += ord(data[i])
        return ret

    @staticmethod
    def num_to_16_le_bytes(num):
        ret = [0]*16
        for i, _ in enumerate(ret):
            ret[i] = int(num) & 0xff
            num >>= 8
        return bytearray(ret)


def solvend(keytags):
    def mk_poly(key, tag, tagHi):
        mac = P1305(key)
        return R(mac.s) + m0*R(mac.r)**2 + m1*R(mac.r) - R(P1305.le_bytes_to_num(tag)) - R(2**128)*R(tagHi)

    for t1 in range(0, 5):
        for t2 in range(0, 5):
            for t3 in range(0, 5):
                tagHis = [t1, t2, t3]
                polys = [mk_poly(keytags[i][0], keytags[i][1], tagHis[i])
                         for i in range(len(tagHis))]
                I = R.ideal(polys)
                vrt = I.variety()
                if len(vrt) != 0:
                    print(vrt)
                    return vrt


def rsoln():
    with remote('127.0.0.1', 2833) as t:
        keytags = [map(unhex, t.recvline().split(" ")[:2]) for _ in range(32)]
        challengeKey = unhex(t.recvline().split(" ")[0])
        vrt = solvend(keytags)
        msg = P1305.num_to_16_le_bytes(vrt[0][m0]) + P1305.num_to_16_le_bytes(vrt[0][m1])
        msg = bytes(msg)
        tag = bytes(P1305(challengeKey).create_tag(msg))
        t.sendline(enhex(tag))
        t.interactive()


rsoln()

Here’s a tip if you are getting the following error when trying to use Pwntools and Sage in the same script:

_curses.error: must call (at least) setupterm() first 

Just export the environment variable PWNLIB_NOTERM=true, this will ensure that the two libraries don’t fight over the display on your terminal.

Overall this was a great challenge as the vulnerability was subtle, believable, and fatal. Also it got us to look into the nuts and bolts of an important algorithm in modern crytography which really was more straightforward and fun than we expected.