Z3 Solver で擬似乱数の内部状態を復元する＋α

はじめに

擬似乱数の出力列から内部状態を復元することができれば、未来予測が可能になります。以前の記事でその一部を紹介しましたが、その構造についてよく理解して解析する必要があるなど、手間がかかっていました。ここでは、ツールを使っていい感じに問題を解いてもらう方法について紹介します。

Z3 Solver

Z3 は、Microsoft Research が開発している SMT ソルバです。私もふんわり使用しているだけなので適当に説明すると、関係式をいくつか投入すると、それらの式が成立するか、もし成立するなら値が何のときか、といったことを求めてくれるプログラムです。例えば、

* x, y は自然数
* x + y == 5
* x >= 3

をすべて満たす x, y は存在するか?

に対して、

(x = 3, y = 2) のとき成立する

といった感じで答えが返ってきます。

様々な言語に対応しており、Readme 曰く python, C++, C#, Java などで使えます。

C# での利用

NuGet で Microsoft.Z3.x64 をインストールすれば使えるようになります。

実装例を以下に示します。これは上に挙げた例を実際にコード化したものです。

using (var context = new Context())
using (var solver = context.MkSolver())
{
    // 変数 x, y を定義
    var x = context.MkIntConst("x");
    var y = context.MkIntConst("y");

    // 関係式 x + y == 5 を追加
    solver.Assert(context.MkEq(context.MkAdd(x, y), context.MkInt(5)));

    // 関係式 x >= 3 を追加
    solver.Assert(context.MkGe(x, context.MkInt(3)));


    // 式が成立するかを調べて、成立すればそれを出力
    var issat = solver.Check();
    Console.WriteLine(issat);

    if (issat == Status.SATISFIABLE)
    {
        Console.WriteLine(solver.Model);
    }

}

実行すると以下の出力を得ました。計算できていることが分かります。

SATISFIABLE
(define-fun y () Int
  2)
(define-fun x () Int
  3)

なお、解が複数あったとしてもそのうちのどれか一つが得られます。今回で言えば (x = 4, y = 1) も条件を満たしますが、こちらは得られるとは限りません。
また、どうやっても成立しない場合は UNSATISFIABLE が得られます。

記述がつらい

上の例を見れば分かると思いますが、Z3 では関係式の記述はすべてメソッド context.Mk***() を通して行います。とてもつらいので、普通の式と同じように演算子を使って書きたくなります。ということで、ちょっとしたラッパー RngSolver を実装しました。 RngSolver と書いてはいますが、乱数用途以外にも使えるかもです。

https://github.com/andanteyk/RngSolver

詳しくは SolveRng.cs を参照してください。

実用例

xoshiro256+ の内部状態復元

上述した RngSolver の SolveRng.cs をちょっといじって、 xoshiro256+ の内部状態復元を試みます。解説コメントも適当に付け足しました。

public static void Solve()
{
    // seed: 適当なシード値(正解)
    var seed = new ulong[] { 0x0123456789abcdef, 0xfedcba9876543210, (ulong)Environment.TickCount, (ulong)DateTime.Now.Ticks }
        .Select(s => new Arithmetic(s)).ToArray();

    // outputs: 観測された出力
    // 今回は検証目的なのでシードから実際に出力させて outpus を設定していますが、
    // 実際に観測から復元するときは outputs に直接突っ込みます
    var outputs = new Arithmetic[seed.Length + 1];
    {
        var clone = seed.Select(s => s.Identity()).ToArray();
        for (int i = 0; i < outputs.Length; i++)
            outputs[i] = Next(clone) as Arithmetic;
    }


    Console.WriteLine($"start: {DateTime.Now:yyyy/MM/dd HH:mm:ss.fff}");

    using (var context = new Context())
    using (var solver = context.MkSolver())
    {
        // state を変数として宣言
        var state = Enumerable.Range(0, seed.Length).Select(i => new BitVecWrapper(context.MkBVConst("state" + i, 64), context)).ToArray();

        // 「出力列 [Next(state), ...] が outputs と等しい」制約を設定
        for (int i = 0; i < outputs.Length; i++)
        {
            var res = Next(state);
            solver.Assert(res.Equals(outputs[i]) as BoolExpr);
        }


        // したがって、outputs と同じ出力を生成する内部状態 state が得られる（かも）
        var issat = solver.Check();
        Console.WriteLine(issat);

        if (issat == Status.SATISFIABLE)
        {
            Console.WriteLine(solver.Model);
        }

    }

    Console.WriteLine($"end  : {DateTime.Now:yyyy/MM/dd HH:mm:ss.fff}");
}

// RngSolver を使うと、以下のように関係式定義が簡潔に行え、 Mk***() 地獄を回避できます 
// ついでに ulong と BitVecExpr の計算を 1 つの定義で行えます
// このメソッドを書き換えれば別の乱数の出力推測ができます
public static IArithmetic Next(IArithmetic[] s)
{
    var result = (s[0] + s[3]);

    var t = s[1] << 17;

    s[2] ^= s[0];
    s[3] ^= s[1];
    s[1] ^= s[2];
    s[0] ^= s[3];

    s[2] ^= t;

    s[3] = s[3].Rol(45);

    return result;
}

実行すると以下が得られました。40 秒程度で、連続した 64 bit の出力 x 5 から内部状態を復元することができました。

start: 2020/12/05 00:18:56.258
SATISFIABLE
(define-fun state3 () (_ BitVec 64)
  #x08d898b35ac76c8c)
(define-fun state1 () (_ BitVec 64)
  #xfedcba9876543210)
(define-fun state0 () (_ BitVec 64)
  #x0123456789abcdef)
(define-fun state2 () (_ BitVec 64)
  #x00000000465512c4)
end  : 2020/12/05 00:19:32.102

ちなみになのですが、 xoshiro256+ は出力関数に + を用いて非線形な出力を行っています。 *1 そのため、生で吐き出す Xorshift や出力関数が線形な MT19937 に対して有効な「行列計算を用いた内部状態復元」が適用できず、私が知る限りでは solver 利用が最速の手法となっています。

なお、復元できるかどうかは遷移関数や出力関数の複雑さに依存します。関数によっては n 時間かかったり、 n 日かかっても結果が出なかったりします。

`x << 2 ^ x >> 19` の可逆性

以前話に出した、 long x; x << 2 ^ x >> 19 (>> は右算術シフトです) が逆算可能かどうか＝可逆であるかを調べたいとします。厳密には数学的に証明する必要がありますが、今回はソルバーでざっくり調べます。

全ての x に対して逆算可能である、と示すのは大変なので、逆算ができない x が存在しないことを求める方針で実装します。例えば異なる a, b を入力として同じ結果 z が得られた場合、逆算 inv(z) の値が a, b の "どちらか" になってしまいただ一つに決定できなくなります。したがって、そのような a, b が存在すれば逆算不可能、存在しなければ逆算可能であるといえるでしょう。前の項とは逆に、成立不可能 UNSATISFIABLE であれば嬉しいわけです。

それをコードに落とし込んだのが Invertible.cs です。ちょっと改造・補足説明して、以下に示します。

public static void IsInvertible()
{
    Console.WriteLine($"start: {DateTime.Now:yyyy/MM/dd HH:mm:ss.fff}");

    using (var context = new Context())
    using (var solver = context.MkSolver())
    {
        // 上の説明で言う a, b を定義
        var state = Enumerable.Range(0, 2).Select(i => new BitVecWrapper(context.MkBVConst("state" + i, 64), context)).ToArray();

        // (a != b) かつ (f(a) == f(b)) を満たす (a, b) ？
        solver.Assert(state[0].NotEquals(state[1]) as BoolExpr);
        solver.Assert(Output(state[0]).Equals(Output(state[1])) as BoolExpr);


        // 成立しなければ逆算可能、成立すれば逆算不可能
        var issat = solver.Check();
        Console.WriteLine(issat);

        if (issat == Status.SATISFIABLE)
        {
            Console.WriteLine(solver.Model);
        }

    }

    Console.WriteLine($"end  : {DateTime.Now:yyyy/MM/dd HH:mm:ss.fff}");
}

// x << 2 ^ x >> 19
public static IArithmetic Output(IArithmetic s)
{
    return s << 2 ^ s.Sar(19);
}

これは速やかに UNSATISFIABLE を得ます。したがって、全ての入力に対して逆算ができることが示されました。（しかしここでは具体的な逆算方法は得られません。自分の目で確かめてみてください。）

start: 2020/12/05 00:51:00.302
UNSATISFIABLE
end  : 2020/12/05 00:51:00.382

では、 x << 6 ^ x >> 19 はどうでしょうか。末尾の Output を書き換えて実行してみると…

start: 2020/12/05 00:53:05.689
SATISFIABLE
(define-fun state1 () (_ BitVec 64)
  #x4b206621b61e1a1b)
(define-fun state0 () (_ BitVec 64)
  #x4f206623b61e1b1b)
end  : 2020/12/05 00:53:05.778

SATISFIABLE を得ます。いわば「反例を得た」状態であり、入力を 0x4f206623b61e1b1b および 0x4b206621b61e1a1b とした場合の出力が一致するため、逆算ができない場合があることが示されました。実際に計算すると同一の出力 0xc81981098b42b003 が得られます。

ついでに x << a ^ x >> b は全ての a, b において常に逆算できるわけではないことも分かりました。