Z3Pyでxorshift128+の出力を推測してみる

「Z3Pyでglibc rand(3)の出力を推測してみる」では、glibc rand(3)の出力をいくつか観測することで、後続の出力を推測した。 ここでは、V8 JavaScript Engineなどで使われている疑似乱数生成アルゴリズムxorshift128+の出力を推測してみる。

環境

Ubuntu 14.04.3 LTS 64bit版

$ uname -a
Linux vm-ubuntu64 3.19.0-25-generic #26~14.04.1-Ubuntu SMP Fri Jul 24 21:16:20 UTC 2015 x86_64 x86_64 x86_64 GNU/Linux

$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 14.04.3 LTS
Release:        14.04
Codename:       trusty

$ gcc --version
gcc (Ubuntu 4.8.4-2ubuntu1~14.04) 4.8.4

xorshift128+を実装してみる

xorshift128+は高速かつ高性能な疑似乱数生成アルゴリズムである。 次の論文を参考に、xorshift128+を使って疑似乱数を生成するプログラムコードを書くと次のようになる。

/* xorshift128plus.c */
#include <stdio.h>
#include <stdint.h>

uint64_t s[2] = {1,2};

uint64_t next(void) {
    uint64_t s1 = s[0];
    const uint64_t s0 = s[1];
    s[0] = s0;
    s1 ^= s1 << 23; // a
    s[1] = s1 ^ s0 ^ (s1 >> 18) ^ (s0 >> 5); // b, c
    return s[1] + s0;
}

int main()
{
    while (1) {
        printf("%lu\n", next());
    }
}

上の内容から、xorshift128+は2個の64bit整数(uint64_t型)を内部状態として持つことがわかる。

上のコードをコンパイルして実行すると次のようになる。

$ gcc xorshift128plus.c -o xorshift128plus

$ ./xorshift128plus | head
8388645
33816707
70368778527840
211106267172129
281552312399723
352084508939685
648800200157934532
2540241598295339419
2648407162339308712
2668752799858137237

xorshift128+の出力を推測してみる

「Z3Pyでglibc rand(3)の出力を推測してみる」と同様に、Z3Pyを用いてxorshift128+の出力を推測するスクリプトを書くと次のようになる。

# predict_xorshift128plus.py
from z3 import *
from subprocess import Popen, PIPE

p = Popen(['./xorshift128plus'], stdout=PIPE)

state = [BitVec("state%d" % i, 64) for i in xrange(2)]
s = Solver()

for i in xrange(2):
    s1 = state[0]
    s0 = state[1]
    state[0] = s0
    s1 ^= s1 << 23;
    state[1] = s1 ^ s0 ^ LShR(s1, 18) ^ LShR(s0, 5);
    output = state[1] + s0
    actual = int(p.stdout.readline())
    s.add(output == actual)

s.check()
m = s.model()

for i in xrange(2, 2+64):
    s1 = state[0]
    s0 = state[1]
    state[0] = s0
    s1 ^= s1 << 23;
    state[1] = s1 ^ s0 ^ LShR(s1, 18) ^ LShR(s0, 5);
    output = m.evaluate(state[1] + s0)
    actual = int(p.stdout.readline())
    print output, actual, m.evaluate(output == actual)

p.terminate()

Z3Pyにおいて、LShR関数はunsigned型に対する右シフト(いわゆる論理右シフト)を表す。 また、xorshift128+の内部状態数は2個のため、推測するために必要な観測数は2である。

上のスクリプトを実行してみる。

$ python predict_xorshift128plus.py
70368778527840 70368778527840 True
211106267172129 211106267172129 True
281552312399723 281552312399723 True
352084508939685 352084508939685 True
648800200157934532 648800200157934532 True
2540241598295339419 2540241598295339419 True
2648407162339308712 2648407162339308712 True
2668752799858137237 2668752799858137237 True
2693699070923777171 2693699070923777171 True
4963962142036894822 4963962142036894822 True
11906738374415673757 11906738374415673757 True
9632391838565739090 9632391838565739090 True
2066554175270807792 2066554175270807792 True
2494022894752328945 2494022894752328945 True
1356498747469623086 1356498747469623086 True
11211414770921777427 11211414770921777427 True
10429009827004399351 10429009827004399351 True
2323958476090753392 2323958476090753392 True
3568022355029630745 3568022355029630745 True
66653323867787511 66653323867787511 True
2202670577644624798 2202670577644624798 True
12857773250674142713 12857773250674142713 True
4201717447333134628 4201717447333134628 True
15638699059651815979 15638699059651815979 True
4364251867564744889 4364251867564744889 True
7660026492187243788 7660026492187243788 True
3800851612386782149 3800851612386782149 True
9605385339319476694 9605385339319476694 True
2406190703679268226 2406190703679268226 True
846469172938628641 846469172938628641 True
5337113899023465296 5337113899023465296 True
15781852488115071549 15781852488115071549 True
15354462637857246627 15354462637857246627 True
11103786004116532909 11103786004116532909 True
10104343325409002424 10104343325409002424 True
12295544783831320534 12295544783831320534 True
9091324406814034890 9091324406814034890 True
6628842478985115447 6628842478985115447 True
12899089858988772368 12899089858988772368 True
16555193421103270775 16555193421103270775 True
5182223508147526313 5182223508147526313 True
1789523054416386623 1789523054416386623 True
8305247958687497212 8305247958687497212 True
4332901280696262112 4332901280696262112 True
4830599505179982300 4830599505179982300 True
16562699778378001540 16562699778378001540 True
4301002138587088699 4301002138587088699 True
16887648884050224867 16887648884050224867 True
8961088417938801842 8961088417938801842 True
18120357346625319699 18120357346625319699 True
5062957422512203146 5062957422512203146 True
14533691471387576319 14533691471387576319 True
17893283120539033726 17893283120539033726 True
8933729491225170482 8933729491225170482 True
7703252517382402300 7703252517382402300 True
4527677543428710360 4527677543428710360 True
11852647525519638421 11852647525519638421 True
14323485818621793660 14323485818621793660 True
1603981125980772416 1603981125980772416 True
10667357879029765177 10667357879029765177 True
12618821681808242380 12618821681808242380 True
15688459637854892994 15688459637854892994 True
16858336139413885781 16858336139413885781 True
8192223518607711332 8192223518607711332 True

実行結果より、xorshift128+の出力を2個観測することにより、後続の疑似乱数列が推測できていることが確認できる。

関連リンク