That’s a lot of fish (400pt)

Rev

Story

The hot sun relentlessly beats down on you as you stagger across the scorching sands of the desert. You’ve been walking for hours and the endless flat landscape hasn’t helped the dizzying feeling you’ve felt from dehydration, but you had to keep moving.

After escaping the sand prison, you opened up the map on your HUD to see where you were. Except there was no map. You were facing a blank screen. For some reason, even escaping the sand prison hasn’t helped with your HUD at all.

“This is fine. Everything is fine. I’m just gonna teleport back home then.”

The dehydration is getting to you, and you’re talking to yourself. It’s a little hard with your tongue so swollen. You go back a few menus on the HUD to teleport to home. But nothing happens when you press the button. Starting to panic, you try to exit REFUGE, but that button doesn’t work either. Frustrated, you try hitting all of the buttons a few more times, but don’t get any feedback. So you pick a direction and start walking.

And then you find out the hard way what happens when you try to teleport about 25 times during a lag spike. You see flashes of a whole bunch of different locations—your home, the carnival, the stegosaurus fountain at the entrance of the plaza, your house outside REFUGE, the HQB library—before your brain finally shuts off completely from sensory overload and you black out.

You hear a siren. Groggily, you lift your head, and find yourself in the middle of a towering city; but it doesn’t look like one you’ve ever seen. It’s not nearly nice enough to be one in REFUGE, not nearly dingy enough to be in the real world. Something feels very, very off here. Oh, and your HUD is gone, so that’s cool.

After a few moments, you hear a loud BANG! from a few streets over. A military convoy of some sort suddenly appears from one of the nearby cross streets. With no other ideas for how to proceed, you choose to follow.

What you see there is… confusing. There’s something that looks like Godzilla attacking a skyscraper, but it seems to be made completely of metal. Mechagodzilla? And the military force you followed here doesn’t seem to have a whole lot of weapons. Instead, from the vehicles, you see them unload tons upon tons of fresh fish, amassing them into one giant heap in the middle of the road. Are they trying to distract a mechanical monster with food? That doesn’t sound like a great plan to you.

An onlooker beside you that you hadn’t noticed up to this point suddenly pipes up. “That’s a lot of fish,” he states flatly.

He’s not wrong, you suppose.

As you watch on, for just a moment, you see a corner of a flag sticking out of the pile of fish, before being covered up by some cod and salmon that are added to the top of the pile. Well, it’s not like you have a better option, right? You run up to the smelly pile and plunge in your hands, desperately hoping to locate that flag you just saw.

Files:

• thats_a_lot_of_fish.gz

Extra:

• clean.ts: typescript source with proper indentation/formatting
• solution.ts: my renamed source with the correct input to print the flag

Overview:

I worked with slOwOck on the initial reversing effort, defund and clam solved the last step once we figured out the constraints.

We are presented with a heavily obfuscated typescript file and a patch to the typescript compile that will let us compile really deeply nested types.

Interestingly most of the code in the typescript file consists of type expressions. The only non-type expression is this line:

Triplespine("your input goes here" as const);

This will invoke the following generic function:

function Triplespine<Largemouth_bass>(
  magikarp: Largemouth_bass &
    (Nase<Largemouth_bass> extends infer Glassfish
      ? Glassfish extends Silver_dory
        ? Sculpin<Glassfish>
        : Dogfish
      : Dogfish)
) {
  let goldeen = (magikarp as any)
    .map((x) => parseInt(x.join(""), 2).toString(16))
    .join("");
  let stunfisk = "";
  for (let i = 0; i < 1000000; i++) {
    stunfisk = require("crypto")
      .createHash("sha512")
      .update(stunfisk)
      .update(goldeen)
      .digest("hex");
  }
  let feebas = Buffer.from(stunfisk, "hex");
  let remoraid = Buffer.from(
    "0ac503f1627b0c4f03be24bc38db102e39f13d40d33e8f87f1ff1a48f63a02541dc71d37edb35e8afe58f31d72510eafe042c06b33d2e037e8f93cd31cba07d7",
    "hex"
  );
  for (var i = 0; i < 64; i++) {
    feebas[i] ^= remoraid[i];
  }
  console.log(feebas.toString("utf-8"));
}

The Largemouth_bass identifier is a type parameter that will be inferred (since we don’t explicitly specify the type in our function invocation). In order for this code to compile, Nase<Largemouth_bass> needs to extend a class that extends Silver_dory and Sculpin<Glassfish> needs to resolve to any. Otherwise, we will get a compilation error on assignment since our type is resolved to never.

However, once this compiles, it will produce a script that will compute a hash over and over and eventually decrypt the flag.

Part 0: Intro to TypeScript

I had never used TypeScript before this challenge and honestly now I think I’m too scared to ever use it again. The basic idea with TypeScript is it’s JavaScript but you have types (duh).

The type checker is very powerful, like turing complete level of powerful. In order to reverse this code we first need to learn a bit about how types work in TypeScript. I’ll outline some basic patterns here but I would also recommend reading through the handbook.

Simple types:

A type comes after the : in a variable declaration or parameter list.

let a: true;    // type: true
let b: false;   // type: false
let c: [];      // type: []
let d: any;     // type: any
let e: never;   // type: never (can't assign to this type)
let f: 5;       // type: 5 (not value, this can only ever be 5)

Named types:

We can name a type with the type keyword. The | operator is a “union” type.

type bin_val = 0|1;         // type: 0|1
type bin_arr = bin_val[];   // type: (0|1)[]

let good: bin_arr = [0,1,0,0,0,1];

// Error: "Type 2 is not assignable to type bin_val"
let my_arr: bin_arr = [0,1,2];

Object types:

We can construct array types that are constrained to explicit values:

type my_obj = [0,1,1,0];
let obj_a: my_obj = [0,1,1,0];  // ok

// Error: "Type 1 is not assignable to type 0"
let obj_b: my_obj = [1,1,1,0];

Conditional types:

We can create generic types that conditionally resolve to different types (at compile time).

type test<H> = (H extends 1 ? any : never);

type test_a = test<1>;  // type: any
type test_b = test<0>;  // type: never

Type inference:

We can use the infer keyword to search for a matching type (like pattern matching). This lets us do some cool stuff like:

type Pair<A,B> = [A,B];
type First<H> = H extends [infer A, infer B] ? A : never;
type Second<H> = H extends [infer A, infer B] ? B : never;

let first: First<Pair<1,99>>;       // type: 1
let second: Second<Pair<1,99>>;     // type: 99

Wow this is starting to look like lambda calculus!

Parameters<K> type

We can use the builtin Parameters<K> type to return function parameters. This lets us start building lists:

type Prepend<A, L extends any[]> = Parameters<(
    (a: A, ...b: L) => void
)>;

let c1: Prepend<3, [0,1,5]>;     // type: [3,0,1,5]

Function types

We can use the ... variable argument parameter to greedily match list types. This lets us do even crazier stuff:

type GetHead<L extends any[]> = (
    (
        (...list: L) => void
    ) extends (
        (h: infer H, ...t: infer T) => void
    ) ? H : never
)

type GetBody<L extends any[]> = (
    (
        (...list: L) => void
    ) extends (
        (h: infer H, ...t: infer T) => void
    ) ? T : never
)

let b1: Head<[0,1,2,3]>;                      // type: 0
let b2: GetBody<[0,1,2,3]>;                   // type: [1,2,3]
let b3: GetBody<GetBody<[0,1,2,3]>>;          // type: [2,3]
let b4: GetBody<GetBody<GetBody<[0,1,2,3]>>>; // type: [3]

Index trick

We can’t directly reference a type in its own assignment. However we can construct an object and index into into it conditionally to achieve recursion. For example:

type Reverse<L extends any[], R extends any[] = []> = {
    done: R,
    recurse: Reverse<GetBody<L>, Prepend<GetHead<L>, R>>
}[
    L extends [] ? "done" : "recurse"
];

let r: Reverse<[1,2,3,4]>;  // type: [4,3,2,1]

If L is empty, Reverse evaluates to R. Otherwise, it evaluates to Reverse<GetBody<L>, Prepend<GetHead<L>, R>>.

Type enlightenment

Once you have made it this far, there is nothing stopping you. You feel the power of the type checker running through your veins.

Read this for inspiration and then go forth and decode the fishes!

I would recommend trying this problem on your own if you haven’t already. It’s very rewarding uncovering all the different patterns. Once you figure out what something does, give it a sensible name and it will make the process a lot easier.

I’ve uploaded a solution script here that contains renamed functions if you got stuck at a certain point.

Part 1: Fish

Let’s start unpacking the control flow. The first thing we need to resolve is the conditional type checks in Triplespine.

Here they are:

function Triplespine<Largemouth_bass>(
  magikarp: Largemouth_bass &
    (Nase<Largemouth_bass> extends infer Glassfish
      ? Glassfish extends Silver_dory
        ? Sculpin<Glassfish>
...

Nase turns out to be a boring type that just makes the object immutable:

type Nase<Zebra_loach> = {
  -readonly [Longnose_chimaera in keyof Zebra_loach]: Nase<
    Zebra_loach[Longnose_chimaera]
  >;
};

Next, we need to make sure our type extends Silver_dory which is defined as:

type Channel_catfish = 0 | 1;
type Leaffish = Channel_catfish[];
type Pancake_batfish = Leaffish & { length: 4 };
type Silver_dory = [
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish,
  Pancake_batfish
];

So our type needs to be a list of size 17 (not 16!) where each element is a length four array that can have types 0 or 1.

For example:

let dat = [
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
    [0,0,0,0],
];

Then our type will resolve to Sculpin<Glassfish>.

type Sculpin<Gizzard_shad extends Silver_dory> = Dragonfish<
    Pike_eel<
        Northern_squawfish<Gizzard_shad>
    >
> extends 0
  ? Nurse_shark     // any
  : Dogfish;        // never

Sculpin needs to evaluate to any so Dragonfish needs to evaluate to 0.

Going from inside to out, we see that Northern_squawfish simply takes our 17 arr data vector, appends to empty lists to the front and a large list to the end.

Then Pike_eel constructs a sort of object type. As it turns out, this will contain the state of our virtual machine so I’ve annotated the fields here:

type Pike_eel<Sand_tilefish extends Leaffish[]> = {
  John_Dory: Sand_tilefish;             // memory buffer
  Sea_toad: [1, 1, 0, 0, 1];            // program counter (19)
  Lefteye_flounder: [[], [], [], []];   // 4 register slots
  Trout_perch: [undefined, undefined];  // 2 heap slots
  Hawkfish: [];                         // call stack
};

Dragonfish turns out to be our RunVM type:

type Dragonfish<Kokopu extends Goldfish> = Yellowtail_barracuda<
  Kokopu
> extends infer Yellowtail
  ? {
      Mud_catfish: Dogfish;
      Sandroller: Yellowtail extends Leaffish
        ? Celebes_rainbowfish<Yellowtail>
        : Dogfish;
      Pineapplefish: Yellowtail extends Goldfish
        ? Dragonfish<Yellowtail>
        : Dogfish;
    }[Yellowtail extends Dogfish
      ? "Mud_catfish"
      : Yellowtail extends Leaffish
      ? "Sandroller"
      : "Pineapplefish"]
  : Dogfish;

Goldfish is a definition of our VM state container. We can see that this type will recursively resolve based on the type resolution of Yellowtail_barracuda.

• If Yellowtail_barracuda<Kokopu> is never, resolve to never
• else if Yellowtail_barracuda<Kokopu> extends Leaffish (a binary vector), resolve to Celebes_rainbowfish<Yellowtail>
• else resolve recursively to Dragonfish again.

So using some intuition about how a VM would work, we can guess that:

• Yellowtail_barracuda is some sort of StepVM function
  • it will either return the next state or a binaryvector result
• Celebes_rainbowfish is some sort of output processing function that needs to eventually resolve to zero for our program to compile

At first Yellowtail_barracuda looks very overwhelming to reverse, but after some time we can pick out patterns and identify what the opcodes are.

If you’re curious on how the code works, I would recommend looking at my solution script where I’ve renamed Yellowtail_barracuda to StepProg and figured out most of the functions within.

Part 2: VM

Now that we know the type checker is running a VM, we can work out the details of this language. The binary vectors in the typescript code end up being reversed binary numbers. For example [0,1,1] == 6 and [1,1,0,0,1] == 19. So it is more convinient to treat them as decimal values.

Instructions can read and write to memory, there are four read modes and three writing modes. A parameter specifies the mode in the bottom two bits of the value.

Reading:

• mode 0: x (immediate)
• mode 1: Rx (register value)
• mode 2: [x] (memory address)
• mode 3: [Rx] (indirect memory address)

Writing has the same modes except for 0 which will throw an error.

There are 15 opcodes. Instructions are 2-4 values long.

• 0 : out <src> :: output src and halt
• 1 : set <dest> <src> :: dest = src
• 2 : add <dest> <src> :: dest = dest + src
• 3 : mul <dest> <src> :: dest = dest * src
• 4 : and <dest> <src> :: dest = dest & src
• 5 : or <dest> <src> :: dest = dest | src
• 6 : xor <dest> <src> :: dest = dest ^ src
• 7 : sne <dest> <src> :: dest = (dest == src ? 0 : 1)
• 8 : neg <dest> <src> :: dest = -src (two’s complement)
• 9 : jmp <target> :: pc = pc + 2 + target
• 10 : bne <target> <src> :: pc = (src != 0 ? pc + 3 + target: pc + 3)
• 11 : setobj <slot> <val> <key> :: add a (val,key) node to heap[slot]
• 12 : getobj <out_val> <out_key> <slot> :: pop the node with the smallest value from heap[slot]
• 13 : clip <dest> <src> :: dest = src & 0xffff
• 14 : call <target> :: stack.push(pc+2) ; pc = target
• 15 : ret :: pc = stack.pop()

In order to reverse this binary, I wrote a plugin for BinaryNinja: https://github.com/hgarrereyn/bn-fish-disassembler.

I also needed to convert the list representaion in typescript to some binary format. Some values were very large in the ROM code so I converted each bitvec list to 4 bytes on disk and scaled all memory accesss by 4 so things would line up.

Using the plugin, we can get a nice graph view of the code:

Our goal is to get to the out 0x0 instruction in the bottom left. When our code is loaded, the bitvecs we provide are in the range MEM[2:19].

Using this plugin I was able to reverse engineer the logic and replicate it in python:

target = [9, 218, 240, 218, 193, 238, 169, 202, 186, 208, 195, 137, 141, 128, 128, 90, 161, 199, 69, 249, 210, 162, 242, 67, 3, 79, 200, 90, 152, 82, 183, 253]

even_target = target[::2]
odd_target = target[1::2]

def check_vecs(v):
    '''v is a list of size 17 containing integers in range [0,16)'''
    total = 0
    
    for i in range(16):
        total += abs(even_target[v[i]] - even_target[v[i+1]])
        total += abs(odd_target[v[i]] - odd_target[v[i+1]])
        
    valid = (total == 0x470) and (len(set(v[:-1])) == 16)
        
    return valid

z3 wasn’t able to handle this efficiently so I passed this off to defund and clam for the final step.

Part 3: Constraints

Defund reformulated the problem in the following way:

target = [(9, 218), (240, 218), (193, 238), (169, 202), (186, 208), (195, 137), (141, 128), (128, 90), (161, 199), (69, 249), (210, 162), (242, 67), (3, 79), (200, 90), (152, 82), (183, 253)]

def check(array):
    total = 0
    for i in range(16):
        x = array[i]
        y = array[(i+1)%16]
        total += abs(x[0] - y[0])
        total += abs(x[1] - y[1])
    return total == 0x470

check(target)

Since we must use every vec value exactly once, we can think of each vec as a 2d point. Then our total value is simply the total round-trip manhattan distance based on our permutation.

Additionally, most permutations seem to be much larger than 0x470 so we need to find a minimum round trip manhattan distance which turns out to be a pretty famous NP-Hard problem.

Clam graphed out the points:

then proceeded to solve it by hand…

to obtain the vector: [0, 9, 15, 2, 1, 4, 3, 8, 10, 5, 13, 11, 14, 6, 7, 12, 0]

We can convert this back to the proper form and compile and run our program:

let dat = [
    [0,0,0,0],
    [1,0,0,1],
    [1,1,1,1],
    [0,1,0,0],
    [1,0,0,0],
    [0,0,1,0],
    [1,1,0,0],
    [0,0,0,1],
    [0,1,0,1],
    [1,0,1,0],
    [1,0,1,1],
    [1,1,0,1],
    [0,1,1,1],
    [0,1,1,0],
    [1,1,1,0],
    [0,0,1,1],
    [0,0,0,0],
];

let goldeen = (dat as any)
    .map((x) => parseInt(x.join(""), 2).toString(16))
    .join("");
let stunfisk = "";
for (let i = 0; i < 1000000; i++) {
    stunfisk = require("crypto")
    .createHash("sha512")
    .update(stunfisk)
    .update(goldeen)
    .digest("hex");
}
let feebas = Buffer.from(stunfisk, "hex");
let remoraid = Buffer.from(
    "0ac503f1627b0c4f03be24bc38db102e39f13d40d33e8f87f1ff1a48f63a02541dc71d37edb35e8afe58f31d72510eafe042c06b33d2e037e8f93cd31cba07d7",
    "hex"
);
for (var i = 0; i < 64; i++) {
    feebas[i] ^= remoraid[i];
}
console.log(feebas.toString("utf-8")); 

🐠PCTF{s0_Lon6_4Nd_tHanK5_f0R_4lL_Th3_f15H!_f74857d88a039}🐟