预测伪随机数：用 Z3 反算 rand() 的种子#
本章的内容#
伪随机数看上去是随机的，但只要知道它的生成方式，就可以预测后面的值，本章以 Visual C++ 的 rand() 为例。
rand()由线性同余法生成，即 LCG只要知道几个输出，就可以用 Z3 反算出内部状态，即种子
从反算出的种子出发，预测下一个值
BitVec 即固定长度的位向量，与 URem 即无符号取余，是本章用到的两个工具。
线性同余法#
线性同余法是生成伪随机数的一种方法，用下面的递推式产生下一个状态。
\(A\)、\(B\)、\(M\) 是常数，通常满足下面的条件。这四条是常数取值的最低要求；周期能有多长，还取决于几个常数之间的配合。
\(M > A\)
\(M > B\)
\(A > 0\)
\(B \geq 0\)
若 \(M = 2^{32}\)，这个式子就相当于 32 位整数的乘法与加法之后，丢掉溢出的部分。这一步在 32 位机器上不需要额外的代码。
Visual C++ 的 rand()#
Visual C++ 的 rand() 使用线性同余法，源代码如下。
static long holdrand = 1L;
int __cdecl rand(void)
{
return (((holdrand = holdrand * 214013L + 2531011L) >> 16) & 0x7FFF);
}
void __cdecl srand(unsigned int seed)
{
holdrand = (long)seed;
}
这段代码只做两件事，下面分别说明。第二件事决定输出的位数，也决定反算的难度。
更新内部状态
holdrand
取出高 16 位，作为 0〜32767 的整数返回，上限就是
0x7FFF
输出只是内部状态的一部分，因此从输出反算状态，本质上是一个信息是否够用的问题，而不是纯数学上的技巧。每次输出只给出 15 位，32 位状态剩下的部分要靠后续输出逐步补齐。也正因如此，rand() 不适合作加密用途：输出量太少，状态容易被还原。
下面准备一个行为与 rand() 相同的 Python 类。
class PseudoRandom:
"""和 Visual C++ 的 rand() 行为相同的伪随机数"""
def __init__(self, seed=1):
self._holdrand = seed
def srand(self, seed: int):
self._holdrand = seed
def rand(self) -> int:
self._holdrand = (self._holdrand * 214013 + 2531011) & 0xFFFFFFFF
return (self._holdrand >> 16) & 0x7FFF
生成 8 个随机数#
取种子 1792，生成 8 个 rand() % 100，即 0〜99 的整数，第 9 个留作验证用。取余 100 是为了模拟只看到部分信息的情形。
rand = PseudoRandom(1792)
numbers = [rand.rand() % 100 for _ in range(8)]
print(numbers)
print(rand.rand() % 100)
[90, 79, 97, 7, 20, 77, 17, 89]
16
用 Z3 反算种子#
下面只用 numbers 中的 8 个值，推断第 9 个值。
内部状态是 32 位的，因此用一个 BitVec('seed', 32) 变量来表示，再把 rand() 的计算原样写成约束。
states[0]是种子推进一次之后的状态，states[1]是再下一次，依此类推相邻的状态满足
state_{i+1} = state_i * a + b，32 位会自然回绕，乘法溢出被自动丢掉由各状态取出的输出
(state >> 16) & 0x7FFF除以mod的余数，与观察到的numbers相等
由于只知道除以 mod 的余数，状态本身未必能唯一确定，但能产生同一数列的种子总能找到，只是未必只有一个。余数丢掉的信息越多，候选种子就越多。
from z3 import *
def find_seed_and_next(numbers, mod, a=214013, b=2531011):
"""从观测到的输出序列，求出种子和下一个输出"""
seed = BitVec('seed', 32)
states = [BitVec(f's_{i}', 32) for i in range(len(numbers) + 1)]
outputs = [URem((s >> 16) & 0x7FFF, mod) for s in states]
solver = Solver()
# 1. 状态的转移（LCG）
for prev, cur in zip([seed] + states[:-1], states):
solver.add(prev * a + b == cur)
# 2. 和观测到的输出一致
for out, observed in zip(outputs, numbers):
solver.add(out == observed)
if solver.check() != sat:
return None
model = solver.model()
return model[seed].as_long(), model.eval(outputs[-1]).as_long()
seed_val, next_val = find_seed_and_next(numbers, mod=100)
print(f'seed = {seed_val}')
print(f'next = {next_val}')
seed = 1792
next = 16
原来的种子 1792 被找了出来，下一个值也预测为 16，而实际的第 9 个值同样是 16，与上面单元格的输出对照即可。
下面用找到的种子重新生成一次随机数列，确认两次的结果是否一致。
rand = PseudoRandom(seed_val)
[rand.rand() % 100 for _ in range(9)]
[90, 79, 97, 7, 20, 77, 17, 89, 16]
完全相同的 9 个数列了出来，预测成功。这个问题的解是 1792 与 2147485440 两个，两者都能产生同一数列，区别只在不影响输出的高位上，输出无法区分它们。
应用：用骰子连续掷出 10 个 6#
用 rand() % 6 + 1 掷骰子时，本节来寻找能连续掷出 10 个 6 的种子，而要得到 6，只需 rand() % 6 == 5，因此把 [5] * 10 作为观察值传入。这与反算种子是同一个框架：把观察到的结果写成约束，让 Z3 去找满足它的种子。
seed_val, next_val = find_seed_and_next([5] * 10, mod=6)
print(seed_val)
rand = PseudoRandom(seed_val)
[rand.rand() % 6 for _ in range(11)]
3689596556
[5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 0]
连续 10 次得到 5、也就是骰子掷出 6 的种子被找到了，不过条件里只写入了最初 10 次，第 11 次并未写入，因此第 11 次的输出未必还会是 5，这次运行得到的是 0。若要让 11 次连续都出 6，把 [5] * 11 作为条件即可；另外，满足条件的种子并不只有一个，每次运行都可能找到不同的种子。
BitVec 与 URem#
BitVec 是 Z3 中固定长度位向量的类型。
BitVec('x', 32)按 32 位整数的方式工作乘法与加法溢出的高位会被丢掉，与 C 语言的符号无关；位向量的长度决定模数，32 位就等价于对 \(2^{32}\) 取模
可以使用
&、|、^、>>、<<等位运算
URem(a, b) 是无符号取余，即 a % b。BitVec 没有符号，因此取余要用 URem() 而不用 %。
把 rand() 的代码原样照抄过来，只需要这两个工具。C 里的类型转换与符号处理在这里都不需要，位向量的长度已经固定。
C 的代码 |
Z3 的表达式 |
|---|---|
|
|
丢掉 32 位溢出的部分 |
|
|
|
|
|
|
|
小结#
只要知道随机数的生成式，就可以从输出反算内部状态，把生成式直接写成
BitVec即可输出只是状态的一部分时，种子的候选可能不止一个
用反算出的种子就能预测下一个值
像连续 10 次出 6 这样的条件，也只要作为观察值传入，就能搜索种子