TL;DR

  • Goの乱数生成器(math/randによって生成された数でフラグをXORした結果とその後の出力607個(但し連続しない)が与えられる
  • フラグとのXORに使った乱数は直後の状態に存在するので607個の乱数から直前の状態をz3で復元する

Prerequisite

  • z3

Writeup

次のGoのソースコードとその出力結果が与えられる。

package main

import (
	"encoding/binary"
	"fmt"
	"math/rand"
)

func main() {
	flag := "actf{REDACTEDREDACTEDREDACTED!!}"
	rand.Seed(12345) // the actual seed is not 12345
	// drastically slow down naive brute force
	for i := 0; i < 100000; i += 1 {
		rand.Uint64()
	}
	for i := 0; i < 4; i += 1 {
		fmt.Printf("flag chunk: %d\n", binary.LittleEndian.Uint64([]byte(flag)[i*8:i*8+8])^rand.Uint64())
	}
	gap := 0
	for i := 0; i < 607; i += 1 {
		fmt.Println(rand.Uint64())
		for j := 0; j < gap; j += 1 {
			rand.Uint64()
		}
		gap = (gap + 1) % 13
	}
}

ブルートフォース対策の為に100000回乱数を生成してからフラグとXORする用の乱数を4つ生成する。その後、gapを変化させながら連続では無い607個の乱数を生成してその結果を与えられる。

rand.Uint64()は次のようになっている。

// Uint64 returns a non-negative pseudo-random 64-bit integer as an uint64.
func (rng *rngSource) Uint64() uint64 {
	rng.tap--
	if rng.tap < 0 {
		rng.tap += rngLen
	}

	rng.feed--
	if rng.feed < 0 {
		rng.feed += rngLen
	}

	x := rng.vec[rng.feed] + rng.vec[rng.tap]
	rng.vec[rng.feed] = x
	return uint64(x)
}

他にもSeedの設定とか色々あるが、最初に呼ばれるだけで途中からは呼ばれる様子が見られない。更にRNGの状態に影響を及ぼす処理は次に示す2行のみであり、非常に簡単な形をしている。

	x := rng.vec[rng.feed] + rng.vec[rng.tap]
	rng.vec[rng.feed] = x

おまけに生成した乱数がそのまま状態に残ることから、フラグとXORする乱数の生成直後の状態を復元出来ればフラグも復元出来そうである。

というわけでz3のbit_vecで状態を再現し、これと同じ処理をすることで元の状態を復元し、フラグを入手する。面倒なのでインデックスを総当りして全部ASCIIな奴を繋げた。

なお、ソースコードではフラグをリトルエンディアンとして4つのUint64型数値に変換しているのでエンディアンを考慮して復号する必要がある。

Code

状態復元部分だけ

from z3 import Solver, BitVec, If, LShR, sat, unsat
import output


int64_mask = (1 << 64) - 1
int32max = (1 << 31) - 1
rngLen   = 607
rngTap   = 273
rngMax   = 1 << 63

feed = rngLen - rngTap
tap = 0
gap = 0

s = Solver()
state = [BitVec(f"v_{i}", 65) for i in range(rngLen)]


def next_idx():
    global tap, feed
    tap -= 1
    feed -= 1

    if tap < 0:
        tap += rngLen

    if feed < 0:
        feed += rngLen


def get_rand():
    next_idx()

    x = state[feed] + state[tap]
    state[feed] = x

    return x

for _ in range(100000):
    next_idx()


flag1 = 4301770859063564088
next_idx()
s.add(((state[feed] ^ flag1) & 0xffffffff) == 1718903649)

for _ in range(3):
    next_idx()

for i in range(rngLen):
    x = get_rand()
    s.add((x & int64_mask) == output.nums[i])

    for j in range(gap):
        get_rand()

    gap = (gap + 1) % 13

res = s.check()
raw_state = []

if res == sat:
    recovered_state = s.model()
    for x in recovered_state:
        raw_state.append(recovered_state[x].as_long())

    print(raw_state)

Flag

actf{i_c4n_f0rs33_th3_p4s7_t00_}

Resources