added web challenge
This commit is contained in:
18
bi0sctf23/web/src/Dockerfile
Normal file
18
bi0sctf23/web/src/Dockerfile
Normal file
@@ -0,0 +1,18 @@
|
||||
FROM node:20.2.0-alpine
|
||||
|
||||
RUN apk update && apk upgrade
|
||||
RUN apk add chromium
|
||||
|
||||
WORKDIR /app
|
||||
COPY . /app/
|
||||
RUN mkdir -p /app/notes
|
||||
|
||||
RUN PUPPETEER_SKIP_CHROMIUM_DOWNLOAD=1 npm install
|
||||
RUN chmod +x /app/index.js
|
||||
RUN rm *.json
|
||||
|
||||
RUN adduser -D -u 1001 bot && chown -R bot:bot /app/notes && chown bot:bot /app/settings.proto
|
||||
|
||||
USER bot
|
||||
ENV PUPPETEER_EXECUTABLE_PATH=/usr/bin/chromium-browser
|
||||
ENTRYPOINT ["node", "index.js"]
|
||||
15
bi0sctf23/web/src/bot.js
Normal file
15
bi0sctf23/web/src/bot.js
Normal file
@@ -0,0 +1,15 @@
|
||||
const puppeteer = require('puppeteer');
|
||||
|
||||
async function healthCheck(){
|
||||
const browser = await puppeteer.launch({
|
||||
headless: true,
|
||||
args:['--no-sandbox']
|
||||
});
|
||||
|
||||
const page = await browser.newPage();
|
||||
await page.setJavaScriptEnabled(false)
|
||||
const response=await page.goto("http://localhost:3000/view/Healthcheck")
|
||||
await browser.close();
|
||||
}
|
||||
|
||||
module.exports = { healthCheck };
|
||||
200
bi0sctf23/web/src/index.js
Normal file
200
bi0sctf23/web/src/index.js
Normal file
@@ -0,0 +1,200 @@
|
||||
const express = require('express');
|
||||
const fs = require('fs');
|
||||
const protobuf = require('protobufjs');
|
||||
const glob = require('glob');
|
||||
const { healthCheck } = require('./bot');
|
||||
const app = express();
|
||||
const port = 3000;
|
||||
|
||||
function generateNoteId(length) {
|
||||
const characters = 'abcdefghijklmnopqrstuvwxyz0123456789';
|
||||
let result = '';
|
||||
for (let i = 0; i < length; i++) {
|
||||
const randomIndex = Math.floor(Math.random() * characters.length);
|
||||
result += characters.charAt(randomIndex);
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
let noteList = [];
|
||||
let flag = process.env.FLAG;
|
||||
if(!flag){
|
||||
flag='{"title":"flag","content":"bi0sctf{fake_flag}"}';
|
||||
}
|
||||
else{
|
||||
flag=`{"title":"flag","content":"${flag}"}`;
|
||||
}
|
||||
const flagid = generateNoteId(16);
|
||||
const healthCheckId='Healthcheck';
|
||||
fs.writeFileSync(`./notes/${flagid}.json`, flag);
|
||||
fs.writeFileSync(`./notes/${healthCheckId}.json`, '{"title":"Healthcheck","content":"success"}');
|
||||
|
||||
app.use(express.json());
|
||||
|
||||
app.set('view engine', 'ejs');
|
||||
app.set('views', __dirname + '/views');
|
||||
|
||||
const restrictToLocalhost = (req, res, next) => {
|
||||
const remoteAddress = req.connection.remoteAddress;
|
||||
if (remoteAddress === '::1' || remoteAddress === '127.0.0.1' || remoteAddress === '::ffff:127.0.0.1') {
|
||||
next();
|
||||
} else {
|
||||
res.status(403).json({ Message: 'Access denied' });
|
||||
}
|
||||
};
|
||||
|
||||
const cleanserver = () => {
|
||||
Object.keys(require.cache).forEach(i => {
|
||||
delete require.cache[i];
|
||||
});
|
||||
};
|
||||
|
||||
app.use('/search', restrictToLocalhost);
|
||||
|
||||
app.get('/delete', (req,res) => {
|
||||
cleanserver();
|
||||
return res.json({Message: 'Notes deleted successfully!'});
|
||||
});
|
||||
|
||||
app.get('/search/:noteId', (req, res) => {
|
||||
const noteId = req.params.noteId;
|
||||
const notes=glob.sync(`./notes/${noteId}*`);
|
||||
if(notes.length === 0){
|
||||
return res.json({Message: "Not found"});
|
||||
}
|
||||
else{
|
||||
try{
|
||||
fs.accessSync(`./notes/${noteId}.json`);
|
||||
return res.json({Message: "Note found"});
|
||||
}
|
||||
catch(err){
|
||||
return res.status(500).json({ Message: 'Internal server error' });
|
||||
}
|
||||
}
|
||||
|
||||
})
|
||||
|
||||
app.get('/customise', (req, res) => {
|
||||
return res.render('customise');
|
||||
});
|
||||
|
||||
app.post('/customise',(req, res) => {
|
||||
try {
|
||||
const { data } = req.body;
|
||||
|
||||
let author = data.pop()['author'];
|
||||
|
||||
let title = data.pop()['title'];
|
||||
|
||||
let protoContents = fs.readFileSync('./settings.proto', 'utf-8').split('\n');
|
||||
|
||||
if (author) {
|
||||
protoContents[5] = ` ${author} string author = 3 [default="user"];`;
|
||||
}
|
||||
|
||||
if (title) {
|
||||
protoContents[3] = ` ${title} string title = 1 [default="user"];`;
|
||||
}
|
||||
|
||||
fs.writeFileSync('./settings.proto', protoContents.join('\n'), 'utf-8');
|
||||
|
||||
return res.json({ Message: 'Settings changed' });
|
||||
} catch (error) {
|
||||
console.error(error);
|
||||
res.status(500).json({ Message: 'Internal server error' });
|
||||
}
|
||||
})
|
||||
|
||||
app.get('/create', (req, res) => {
|
||||
return res.render('create', { noteList, Message: false });
|
||||
});
|
||||
|
||||
app.post('/create', (req, res) => {
|
||||
requestBody=req.body
|
||||
try{
|
||||
schema = fs.readFileSync('./settings.proto', 'utf-8');
|
||||
root = protobuf.parse(schema).root;
|
||||
Note = root.lookupType('Note');
|
||||
errMsg = Note.verify(requestBody);
|
||||
|
||||
if (errMsg){
|
||||
return res.json({ Message: `Verification failed: ${errMsg}` });
|
||||
}
|
||||
buffer = Note.encode(Note.create(requestBody)).finish();
|
||||
decodedData = Note.decode(buffer).toJSON();
|
||||
|
||||
const noteId = generateNoteId(16);
|
||||
fs.writeFileSync(`./notes/${noteId}.json`, JSON.stringify(decodedData));
|
||||
noteList.push(noteId);
|
||||
|
||||
return res.json({Message: 'Note created successfully!',Noteid: noteId });
|
||||
}
|
||||
catch (error) {
|
||||
console.error(error);
|
||||
res.status(500).json({Message: 'Internal server error' });
|
||||
}
|
||||
});
|
||||
|
||||
|
||||
app.get('/view/:noteId', (req, res) => {
|
||||
const noteId = req.params.noteId;
|
||||
|
||||
try {
|
||||
let note=require.resolve(`./notes/${noteId}`);
|
||||
if(!note.endsWith(".json")){
|
||||
return res.status(500).json({ Message: 'Internal Server Error' });
|
||||
}
|
||||
|
||||
let noteData = require(`./notes/${noteId}`);
|
||||
for (var key in module.constructor._pathCache) {
|
||||
if (key.startsWith("./notes/"+noteId)){
|
||||
if (!module.constructor._pathCache[key].endsWith(noteId+".json")){
|
||||
if (noteId===healthCheckId){
|
||||
cleanserver();
|
||||
}
|
||||
delete module.constructor._pathCache[key];
|
||||
return res.status(500).json({ Message: 'Internal Server Error' });
|
||||
}
|
||||
}
|
||||
}
|
||||
if(req.query.temp !== undefined){
|
||||
fs.unlink(`./notes/${noteId}.json`, (unlinkError) => {
|
||||
if (unlinkError) {
|
||||
console.error('File missing');
|
||||
}
|
||||
noteList=noteList.filter((value)=>value!=noteId);
|
||||
});
|
||||
}
|
||||
return res.render('view', { noteData });
|
||||
|
||||
} catch (error) {
|
||||
console.log(error)
|
||||
return res.status(500).json({ Message: 'Internal Server Error' });
|
||||
}
|
||||
});
|
||||
|
||||
|
||||
app.get('/healthcheck',async(req,res)=>{
|
||||
try {
|
||||
await healthCheck();
|
||||
|
||||
return res.json({ Message: 'healthcheck successful' });
|
||||
} catch (error) {
|
||||
console.error(error);
|
||||
return res.json({ Message: 'healthcheck failed' });
|
||||
}
|
||||
});
|
||||
|
||||
app.get('/', (req, res) => {
|
||||
return res.redirect('/create');
|
||||
});
|
||||
|
||||
|
||||
app.use((err, req, res, next) => {
|
||||
console.error(err.stack);
|
||||
res.status(500).json({ error: 'Internal Server Error' });
|
||||
});
|
||||
|
||||
app.listen(port, () => {
|
||||
console.log(`Server running on port ${port}`);
|
||||
});
|
||||
4499
bi0sctf23/web/src/package-lock.json
generated
Normal file
4499
bi0sctf23/web/src/package-lock.json
generated
Normal file
File diff suppressed because it is too large
Load Diff
19
bi0sctf23/web/src/package.json
Normal file
19
bi0sctf23/web/src/package.json
Normal file
@@ -0,0 +1,19 @@
|
||||
{
|
||||
"name": "bi0sctfchall",
|
||||
"version": "1.0.0",
|
||||
"description": "",
|
||||
"main": "index.js",
|
||||
"scripts": {
|
||||
"test": "echo \"Error: no test specified\" && exit 1"
|
||||
},
|
||||
"author": "",
|
||||
"license": "ISC",
|
||||
"dependencies": {
|
||||
"body-parser": "1.20.2",
|
||||
"ejs": "3.1.9",
|
||||
"express": "4.18.2",
|
||||
"glob": "10.3.3",
|
||||
"protobufjs": "7.2.3",
|
||||
"puppeteer": "21.5.2"
|
||||
}
|
||||
}
|
||||
7
bi0sctf23/web/src/settings.proto
Normal file
7
bi0sctf23/web/src/settings.proto
Normal file
@@ -0,0 +1,7 @@
|
||||
syntax = "proto2";
|
||||
|
||||
message Note {
|
||||
optional string title = 1 [default="user"];
|
||||
optional string content = 2;
|
||||
optional string author = 3 [default="user"];
|
||||
}
|
||||
156
bi0sctf23/web/src/views/create.ejs
Normal file
156
bi0sctf23/web/src/views/create.ejs
Normal file
@@ -0,0 +1,156 @@
|
||||
<!-- views/create.ejs -->
|
||||
<!DOCTYPE html>
|
||||
<html>
|
||||
<head>
|
||||
<title>Create Note</title>
|
||||
<style>
|
||||
body {
|
||||
background-color: #303030; /* Dark background color */
|
||||
color: #ffffff; /* Text color */
|
||||
font-family: 'Arial', sans-serif;
|
||||
display: flex;
|
||||
align-items: center;
|
||||
justify-content: center;
|
||||
height: 100vh;
|
||||
margin: 0;
|
||||
}
|
||||
|
||||
.card {
|
||||
background-color: #444444; /* Card background color */
|
||||
border-radius: 8px;
|
||||
box-shadow: 0 4px 8px rgba(0, 0, 0, 0.2);
|
||||
padding: 20px;
|
||||
width: 400px;
|
||||
box-sizing: border-box;
|
||||
}
|
||||
|
||||
h1, h2 {
|
||||
color: #ffffff; /* Heading text color */
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
form {
|
||||
max-width: 100%;
|
||||
margin-top: 20px;
|
||||
}
|
||||
|
||||
label {
|
||||
color: #ffffff; /* Label text color */
|
||||
}
|
||||
|
||||
input[type="text"], textarea {
|
||||
width: 100%;
|
||||
padding: 10px;
|
||||
margin: 8px 0;
|
||||
box-sizing: border-box;
|
||||
background-color: #333333; /* Input background color */
|
||||
color: #ffffff; /* Input text color */
|
||||
border: 1px solid #ffffff; /* Input border color */
|
||||
}
|
||||
|
||||
input[type="button"] {
|
||||
background-color: #ffffff; /* Button background color */
|
||||
color: #303030; /* Button text color */
|
||||
padding: 10px 15px;
|
||||
border: none;
|
||||
cursor: pointer;
|
||||
width: 100%;
|
||||
}
|
||||
|
||||
input[type="button"]:hover {
|
||||
background-color: #555555; /* Button background color on hover */
|
||||
}
|
||||
|
||||
#message {
|
||||
color: #ff0000; /* Error message color */
|
||||
margin-top: 10px;
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
#noteList {
|
||||
list-style-type: none;
|
||||
padding: 0;
|
||||
}
|
||||
|
||||
#noteList li {
|
||||
margin-bottom: 8px;
|
||||
}
|
||||
|
||||
#noteList a {
|
||||
text-decoration: none;
|
||||
color: #ffffff; /* Link text color */
|
||||
}
|
||||
|
||||
#noteList a:hover {
|
||||
text-decoration: underline;
|
||||
}
|
||||
</style>
|
||||
</head>
|
||||
<body>
|
||||
<div class="card">
|
||||
<h1>Create a New Note</h1>
|
||||
<form id="noteForm">
|
||||
<label for="title">Title:</label><br>
|
||||
<input type="text" id="title" name="title" required><br>
|
||||
<label for="content">Content:</label><br>
|
||||
<textarea id="content" name="content" rows="4" cols="50" required></textarea><br><br>
|
||||
<input type="button" value="Create Note" onclick="submitNote()">
|
||||
</form>
|
||||
|
||||
<div id="message" style="color: red;"></div>
|
||||
|
||||
<script>
|
||||
function addItemToList(item) {
|
||||
const noteList = document.getElementById('noteList');
|
||||
const listItem = document.createElement('li');
|
||||
|
||||
const link = document.createElement('a');
|
||||
link.href = `/view/${item.Noteid}`;
|
||||
link.textContent = item.Noteid;
|
||||
listItem.appendChild(link);
|
||||
|
||||
noteList.appendChild(listItem);
|
||||
}
|
||||
|
||||
function submitNote() {
|
||||
const title = document.getElementById("title").value;
|
||||
const content = document.getElementById("content").value;
|
||||
|
||||
const noteData = { title, content };
|
||||
|
||||
fetch("/create", {
|
||||
method: "POST",
|
||||
headers: {
|
||||
"Content-Type": "application/json",
|
||||
},
|
||||
body: JSON.stringify(noteData),
|
||||
})
|
||||
.then((response) => response.json())
|
||||
.then((data) => {
|
||||
if (data.Message) {
|
||||
document.getElementById("message").innerHTML = data.Message;
|
||||
if (data.Noteid){
|
||||
addItemToList(data);
|
||||
}
|
||||
}
|
||||
})
|
||||
.catch((error) => {
|
||||
console.error("error:", error);
|
||||
document.getElementById("message").innerText = 'Error';
|
||||
});
|
||||
|
||||
}
|
||||
</script>
|
||||
|
||||
<% if (Message) { %>
|
||||
<p><%= Message %></p>
|
||||
<% } %>
|
||||
<h2>Created Notes:</h2>
|
||||
<ul id="noteList" style="text-align:center">
|
||||
<% for (const noteId of noteList) { %>
|
||||
<li><a href="/view/<%= noteId %>"><%= noteId %></a></li>
|
||||
<% } %>
|
||||
</ul>
|
||||
</div>
|
||||
</body>
|
||||
</html>
|
||||
56
bi0sctf23/web/src/views/customise.ejs
Normal file
56
bi0sctf23/web/src/views/customise.ejs
Normal file
@@ -0,0 +1,56 @@
|
||||
<!-- views/customise.ejs -->
|
||||
<!DOCTYPE html>
|
||||
<html>
|
||||
<head>
|
||||
<title>Settings</title>
|
||||
</head>
|
||||
<body>
|
||||
<h1>Settings</h1>
|
||||
<form id="customizationForm">
|
||||
<label for="titleCheckbox">Title:</label>
|
||||
<input type="checkbox" id="titleCheckbox" name="titleCheckbox">
|
||||
|
||||
<label for="authorCheckbox">Author:</label>
|
||||
<input type="checkbox" id="authorCheckbox" name="authorCheckbox">
|
||||
|
||||
<button type="button" onclick="customizeFields()">Customize</button>
|
||||
</form>
|
||||
|
||||
<div id="message" style="color: red;"></div>
|
||||
|
||||
<script>
|
||||
function customizeFields() {
|
||||
const data = [];
|
||||
|
||||
const titleCheckbox = document.getElementById('titleCheckbox');
|
||||
const authorCheckbox = document.getElementById('authorCheckbox');
|
||||
|
||||
if (titleCheckbox.checked) {
|
||||
data.push({ title: 'required' });
|
||||
} else {
|
||||
data.push({ title: 'optional' });
|
||||
}
|
||||
|
||||
if (authorCheckbox.checked) {
|
||||
data.push({ author: 'required' });
|
||||
} else {
|
||||
data.push({ author: 'optional' });
|
||||
}
|
||||
|
||||
// Send a fetch request with the data array
|
||||
fetch('/customise', {
|
||||
method: 'POST',
|
||||
headers: {
|
||||
'Content-Type': 'application/json',
|
||||
},
|
||||
body: JSON.stringify({ data }),
|
||||
})
|
||||
.then(response => response.json())
|
||||
.then(result => {
|
||||
document.getElementById("message").innerText = result.Message;
|
||||
})
|
||||
.catch(error => console.error('Error:', error));
|
||||
}
|
||||
</script>
|
||||
</body>
|
||||
</html>
|
||||
67
bi0sctf23/web/src/views/view.ejs
Normal file
67
bi0sctf23/web/src/views/view.ejs
Normal file
@@ -0,0 +1,67 @@
|
||||
<!-- views/view.ejs -->
|
||||
<!DOCTYPE html>
|
||||
<html>
|
||||
<head>
|
||||
<title>Note Viewer</title>
|
||||
<style>
|
||||
body {
|
||||
font-family: Arial, sans-serif;
|
||||
background-color: #f2f2f2;
|
||||
color: #333333;
|
||||
margin: 0;
|
||||
padding: 0;
|
||||
}
|
||||
|
||||
.container {
|
||||
max-width: 800px;
|
||||
margin: 20px auto;
|
||||
padding: 20px;
|
||||
background-color: #ffffff;
|
||||
box-shadow: 0 0 10px rgba(0, 0, 0, 0.1);
|
||||
border-radius: 5px;
|
||||
}
|
||||
|
||||
h1 {
|
||||
font-size: 24px;
|
||||
color: #333333;
|
||||
margin-bottom: 20px;
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
h2 {
|
||||
font-size: 20px;
|
||||
color: #333333;
|
||||
margin-bottom: 10px;
|
||||
}
|
||||
|
||||
p {
|
||||
font-size: 16px;
|
||||
color: #555555;
|
||||
line-height: 1.6;
|
||||
}
|
||||
</style>
|
||||
</head>
|
||||
<body>
|
||||
<div class="container">
|
||||
<h1>Note Details</h1>
|
||||
|
||||
<% if (noteData.title) { %>
|
||||
<h2><%= noteData.title %></h2>
|
||||
<% } %>
|
||||
|
||||
<% if (noteData.author) { %>
|
||||
<p>Author: <%= noteData.author %></p>
|
||||
<% } %>
|
||||
|
||||
<p><%- noteData.content %></p>
|
||||
|
||||
<button onclick="redirectToTemp()">Delete</button>
|
||||
|
||||
</div>
|
||||
<script>
|
||||
function redirectToTemp() {
|
||||
window.location.href = "?temp";
|
||||
}
|
||||
</script>
|
||||
</body>
|
||||
</html>
|
||||
220
bi0sctf23/web/src/xs128p.py
Normal file
220
bi0sctf23/web/src/xs128p.py
Normal file
@@ -0,0 +1,220 @@
|
||||
import argparse
|
||||
import struct
|
||||
from decimal import *
|
||||
import os
|
||||
from z3 import *
|
||||
|
||||
MAX_UNUSED_THREADS = 2
|
||||
|
||||
|
||||
# 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 solve_instance(points, multiple, unknown_leading=False):
|
||||
# setup symbolic state for xorshift128+
|
||||
ostate0, ostate1 = BitVecs('ostate0 ostate1', 64)
|
||||
sym_state0 = ostate0
|
||||
sym_state1 = ostate1
|
||||
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
|
||||
slvr = SolverFor(
|
||||
"QF_BV") # This type of problem is much faster computed using QF_BV (also, if branching happens, we can use parallelization)
|
||||
|
||||
# run symbolic xorshift128+ algorithm for three iterations
|
||||
# using the recovered numbers as constraints
|
||||
|
||||
if unknown_leading:
|
||||
# we want to try to predict one value ahead so let's slide one unknown into the calculation
|
||||
sym_state0, sym_state1 = sym_xs128p(sym_state0, sym_state1)
|
||||
|
||||
for point in points:
|
||||
sym_state0, sym_state1 = sym_floor_random(slvr, sym_state0, sym_state1, point, multiple)
|
||||
|
||||
if slvr.check() == sat:
|
||||
# get a solved state
|
||||
m = slvr.model()
|
||||
state0 = m[ostate0].as_long()
|
||||
state1 = m[ostate1].as_long()
|
||||
|
||||
return state0, state1
|
||||
else:
|
||||
print("Failed to find a valid solution")
|
||||
return None, None
|
||||
|
||||
def solve(points, multiple, lead):
|
||||
if lead > 0:
|
||||
last_state0 = None
|
||||
last_state1 = None
|
||||
|
||||
for i in range(0, int(lead)):
|
||||
last_state0, last_state1 = solve_instance(points, multiple, True)
|
||||
|
||||
state0, state1, output = xs128p(last_state0, last_state1)
|
||||
new_point = math.floor(multiple * to_double(output))
|
||||
points = [new_point] + points
|
||||
|
||||
return last_state0, last_state1
|
||||
else:
|
||||
return solve_instance(points, multiple)
|
||||
|
||||
|
||||
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('--multiple',
|
||||
help="Specifies the multiplier used in 'Math.floor(MULTIPLE * Math.random())'. Defaults to 1.")
|
||||
parser.add_argument('--gen',
|
||||
help="Instead of predicting state, take a state pair and generate output. (state0,state1,num)")
|
||||
parser.add_argument('--lead',
|
||||
help="The number of elements backwards to predict")
|
||||
|
||||
args = parser.parse_args()
|
||||
|
||||
multiple_arg = args.multiple
|
||||
lead_arg = args.lead
|
||||
|
||||
multiple = 1.0 if multiple_arg is None else float(multiple_arg)
|
||||
lead = 0 if lead_arg is None else float(lead_arg)
|
||||
|
||||
if args.gen:
|
||||
state0, state1, count = list(map(lambda x: int(x), args.gen.split(",")))
|
||||
|
||||
return None, multiple, (state0, state1, count), None
|
||||
else:
|
||||
points = list(map(lambda line: int(line), sys.stdin.readlines()))
|
||||
|
||||
assert len(
|
||||
points) != 0, "Pipe the leaked, unbucketed points via STDIN.\nExample:\n\tcat FILE | python3 xs2.py --multiple 1000"
|
||||
|
||||
return lead, multiple, None, points
|
||||
|
||||
def 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)
|
||||
# -----------------------------------------------------------------------------------------------------------------------------------------------------------
|
||||
"""
|
||||
|
||||
lead, multiple, gen, points = get_args()
|
||||
|
||||
if gen is not None:
|
||||
state0, state1, count = gen
|
||||
|
||||
for i in range(count):
|
||||
state0, state1, output = xs128p(state0, state1)
|
||||
print(math.floor(multiple * to_double(output)))
|
||||
else:
|
||||
state0, state1 = solve(points, multiple, lead)
|
||||
|
||||
if state0 is not None and state1 is not None:
|
||||
print("{},{}".format(state0, state1))
|
||||
|
||||
|
||||
main()
|
||||
Reference in New Issue
Block a user