擬似乱数列の予測

擬似乱数列の予測#

疑似乱数は一見ランダムに見えますが、生成アルゴリズムが分かっていれば、その内部状態を推測し、次の値を予測することが可能です。本章では、線形合同法（LCG）を用いた乱数生成の仕組みを解析し、Z3 を用いてシードを逆算し、次に生成される乱数を予測する方法を紹介します。さらに、特定の出力パターンを満たすシードの探索についても考察します。

線形合同法#

線形合同法（Linear Congruential Generator, LCG）は、擬似乱数を生成する手法の一つです。その生成規則は、以下の漸化式で表されます。

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

ここで、\( A \)、\( B \)、\( M \) は定数であり、通常以下の条件を満たします。

  • \( M > A \)

  • \( M > B \)

  • \( A > 0 \)

  • \( B \geq 0 \)

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;
}

この rand() 関数は、内部状態 holdrand を次の式に基づいて更新し、上位16ビットを抽出して 0 から 32767 (0x7FFF) の範囲の整数を返します。

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

次に、同様の動作を Python で模倣するクラス PseudoRandom を示します。

class PseudoRandom:
    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  # 32bitで維持
        return (self._holdrand >> 16) & 0x7FFF

この PseudoRandom クラスを用いて、100 以下の整数を 8 個生成し numbers に格納し、さらに 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

乱数列の予測#

numbers に格納された 8 個の乱数をもとに、9 個目の乱数を予測することは可能でしょうか？ ここでは、Z3 を用いて rand() の内部状態（シード）を逆算し、次の乱数を求める方法を紹介します。

以下の Python コードでは、既知の乱数列 numbers を与えると、対応するシード (seed_val) を求め、さらに次に生成される乱数 (next_val) を予測します。

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()
    
    for sp, sv in zip([seed] + states[:-1], states):
        solver.add(sp * a + b == sv)
    
    for o, n in zip(outputs, numbers):
        solver.add(o == n)
    
    solver.check()
    model = solver.model()
    seed_val = model[seed].as_long()
    next_val = model.eval(outputs[-1]).as_long()
    return seed_val, next_val

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

ここで求めた seed_val は、元の 1792 とは異なる可能性がありますが、このシードを用いることで同じ乱数列を再現できます。

rand = PseudoRandom(seed_val)
[rand.rand() % 100 for _ in range(9)]

[90, 79, 97, 7, 20, 77, 17, 89, 16]

次に、rand() % 6 + 1 でサイコロを模擬する場合、連続 10 回 6 を出力できるシードを探索します。この場合、rand() % 6 の出力が 5 である必要があります（5 + 1 = 6 になるため）。次のコードを実行すると、連続 10 回 6 を出すことができるシード seed_val が求められます。

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)]

1522212766

[5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 2]

コードの説明#

BitVec は、Z3 で固定長のビットベクトルを扱うためのデータ型です。整数や論理式の制約を解く際に BitVec を用いることで、「ビット単位の演算」や「オーバーフローを考慮した計算」を行うことができます。

BitVec 変数は、通常の整数型とは異なり、固定長のビット列として扱われます。例えば、BitVec('x', 32) は32ビット整数のように動作します。BitVec 変数は Python のビット演算子を使用して、AND、OR、XOR、シフトなどのビット演算を行うことができます。また、オーバーフローの影響を正確にシミュレーションすることも可能です。

一方、URem は「Unsigned Remainder（符号なし剰余）」の略で、ビットベクトルに対する剰余演算（%）を行う Z3 の関数です。これは、BitVec 型の変数に対して剰余を求める際に使用され、符号なし整数として演算が処理されるという特徴があります。

このコードでは、まず、N+1 個の状態を表す BitVec 型の変数リスト statesを作成します。

1. states の作成

states = [BitVec(f's_{i}', 32) for i in range(len(numbers) + 1)]

ここで、各 states[i] は、線形合同法（LCG）に基づく疑似乱数生成器の内部状態を表します。

2. rand() の出力を計算

outputs = [URem((s >> 16) & 0x7FFF, mod) for s in states]

このコードでは、各 states[i] から rand() の出力 (state >> 16) & 0x7FFF を計算し、それを mod で割った剰余を outputs に格納しています。 この処理により、実際の rand() 関数と同じ出力が得られるように制約を設定することができます。

3. 状態遷移の制約を追加

前後の states の関係が、線形合同法（LCG）の漸化式に従うように制約を設定します。

for sp, sv in zip([seed] + states[:-1], states):
    solver.add(sp * a + b == sv)

ここで、sp は前の状態、sv は次の状態を表し、sp * a + b == sv という条件を追加することで、すべての states が線形合同法の式を満たすように制約を課しています。

Contents