Rustの形式検証ツールCreusotを触ってみる
概要
Rustの形式検証ツールCreusotを触ってみた備忘的まとめ
Creusotとは
github
論文
CreusotはRustの形式検証、演繹的検証(Deductive Verification)のためのツールです。Rustのソースコード中にプログラムが満たす仕様を記述し、形式的に検証することができます。
形式検証では、proptestなどによるプロパティテストとは異なり、プログラムが仕様を満たすことを数学的に厳密に検証します。したがって、コーナーケースを見落とすようなことがありません。また、同様に厳密な検証を行うkaniなどのモデル検査よりも複雑な命題についての検証ができます。kaniのブログ記事に"subway map"という名前でRustのテスト・検証手法をいくつかまとめた図がありますが、この中ではPrustiと並んで最も右に位置する「重量級」の手法です。
CreusotはRust(のサブセット)からWhyMLへの翻訳機として動作します。WhyMLとは形式検証プラットフォームWhy3において検証対象のプログラムを記述するために用いられる言語です。Why3ではWhyMLで書かれたプログラムについての命題をZ3などの自動証明器やCoqなどの対話型証明器を用いて証明することができます。Why3を用いたプログラムの検証ツールには他に、C言語を対象とするFrama-CやOCamlを対象とするCameleerなどがあります。
特徴
Creusotでは預言(prophet)という手法を用い、Safe Rustを対象とすることで、分離論理を必要とせずに検証ができます。
最初に分離論理について少し触れておきます。以下のようなCの関数があったとしましょう。
int hello(int *a, int *b) {
*a = 0;
*b = 1;
return *a + *b;
}
これは必ず1を返すでしょうか？残念ながらそうではなく、例えばaとbが同じであれば2を返します。この関数についての仕様を記述するならば、「aとbが重ならない（すなわち「分離された」）領域を指す正当なポインタならば2を返す」というような表現ができる必要があります。
そのような記述のための仕組みを備えるのが分離論理であり、手続き型言語の検証ではしばしば用いられるのですが、分離論理の不要な純粋関数型言語の場合と比べて検証が複雑になることは否めません。
ところで先程のhello関数においてaとbが異なる領域であるということは、Rustのボローチェッカがまさに保証することです。これは、Safe Rustの範疇では面倒な分離論理を回避できるはずだということを示唆しています。Rustを純粋関数型に近い形へと翻訳するために、Creusotでは預言という手法を用いてRustの参照を表現しています。自分は預言についてはざっくりとしか理解していませんが、参照を「今の値」と「参照が終わるときの値」のペアとして表すものです。ちなみにCreusotが基にしている「Rustの検証に預言を用いる」手法は日本人研究者が提案したものなので日本語の資料が存在しています。
使用法
インストールについては公式リポジトリのREADMEに従えば問題ないと思います。
また、具体的な使用法についてはCreusotを用いて検証されたSATソルバであるCreuSATの論文が詳しいです。
ここでは、先程例示したhello関数のRust版を考えます。(完全なソースは ここ)
use creusot_contracts::*;
// 関数の事後条件を"ensures"アトリビュートで記述する
// 返り値はresultで表される
// ここでは、関数の返り値が1になるという仕様を記述している。
#[ensures(result == 1i32)]
// ^記号は参照の終了時の値を表す。ここでは、関数から戻る時点でaが0であるという仕様を記述している
#[ensures(^a == 0i32)]
// aの場合と同様、関数から戻る辞典でbが0であるという仕様を記述している
#[ensures(^b == 1i32)]
fn hello(a : &mut i32, b : &mut i32) -> i32 {
*a = 0;
*b = 1;
*a + *b
}
ensuresのカッコ内は、Pearliteという言語で記述されます。基本的にはrustと同じ文法ですが、「ならば」記号==>や量化子forall/exists を用いた一階の論理式を書くことができます。
cargo creusotコマンドでWhyMLのソースであるmlcfgファイルを生成することができます。Creusotの役目はここまでで、その先はWhy3を使った検証作業になります。
生成されたmlcfgファイルをWhy3のIDEで開くと、以下のような画面が表示されます。
左のペインに証明すべき命題(goal)が表示されます。hello'vc と書かれているのが、hello関数についての示すべき命題です。まだ証明されていないので左のStatus欄が？マークになっています。また、右のペインには明らかにいかつい見た目のものがgoalとして表示されています。
見た目はいかついですが、自動証明器はこの程度であれば一瞬で証明してくれます。ゴールの右クリックから自動証明コマンド"Auto level 0"を選ぶと
命題が証明され、Status欄が緑のチェックマークに変わりました。
これでhello関数についての主張は形式的に検証されたことになります。
より詳しくは別の記事を書いたのでそちらを参照してください。
制約
ポインタ
ポインタは使えません。これは先に述べた通り分離論理を回避するためには本質的な制約だと考えられます。
unsafeだからこそ検証したいというのはまっとうな需要だと思いますが、その場合はPrustiなど他のツールを使うことになると思います。
ただし、unsafeなポインタ操作などを含む関数に対しても、#[trusted]を用いて検査を無効化した上で、その関数に対してどのような仕様を期待しているのかを形式的に記述することはできます。
停止性
現状では通常の実行可能な関数（即ち#[logic]がついていない関数）について停止性の検証ができません。#[logic]をつけた関数はPearliteにおける命題の記述に用いる関数として扱われ、これについては停止性の証明を要求されます。
Discussion