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個観測することにより、後続の疑似乱数列が推測できていることが確認できる。