Z3Pyでglibc rand(3)の出力を推測してみる

Crypto

疑似乱数列は、いくつかの出力を観測することにより内部状態を復元することで推測が可能である。 ここでは、SMTソルバZ3Pyを使い、glibc rand(3)の出力を推測してみる。

環境

Ubuntu 14.04.3 LTS 64bit版、EGLIBC 2.19

$ 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

$ /lib/x86_64-linux-gnu/libc.so.6
GNU C Library (Ubuntu EGLIBC 2.19-0ubuntu6.6) stable release version 2.19, by Roland McGrath et al.

Z3Pyのインストール

Z3PyはMicrosoft Researchが開発したSMTソルバZ3のPythonバインディングである。 Z3Pyを使うには、まずZ3のReleasesページから最新のバイナリをダウンロードして展開する。

$ wget https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/z3-4.4.1-x64-ubuntu-14.04.zip
$ unzip z3-4.4.1-x64-ubuntu-14.04.zip
$ cd z3-4.4.1-x64-ubuntu-14.04/bin/

サンプルコードを実行してみる。

$ cat example.py
# Copyright (c) Microsoft Corporation 2015

from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print(s.check())
print(s.model())

$ python example.py
sat
[y = 4, x = 2]

上の結果から、制約を満たすx、yの組が一つ出力されていることがわかる。

rand(3)の実装を調べてみる

glibc（正確にはEGLIBC）におけるrand(3)に関連するコードのうち、主要な部分を抜き出すと次のようになる。

/* Return a random integer between 0 and RAND_MAX.  */
int
rand (void)
{
  return (int) __random ();
}
(snip)

/* x**31 + x**3 + 1.  */
#define TYPE_3      3
#define BREAK_3     128
#define DEG_3       31
#define SEP_3       3

(snip)

static int32_t randtbl[DEG_3 + 1] =
  {
    TYPE_3,

    -1726662223, 379960547, 1735697613, 1040273694, 1313901226,
    1627687941, -179304937, -2073333483, 1780058412, -1989503057,
    -615974602, 344556628, 939512070, -1249116260, 1507946756,
    -812545463, 154635395, 1388815473, -1926676823, 525320961,
    -1009028674, 968117788, -123449607, 1284210865, 435012392,
    -2017506339, -911064859, -370259173, 1132637927, 1398500161,
    -205601318,
  };


static struct random_data unsafe_state =
  {
/* FPTR and RPTR are two pointers into the state info, a front and a rear
   pointer.  These two pointers are always rand_sep places apart, as they
   cycle through the state information.  (Yes, this does mean we could get
   away with just one pointer, but the code for random is more efficient
   this way).  The pointers are left positioned as they would be from the call:
    initstate(1, randtbl, 128);
   (The position of the rear pointer, rptr, is really 0 (as explained above
   in the initialization of randtbl) because the state table pointer is set
   to point to randtbl[1] (as explained below).)  */

    .fptr = &randtbl[SEP_3 + 1],
    .rptr = &randtbl[1],

/* The following things are the pointer to the state information table,
   the type of the current generator, the degree of the current polynomial
   being used, and the separation between the two pointers.
   Note that for efficiency of random, we remember the first location of
   the state information, not the zeroth.  Hence it is valid to access
   state[-1], which is used to store the type of the R.N.G.
   Also, we remember the last location, since this is more efficient than
   indexing every time to find the address of the last element to see if
   the front and rear pointers have wrapped.  */

    .state = &randtbl[1],

    .rand_type = TYPE_3,
    .rand_deg = DEG_3,
    .rand_sep = SEP_3,

    .end_ptr = &randtbl[sizeof (randtbl) / sizeof (randtbl[0])]
};

long int
__random (void)
{
  int32_t retval;

  __libc_lock_lock (lock);

  (void) __random_r (&unsafe_state, &retval);

  __libc_lock_unlock (lock);

  return retval;
}
int
__random_r (buf, result)
     struct random_data *buf;
     int32_t *result;
{
  int32_t *state;

  if (buf == NULL || result == NULL)
    goto fail;

  state = buf->state;

  if (buf->rand_type == TYPE_0)
    {
      int32_t val = state[0];
      val = ((state[0] * 1103515245) + 12345) & 0x7fffffff;
      state[0] = val;
      *result = val;
    }
  else
    {
      int32_t *fptr = buf->fptr;
      int32_t *rptr = buf->rptr;
      int32_t *end_ptr = buf->end_ptr;
      int32_t val;

      val = *fptr += *rptr;
      /* Chucking least random bit.  */
      *result = (val >> 1) & 0x7fffffff;
      ++fptr;
      if (fptr >= end_ptr)
    {
      fptr = state;
      ++rptr;
    }
      else
    {
      ++rptr;
      if (rptr >= end_ptr)
        rptr = state;
    }
      buf->fptr = fptr;
      buf->rptr = rptr;
    }
  return 0;

 fail:
  __set_errno (EINVAL);
  return -1;
}

上の内容から、rand(3)は内部的にrandom(3)を使っていることがわかる。 random(3)は標準でTYPE_3で動作し、内部状態として31個の32bit整数（int32_t）を持つ。 また、出力される値は内部状態の値の下位1ビットを右シフトにより捨てたものとなっている。

rand(3)の出力を推測してみる

rand(3)の実装に基づき、いくつかの出力から内部状態を復元し、後続の乱数列を推測してみる。

まず、疑似乱数列を出力するC言語コードを用意する。

/* randgen.c */
#include <stdio.h>
#include <stdlib.h>
#include <time.h>

int main()
{
    srand(time(NULL));
    while (1) {
        printf("%d\n", rand());
    }
}

Z3Pyを使い、93個（内部状態数×3）の出力から内部状態を復元するスクリプトを書くと次のようになる。 ここで、内部状態数の3倍の出力を使うのは、捨てられた下位1ビットの組として00、01、11の3パターンがありえるためである。

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

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

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

for i in xrange(93):
    state[(3+i) % 31] += state[i % 31]
    output = (state[(3+i) % 31] >> 1) & 0x7fffffff
    actual = int(p.stdout.readline())
    s.add(output == actual)

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

for i in xrange(93, 93+31):
    state[(3+i) % 31] += state[i % 31]
    output = m.evaluate((state[(3+i) % 31] >> 1) & 0x7fffffff)
    actual = int(p.stdout.readline())
    print output, actual, m.evaluate(output == actual)

p.terminate()

実際に実行してみると次のようになる。

$ gcc randgen.c -o randgen

$ python predict.py
1539474640 1539474640 True
1744805117 1744805117 True
769627106 769627106 True
686469934 686469934 True
1300759149 1300759149 True
1946964639 1946964639 True
832211969 832211969 True
1160214192 1160214192 True
1036560838 1036560838 True
388213498 388213498 True
372849012 372849012 True
1030306283 1030306283 True
1889902623 1889902623 True
1661141766 1661141766 True
291669262 291669262 True
811132721 811132721 True
1408205630 1408205630 True
1271197160 1271197160 True
1919090387 1919090387 True
664892816 664892816 True
1466540625 1466540625 True
433264183 433264183 True
171891431 171891431 True
480533914 480533914 True
662509870 662509870 True
2125134586 2125134586 True
279987208 279987208 True
1951967228 1951967228 True
1181304332 1181304332 True
121929249 121929249 True
916132829 916132829 True

$ python predict.py
343473243 343473243 True
281526738 281526738 True
1943222783 1943222783 True
608829054 608829054 True
1390625565 1390625565 True
266302862 266302862 True
1215290211 1215290211 True
1521157852 1521157852 True
1371756071 1371756071 True
1855803104 1855803104 True
2122934828 2122934828 True
2025557163 2025557163 True
153275759 153275759 True
907581179 907581179 True
1420550946 1420550946 True
1180862840 1180862840 True
1459580178 1459580178 True
1856504581 1856504581 True
1129491927 1129491927 True
739379874 739379874 True
1762455194 1762455194 True
478009561 478009561 True
1906949940 1906949940 True
1419743025 1419743025 True
267136936 267136936 True
1186839526 1186839526 True
38496104 38496104 True
2062317532 2062317532 True
84709225 84709225 True
240334224 240334224 True
329038695 329038695 True

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

関連リンク