擬似乱数の予測 ― rand() のシードを Z3 で逆算する

擬似乱数の予測 ― rand() のシードを Z3 で逆算する#

この章で学ぶこと#

疑似乱数は、見た目はランダムですが、生成の仕組みが分かっていれば先の値を予測できます。この章では Visual C++ の rand() を題材にします。

  • rand() は線形合同法（LCG）で作られている

  • 出力が数個分かれば、内部状態（シード）を Z3 で逆算できる

  • 逆算したシードから、次の値を予測する

BitVec（固定長のビット列）と URem（符号なしの剰余）が主役です。

線形合同法（LCG）#

線形合同法（Linear Congruential Generator, LCG）は、疑似乱数を作る方法の1つです。次の漸化式で次の状態を作ります。

\[ X_{n+1} = \left(A \times X_n + B\right) \bmod M \]

\(A\), \(B\), \(M\) は定数で、ふつう次の条件を満たします。

  • \(M > A\)

  • \(M > B\)

  • \(A > 0\)

  • \(B \geq 0\)

\(M = 2^{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;
}

やっていることは2つです。

  1. 内部状態 holdrand を更新する

\[ \text{holdrand} = (\text{holdrand} \times 214013 + 2531011) \bmod 2^{32} \]

  1. 上位16ビットを取り出し、0〜32767（0x7FFF）の整数として返す

出力は内部状態の一部だけです。だからこそ、出力から状態を逆算するのは「情報が足りるかどうか」の問題になります。

同じ動きをする 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 で、rand() % 100（0〜99）を8個作ります。9個目は答え合わせ用に取っておきます。

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() の計算をそのまま制約にします。

  1. states[0] は「シードを1回進めた状態」、states[1] はその次…と並べる

  2. 隣り合う状態は state_{i+1} = state_i * a + b（32ビットで巡回するので、掛け算のあふれは自動的に捨てられる）

  3. 各状態から取り出した出力 (state >> 16) & 0x7FFF を mod で割った余りが、観測した numbers と一致する

mod で割った余りしか分からないので、状態そのものは1つに決まらないことがあります。それでも「同じ数列を作るシード」は見つかります。

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個が並びました。予測成功です。

ただし、mod 100 で切り捨てているので、シードの候補は1つとは限りません。この問題では 1792 と 2147485440 の2つが条件を満たし、どちらでも同じ数列になります。出力の情報が少ないほど、候補は増えます。

応用：サイコロで6を10回出す#

rand() % 6 + 1 でサイコロを振るとき、「10回続けて6」になるシードを探してみます。

6を出すには rand() % 6 == 5 であればよいので、[5] * 10 を観測値として渡します。

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回目は条件に入れていないので、5 が続くとは限りません（この実行では 0 でした）。「11回連続で6」を狙うなら、[5] * 11 と11回分を条件にすればよいだけです。

また、条件を満たすシードは1つとは限らないので、実行するたびに別のシードが見つかることがあります。

BitVec と URem#

BitVec は、Z3 の固定長のビット列の型です。

  • BitVec('x', 32) は「32ビットの整数」として動く

  • 掛け算や足し算であふれたビットは捨てられる（C 言語の符号なし整数と同じ）

  • &, |, ^, >>, << などのビット演算が使える

URem(a, b) は符号なしの剰余（a % b）です。BitVec には符号がないので、% の代わりに URem() を使います。

rand() のコードは、この2つでそのまま書き写せます。

C のコード

Z3 の式

holdrand * 214013 + 2531011

prev * 214013 + 2531011

32ビットであふれた分を捨てる

BitVec の計算（自動）

holdrand >> 16

s >> 16

& 0x7FFF

& 0x7FFF

% mod

URem(..., mod)

まとめ#

  • 乱数の生成式が分かっていれば、出力から内部状態を逆算できる（BitVec に生成式をそのまま書く）

  • 出力が状態の一部だけなら、シードの候補は複数になりうる

  • 逆算したシードを使えば、次の値を予測できる

  • 「10回連続で6」のような条件も、観測値として渡すだけでシードを探索できる