「記号実行」で利用される「SMTソルバ」

私は興味のある分野がいろいろあるのですが、プログラムの解析技術もその中の一つです。

プログラム解析技術の中には、「記号実行 (シンボリック実行)」というものがあります。

これは、「どのような入力を与えられたとき、どの経路を実行するのか」を特定する技術です。

これを使うことで、プログラム上の多くの経路を通るような、高いテストカバレッジのテストケースを作成できるようになったりします。

一般的に、経路は条件分岐によって行き先が変わるので、分岐における条件式とそこに含まれる変数の関係を解き明かす必要があります。

そこで、登場するのが、「SMTソルバ」というプログラムです。

今回使う「z3」は、Microsoft Researchが開発しているSMTソルバです。

GitHub - Z3Prover/z3: The Z3 Theorem Prover

これを使えば、条件式がtrueになる可能性があるのかを特定したり、条件式がtrueになる変数の例を挙げることができます。

Rustのcrateの中にも、すでに「z3」を使うためのcrateがいくつか存在するようです。

今回は、その中でも最もメジャーそうなcrate「z3」(crateの名前もそのままでした)を使ってみます。

z3 - Cargo: packages for Rust

「z3」を使ったサンプルコード

私の実行環境はDebian Linux 9.8。

Rustのバージョンは、1.34.0 (91856ed52 2019-04-10)、crateの「z3」のバージョンは、0.3.2。

crateの「z3」を使うためには、Linux環境にz3の機能を持つlibz3が必要なので、apt-getなどで先にインストールしておく必要があります。

内部的にはこのライブラリを呼び出しているようです。

そして、サンプルコードはこちらになります。

use z3;

fn main() {
    let cfg = z3::Config::new();
    let ctx = z3::Context::new(&cfg);

    let x = ctx.named_int_const("x");
    let y = ctx.named_int_const("y");

    let zero = ctx.from_i64(0);
    let two = ctx.from_i64(2);
    let seven = ctx.from_i64(7);

    let solver = z3::Solver::new(&ctx);
    solver.assert(&x.gt(&y));
    solver.assert(&x.gt(&zero));
    solver.assert(&y.gt(&zero));
    solver.assert(&y.rem(&seven)._eq(&two));
    solver.assert(&x.add(&[&two]).gt(&seven));

    println!("solver: {}", solver);
    println!("check: {}", solver.check());

    let model = solver.get_model();
    let x_value = model.eval(&x).unwrap().as_i64().unwrap();
    let y_value = model.eval(&y).unwrap().as_i64().unwrap();

    println!("x: {}", x_value);
    println!("y: {}", y_value);
}

これを実行すると、次のように出力されました。

solver: (declare-fun y () Int)
(declare-fun x () Int)
(assert (> x y))
(assert (> x 0))
(assert (> y 0))
(assert (= (rem y 7) 2))
(assert (> (+ x 2) 7))

check: true
x: 6
y: 2

解説

少しずつ追って見ていきます。

    let cfg = z3::Config::new();
    let ctx = z3::Context::new(&cfg);

まず、ここでz3の環境を整えるため、ConfigとContextを新たに作ります。

ここにいろいろな変数、数値、条件式などが格納されていくようです。

    let x = ctx.named_int_const("x");
    let y = ctx.named_int_const("y");

    let zero = ctx.from_i64(0);
    let two = ctx.from_i64(2);
    let seven = ctx.from_i64(7);

変数xとyを定義し、他にも数値データである0、2、7についても定義します。

    let solver = z3::Solver::new(&ctx);
    solver.assert(&x.gt(&y));
    solver.assert(&x.gt(&zero));
    solver.assert(&y.gt(&zero));
    solver.assert(&y.rem(&seven)._eq(&two));
    solver.assert(&x.add(&[&two]).gt(&seven));

ここではSolverを新たに作成し、条件式を追加していきます。

ここで入力した条件式は、次のようになります。

x > y
x > 0
y > 0
y%7 == 2 (yを7で割った余りが2に等しい)
x + 2 > 7

    println!("solver: {}", solver);
    println!("check: {}", solver.check());

solver自体を出力すると、入力した条件式を見ることができます。

solver.check()をすることで、入力した条件式が成立する変数x、yが存在するかがわかります。

実際、trueが返されたので、この式が成立する値があるようです。

    let model = solver.get_model();
    let x_value = model.eval(&x).unwrap().as_i64().unwrap();
    let y_value = model.eval(&y).unwrap().as_i64().unwrap();

    println!("x: {}", x_value);
    println!("y: {}", y_value);

ここでは、このSolverからModelを取得し、さきほどの式が成立する、具体的なxとyを取得しています。

結果的に、x = 6、y = 2となり、確かに当たっているようですね。

今回は、適当なxとyを取得しましたが、線形計画問題のように「x + yが最大(または最小)になるような値」なども取得することができます。

まとめ

SMTソルバ「z3」を使うことで、プログラム中にある条件式がtrueになる条件を調べることができます。

これによって、「どのような入力を与えられたとき、どの経路を実行するのか」を特定することができるようになります。

実際、有名なCTFチームの一つである「Shellphish」が開発している「angr」という記号実行ツールでも、「z3」が使われています。

SMTソルバを使えば、パズルを解いたり、線形計画問題を解いたりすることもできるので、記号実行以外にも使える場面はいろいろありそうです。

Toshihiro YAMAGUCHI’s Diary

RustでMicrosoft製SMTソルバ「z3」を使う

「記号実行」で利用される「SMTソルバ」

「z3」を使ったサンプルコード

解説

まとめ