Plaid CTF - innov8 challenge

import subprocess

secret = open('secret.txt').read().strip()
secretbits = ''.join(f'{ord(i):08b}' for i in secret)

output = []

for bit in secretbits:
    if bit == '0':
        output += [float(i) for i in subprocess.check_output('./d8 gen.js', shell=True).decode().split()]
    else:
        output += [float(i) for i in subprocess.check_output('node gen.js', shell=True).decode().split()]

for i in output:
    print(i)

for (let i = 0; i < 24; i++) {
  console.log(Math.random());
}

// ES6 #sec-math.random
extern macro RefillMathRandom(NativeContext): Smi;

transitioning javascript builtin MathRandom(
    js-implicit context: NativeContext, receiver: JSAny)(): Number {
  let smiIndex: Smi = *NativeContextSlot(ContextSlot::MATH_RANDOM_INDEX_INDEX);
  if (smiIndex == 0) {
    // refill math random.
    smiIndex = RefillMathRandom(context);
  }
  const newSmiIndex: Smi = smiIndex - 1;
  *NativeContextSlot(ContextSlot::MATH_RANDOM_INDEX_INDEX) = newSmiIndex;

  const array: FixedDoubleArray =
      *NativeContextSlot(ContextSlot::MATH_RANDOM_CACHE_INDEX);
  const random: float64 =
      array.values[Convert<intptr>(newSmiIndex)].ValueUnsafeAssumeNotHole();
  return AllocateHeapNumberWithValue(random);
}

Address MathRandom::RefillCache(Isolate* isolate, Address raw_native_context) {
  Tagged<Context> native_context =
      Cast<Context>(Tagged<Object>(raw_native_context));
  DisallowGarbageCollection no_gc;
  Tagged<PodArray<State>> pod =
      Cast<PodArray<State>>(native_context->math_random_state());
  State state = pod->get(0);
  // Initialize state if not yet initialized. If a fixed random seed was
  // requested, use it to reset our state the first time a script asks for
  // random numbers in this context. This ensures the script sees a consistent
  // sequence.

  if (state.s0 == 0 && state.s1 == 0) {
    uint64_t seed;
    if (v8_flags.random_seed != 0) {
      seed = v8_flags.random_seed;
    } else {

      isolate->random_number_generator()->NextBytes(&seed, sizeof(seed));
    }
    state.s0 = base::RandomNumberGenerator::MurmurHash3(seed);
    state.s1 = base::RandomNumberGenerator::MurmurHash3(~seed);
    CHECK(state.s0 != 0 || state.s1 != 0);
  }

  Tagged<FixedDoubleArray> cache =
      Cast<FixedDoubleArray>(native_context->math_random_cache());
  // Create random numbers.
  for (int i = 0; i < kCacheSize; i++) {
    // Generate random numbers using xorshift128+.
    base::RandomNumberGenerator::XorShift128(&state.s0, &state.s1);
    cache->set(i, base::RandomNumberGenerator::ToDouble(state.s0));
  }
  pod->set(0, state);

  Tagged<Smi> new_index = Smi::FromInt(kCacheSize);
  native_context->set_math_random_index(new_index);
  return new_index.ptr();
}

"""
This file contains functions primarily generated by DeepSeek-V3 (then edited by me).

I gave Deepseek the files:

- https://github.com/PwnFunction/v8-randomness-predictor/blob/main/main.py
- chall.py
"""

import z3
import struct
from itertools import batched

def is_node_sequence(floats: list[float]) -> bool:
    assert len(floats) == 24

    reversed_floats = floats[::-1]

    solver = z3.Solver()
    state0, state1 = z3.BitVecs("se_state0 se_state1", 64)

    current_state0 = state0
    current_state1 = state1

    for num in reversed_floats:
        # Compute the mantissa of the number (as per V8's ToDouble method)
        try:
            float_plus_one = num + 1.0
            packed = struct.pack("d", float_plus_one)
            uint64 = struct.unpack("<Q", packed)[0]
            mantissa = uint64 & ((1 << 52) - 1)
        except:
            return False

        # Perform one step of XorShift128+
        s1 = current_state0
        s0 = current_state1
        new_state0 = s0
        s1 ^= s1 << 23
        s1 ^= z3.LShR(s1, 17)
        s1 ^= s0
        s1 ^= z3.LShR(s0, 26)
        new_state1 = s1

        # Add constraint: the upper 52 bits of new_state0 (after shift) must equal the mantissa
        solver.add(z3.LShR(new_state0, 12) == mantissa)

        # Update the current states for next iteration
        current_state0, current_state1 = new_state0, new_state1

    return solver.check() == z3.sat

def reverse_secretbits(secretbits: str) -> str:
    # Split the binary string into chunks of 8 bits
    chunks = [secretbits[i:i+8] for i in range(0, len(secretbits), 8)]
    # Convert each 8-bit binary string to its corresponding character
    return ''.join(chr(int(chunk, 2)) for chunk in chunks)

"""
this script takes "output.txt" from plaidctf.com for the "innov8" challenge.

- https://plaidctf.com/challenge/5
- https://plaidctf.com/files/innov8_excav8.d35e5bf36e3e6438dd960aa7adeeb1dcbb25479bddd96509ba72968e1238b488.tgz

It was adapted from PwnFunction's v8-randomness-predictor.

- https://github.com/PwnFunction/v8-randomness-predictor
"""

from deepseek import is_node_sequence, reverse_secretbits
from itertools import batched
from tqdm import tqdm


def is_node_wrapper(f: list[float]) -> int:
    assert len(f) == 24
    if is_node_sequence(f):
        return 1
    else:
        return 0

def main():
    print('starting...')

    with open("output.txt") as f:
        numbers = [float(line.strip()) for line in f]
        windows = batched(numbers, 24)

    decoded_bits = ""

    for group in tqdm(windows):
        bit = is_node_wrapper(group)
        print(bit)
        decoded_bits += str(bit)

    print(reverse_secretbits(decoded_bits))

if __name__ == "__main__":
    main()