SMT Solver無しでXorshift128+を解く
先週のCBCTFではXorshift128+の32個の出力列が与えられた場合にその先を予測させる問題が出題された（Random RSA）。
想定解はSMT Solverを使うのだが、宗教上の理由で使えない人が居るかもしれないため別の解法を考えた。
なお、先に言っておくとこの解法は多大なリソースを必要とし、具体的にはメモリを200GBほど使用する。研究室の500万円の計算機で64Thread立てて計算しても30分ほど掛かった。要するにz3を使え、その辺のパソコンで10秒で解ける。
Xorshift128+とは
while True: s1 = s[0] s0 = s[1] s[0] = s0 s1 ^= (s1 << 23) & ((1<<64) - 1) s[1] = s1 ^ s0 ^ (s1 >> 18) ^ (s0 >> 5) yield (s[1] + s0) & ((1<<64) - 1)
Xorshiftとは主にxor, bitshiftで構成された軽量な乱数生成器である。Xorshift系の乱数生成器には様々なバリエーションが有り、その中の1つであるXorshift128+はadditionを加えることで線形性を除いている（後述）。なお、128とは状態数が128bitなことに起因すると思われる（もしかしたら周期かも？）。
Xorshift128+の難しさ
もしこの出題が普通のXorshift128であったなら簡単に解くことが出来る。
何故なら、Xorshift128に使われる処理はxorと固定長bitshiftだけであり、これらは共に状態bitをGF(2)上のベクトルと見なせば線形性を持つ。つまり、全ての演算が行列で書き表せる為に逆行列を作ることで簡単に初期状態を復元できる。
しかし、Xorshift128+の出力列は最後に加算される。この処理は線形性を持たない。この簡単な処理を付け加えるだけで問題は飛躍的に難しくなる。
Xorshift128+の線形性
しかし、Xorshift128+であっても線形性を持つ箇所がある。LSB（最下位bit）である。
LSBは下の桁が無いため、繰り上がりを気にしなくても良い。その為32個の出力列から32個の線形方程式を得ることが出来る。もう少し考察すると、注目するbitより下位が全て1である場合も繰り上がりを気にしなくてもよく、N個の出力列からおよそN/2個の方程式を得ることが出来る。
Random RSAでは新たに28個の線形方程式を得て、60個の方程式が集った。
行列に対するMITM
60個の方程式を集めたということは、128bit中60bitがleakしたと考えることが出来る。しかしまだ68bitの総当りが残る。
これを何とかしてMITMで計算量を落とせないか考えた。ここからの説明はかなり雑なので分かる人しか分からないと思う（真面目に行列の式書くのがめんどい……）。
ここから内部状態を64bitずつのx, yと表すことにする。
今60個しか式が集まっていないが、適当に4bit固定することにより64個の線形独立な式を得る。この行列を変形し、[E | M]のように左半分を単位行列とする行列を得る。これにより、xとyの関係を線形方程式で記述出来る（x + My = 64次ベクトル）。
ここで1つ目の出力列により、yを定めればxが定まる。また、先述の線形方程式からもyを定めればxが定まり、これらが一致すれば解となる。
ここでyを上位32bitと下位32bitに分割する（y1, y2）。そうすると先の線形方程式はx + M1y1 + M2y2 = 64次ベクトル という様な式に変形できる（y1, y2を定めるとxはそれぞれ繰り上がりの有無を無視すれば一意に定まることに注意）。以上から、M1'y1 + M2'y2 = 64次ベクトル という式を得る。
これは、M1'y1 - 64次ベクトル とM2'y2をそれぞれ独立に計算し、一致する場合を探せば良い。
これを実装すると64個の解が出てきた。これは最初に足りない4bitを定めた分と無視した繰り上がりの2bitで6bitの自由度を持った為だと考えられる。あとは全て試すと正しい解を得た。
enumulating all y1 merging vectors miv1: 8589934592 enumulating all y2 merging vectors miv2: 4294967296 serching 2476520362 61509141 2157264084 3353016742 656009753 1860619162 2574392452 2567461328 3446121306 463614785 3288533184 2667169677 3065249141 186478286 769889559 1500841788 540840065 3086893980 1799405833 2135579198 954749789 548963819 3960811688 2581296186 3103250995 4048812002 2904438575 287535986 1008273453 742342059 1609709208 525912563 102537622 2128507249 2446164013 1093192679 2075536625 1789293171 1195834711 2725839867 295618493 3554538105 2373988069 3548126869 1347207931 483994859 1071373495 101210017 193547184 2191692163 1021151311 519290032 1916084563 544594116 2047105320 318595631 66506444 2834209036 1251206337 3094191279 4186820173 2782881948 2114031298 3190589275 508037032 453555974 745063296 2750048806 2923802844 1177402636 2832440853 273566763 1518323354 358834199 1122617837 2403936068 1091218555 4018685749 4136247442 294350163 2928405395 1799492342 2197082799 759383716 4077570164 1016706399 3093126019 3118276782 2943083703 1649561999 3404147677 124557829 716115770 275919643 2901710221 4203208796 657711912 331906217 2690332004 2083220237 433830677 896965898 1296534180 1664930400 1977485902 3742108858 3115534102 689202550 1477097847 3976949959 378126705 2382484743 2943110840 288054401 3860062577 4057827336 1338808793 100592408 133487806 3607172407 2616266322 477564116 3764152924 916057340 1307750470 153169944 1629761026 657825298 829409657 396404147 3151417975 3300223157 2494409012 3774521208 3045576677 1401251776 1775617714 3515828845
y1, y2 = 508037032, 453555974が答え。
実装
64Threadで実行して30分くらいだった。
GF(2)上であれば行列積がandとbitcountになることを使って高速化したりしたがまだまだ重い。ソート列のマージをシングルスレッドで行っているのがボトルネックで、頑張れば10分を切るくらいにはなると思う。メモリも工夫すれば60GB程度には減らせそう。最初はy2の列だけ生成して各y1で二分探索していたのだけど期待よりかなり重くなった。研究室マシンが1.5TBのメモリを持っていたので雑に両方持ってやったほうが速いようだ。
あと普段競プロで並列化やメモリキャッシュやらに気を配ることが殆ど無いのでこのあたりのノウハウが皆無なことに気がついた。悲しい。
