如何适配脚本预测V8引擎Math.random()截断后的输出？

核心原理 #

Node.js的Math.random()基于XORSHIFT128+算法，只要通过约束还原出伪随机数生成器（PRNG）的内部状态，就能精准预测后续输出。你场景中的RandomInt函数输出，对应Math.random()的明确范围约束：
已知RandomInt(min, max) = val，等价于：

(val - min) / (max - min + 1) ≤ Math.random() < (val - min + 1) / (max - min + 1)

v8_rand_buster正是利用Z3约束求解器，通过这类范围约束反向推导PRNG的内部状态。

具体适配步骤 #

1. 环境准备
   确保安装Python 3.x，然后安装Z3求解器：

   pip install z3-solver
   

2. 整理输入样本
   将你获取到的randomVal1~randomVal7整理成包含(min, max, 结果值)的列表，替换脚本中原有的输入逻辑：

   # 替换为你实际拿到的randomVal1~randomVal7数值
   samples = [
       (250, 300, randomVal1),
       (0, 900, randomVal2),
       (300, 500, randomVal3),
       (0, 800, randomVal4),
       (500, 900, randomVal5),
       (0, 800, randomVal6),
       (0, 900, randomVal7)
   ]
   

3. 修改约束生成逻辑
   找到脚本中绑定PRNG输出约束的代码，替换为范围约束（原脚本可能直接绑定精确值，现在要改成区间约束）：

   from z3 import *
   
   # 初始化对应每个Math.random()输出的64位浮点数变量
   r = [FP(f'r{i}', Float64()) for i in range(len(samples))]
   s = Solver()
   
   # 为每个样本添加范围约束
   for i, (min_val, max_val, result) in enumerate(samples):
       range_size = max_val - min_val + 1
       lower_bound = (result - min_val) / range_size
       upper_bound = (result - min_val + 1) / range_size
       # 将区间约束加入求解器
       s.add(r[i] >= FPVal(lower_bound, Float64()))
       s.add(r[i] < FPVal(upper_bound, Float64()))
   

4. 关联PRNG状态与约束
   脚本中XORSHIFT128+的状态转移逻辑无需修改，只需确保上述r数组的顺序和你调用RandomInt的顺序完全一致——每个r[i]对应PRNG连续输出的第i个值。

5. 运行求解并验证
   执行脚本后，Z3会尝试找到满足所有约束的PRNG状态。得到状态后，用XORSHIFT128+算法生成后续Math.random()输出，再代入RandomInt函数即可得到预测值。

注意事项 #

• 样本数量：一般7个不同范围的RandomInt输出即可唯一确定PRNG状态（范围越小，单个样本提供的约束越强，所需样本数越少）。
• 精度问题：使用Z3的Float64类型对应JS的双精度浮点数，计算上下界时用浮点数运算，避免整数除法导致的误差。

内容的提问来源于stack exchange，提问作者laut3n