低レイヤのプログラムの形式検証ツール

形式検証アドベントカレンダー 10 日目の記事です｡(2 本しかありませんが)

OS カーネルの実装や組み込みソフトウェアに利用できるような､C 言語とアセンブリ言語を対象とする形式検証ツールの紹介です｡出来ることと基本的な使い方くらいの説明になります｡(例もショボい) 今回紹介するツールは､軽量形式手法で使われるようなソースコードと直接的な繋がりが少ない設計を吟味するためのものではなく､ソースコードとの乖離が少ないものを選びました｡また､以下に紹介するツールは研究プロジェクトであったり､メンテナンスが放棄されたものも含みます｡

環境

OS: ArchLinux
opam version: 2.1.3
Nix version: 2.12.0

RefinedC

並行分離論理を Coq で形式化した iris を利用した検証ツール｡^refinedc^{refinedc_source}^oshi

Installation

opam にパッケージがある｡coq と iris のリポジトリを使っているので追加してからインストールする｡^{refinedc_installation}^{refinedc_note1}

opam repo add coq-released "https://coq.inria.fr/opam/released"
opam repo add iris-dev "https://gitlab.mpi-sws.org/iris/opam.git"
opam update
opam pin add -n -y cerberus "git+https://github.com/rems-project/cerberus.git#b60ea9a7d30dfa7f048c2b312dd86547939a035a"
opam pin add refinedc "git+https://gitlab.mpi-sws.org/iris/refinedc.git"

使い方

C のソースコードに注釈をつけたものが Coq に変換され,ある程度自動的に証明されたあと残ったものを手動で補題を立てて自動証明器に指示しつつ証明する｡

プロジェクトの生成

refinedc init

swap 関数がちゃんと値を入れ替えているか検証する例

#include <refinedc.h>
[[rc::parameters("a : loc", "b : loc", "n : Z", "m : Z")]]
[[rc::args("a @ &own<n @ int<i32>>", "b @ &own<m @ int<i32>>")]]
[[rc::ensures("own a : m @ int<i32>", "own b : n @ int<i32>")]]
void swap(int *a, int *b)
{
	int tmp = *a;
	*a = *b;
	*b = tmp;
}

refinedc init したディレクトリで以下のようにする

refinedc check swap.c

proofs/swap 以下に Coq に変換されたコードや生成された証明がある｡

この程度ならば自動で証明してくれるが､Coq に変換されるのでより複雑な対象には手動で証明することで対応できる｡

CBMC

モデル検査による C と C++の検査ツール｡^cbmc^cbmc_source^cbmc_hp CProver というプロジェクトの成果物で､他の成果物は^{cprover_overview}に説明がある｡ CBMC の他には goto 文を解析してくれるようなものもある｡

C 言語の場合 C99,C89,C11 と GCC や Visual Studio のほとんどの拡張に対応していて､未定義動作などのバグの種となるミスを指摘してくれる他､ユーザーが定義した性質が実行時に満たされるかどうかを静的に解析してくれる｡ (もちろん､検査器に指摘されたからと言ってバグであるとは限らない)

Installation

Win/Mac/Ubuntu に対応していますが､Docker Image が公開されているので使う｡

docker run -it diffblue/cbmc:5.71.0

使いかた

以下のようなフラグで検査する性質を指定できる｡

以下のようなプログラムに対して検査してみる｡

int main() {
	char buf[3] = {'a', 'b', 'c'};
	buf[3] = 'd';
}

指定したフラグでチェックされる性質(assertion)を見るには--show-propertiesをつける｡すると以下のように配列の境界チェックの条件が生成されていることがわかる｡

cbmc --bounds-check --pointer-check cbmc_sample.c --show-properties

実際に解析を実行するには先のフラグ--show-propertiesを外す

期待通りに検証が失敗している｡

ユーザー定義の条件の例

CBMC には､定義したアサーションに対して満たされるかどうか静的に検査する機能がある｡例えば wrap around しない減算をする以下のような関数にアサーションを加えて検査すると

cbmc  cbmc_sample1.c --function uint_sub_not_wa --trace

#include <assert.h>

unsigned int uint_sub_not_wa(unsigned int a, unsigned int b)
{
	assert(a >= b);
	unsigned int res = a - b;
	assert(res + b == a);
	return res;
}

1 つ目のアサーションに対していくつか反例が上がってくる｡(--traceで反例を表示できる) 以下のようにバリデーションを加えると検証が通る｡

unsigned int uint_sub_not_wa(unsigned int a, unsigned int b)
{
	if (a < b) {
		return 0;
	}
	assert(a >= b);
	unsigned int res = a - b;
	assert(res + b == a);
	return res;
}

ループが絡む検証の例

CBMC はループに関する性質を検証するために以下のようなコードを

while (flag) {
    YOURCODE
}

if (flag) {
    YOURCODE[1/flag]
    if (flag) {
        YOURCODE[2/flag]
        if (flag) {
            YOURCODE[3/flag]
        }
    }
}

のように解釈して(loop unrolling/unwinding)検査するため,どこまで検査するか上限を決定する必要がある｡^{cbmc_loop_unwinding} プログラム全体の各ループに対して統一的に設定するには--unwind Nのように指定する｡

例:

#include <assert.h>
int main() {
	for (int i = 0; i < 100; ++i) {
		assert(i < 100);
	}
}

cbmc --unwind 100 cbmc_loop.c

しかし､今回の場合のようにループ回数が固定だったりすると CBMC が自動的に N を推測してくれるので､一旦--unwind無しで実行してから手動で推測すればよい｡

VST/CompCert

言わずとしれた(?)形式検証済み C コンパイラ^compcert_hpだが､普通のプログラム検証にも使える｡派生物も研究･開発されており､アセンブリとの相互運用も形式検証出来るものもある｡^compcertm VST は CompCert の成果を使って一般のプログラム検証が出来るようにしている｡^vst_note1

Installation

opam で coq-released リポジトリを追加後に^vst_note2

opam install coq-vst coq-compcert

使いかた

Coq で設計の形式モデルを作って､その実装である C のソースコードをclightgenで Coq に変換し設計のモデルの要求を満たしていることを証明する｡

VST を使ったワークフローは

clightgen your_code.c(出力: your_code.v)
API spec を書く
実装が API spec を満たしていることを証明

// swap.c
void swap(int *a, int *b)
{
	int tmp = *a;
	*a = *b;
	*b = tmp;
}
int main()
{
	int x = 1, y = 2;
	swap(&x, &y);
	return x;
}

clightgen swap.c

API spec は､以下のようになる

Definition swap_spec : ident * funspec :=
DECLARE _swap
WITH sh: share, a: val, b: val, a_val: Z, b_val: Z
  PRE [ tptr tint, tptr tint ]
    PROP (writable_share sh)
    PARAMS (a; b)
    SEP (data_at sh tint (Vint (Int.repr a_val)) a; data_at sh tint (Vint (Int.repr b_val)) b)
  POST [ tvoid ] (
    PROP()
    RETURN()
    SEP (data_at sh tint (Vint (Int.repr b_val)) a; data_at sh tint (Vint (Int.repr a_val)) b)
  ).

Definition main_spec :=
 DECLARE _main
  WITH gv : globals
  PRE [] main_pre prog tt gv
  POST [ tint ]
     PROP()
     RETURN (Vint (Int.repr 2))
     SEP(TT).

PRE/POST で事前･事後条件を指定している
PARAMS で引数を指定
SEP は､メモリの状態(e.g. ここではポインタ a,b が指す値)を規定
PROP で追加の条件を書ける

Lemma body_swap: semax_body Vprog Gprog f_swap swap_spec.
Proof.
  start_function.
  try repeat forward.
  entailer!.
Qed.

実装が API spec を満たしていることを示している
start_functionはゴールを Hoare triple に変換してくれる｡この時点で API spec と実装のミスマッチ(e.g. spec の返り値の型と実装の返り値の型が食い違っている)も検出してくれる
forwardは､sequence rule の適用(gdb で si 連打するみたいな...)
entailer!は､分離論理のソルバ

全体はこのようになる

(* swap_verify.v *)
Require Import VST.floyd.proofauto.
Require Import swap.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.

Definition swap_spec : ident * funspec :=
DECLARE _swap
WITH sh: share, a: val, b: val, a_val: Z, b_val: Z
  PRE [ tptr tint, tptr tint ]
    PROP (writable_share sh)
    PARAMS (a; b)
    SEP (data_at sh tint (Vint (Int.repr a_val)) a; data_at sh tint (Vint (Int.repr b_val)) b)
  POST [ tvoid ] (
    PROP()
    RETURN()
    SEP (data_at sh tint (Vint (Int.repr b_val)) a; data_at sh tint (Vint (Int.repr a_val)) b)
  ).

Definition main_spec :=
 DECLARE _main
  WITH gv : globals
  PRE [] main_pre prog tt gv
  POST [ tint ]
     PROP()
     RETURN (Vint (Int.repr 2))
     SEP(TT).

Definition Gprog := [swap_spec; main_spec].

Lemma body_swap: semax_body Vprog Gprog f_swap swap_spec.
Proof.
  start_function.
  try repeat forward.
  entailer!.
Qed.

わりと最近に softwarefoundations の vol. 5 としてハンズオンが作られた｡^sf_vc

c-parser(StrictC)(seL4)

seL4 の検証プロジェクトの一部として配布されているのでリポジトリを持ってきて一部を使う｡

mkdir $workdir
cd $workdir
repo init -u ssh://[email protected]/seL4/verification-manifest.git
repo sync

https://github.com/seL4/l4v/blob/master/docs/setup.mdに従って依存を揃える^sel4_nix
$workdir/l4v/tools/c-parserに移動してmake CParser
$workdirに戻って./isabelle/bin/isabelle jedit -d ./l4v -l CParserとすれば jedit が起動して開発の準備が完了

使い方

C 言語のコードを Isabelle 上の形式言語 Simpl^simplに変換して Isabelle で形式化された要求を満たしていることを検証する｡

jedit を立ち上げて

./isabelle/bin/isabelle jedit -d ./l4v -l CParser CParserExample.thy

以下のようにすれば､ファイル名_global_addressesという context^{isabelle_context}に関数定義などが変換されたものが入っている｡

theory CParserExample
  imports CParser.CTranslation
begin
install_C_file "path/to/c_src.c"

関数はf_関数名_body_defのような名前で変換されるので,上に付け加えて

context c_src_global_addresses
begin
    thm f_your_function_body
end

などとすれば Output タブに Simpl の式が表示される

かなり自明な例

// a.c
void f(void) {}

(* CParserVerySimpleExample.thy *)
theory CParserVerySimpleExample
  imports CParser.CTranslation
begin
install_C_file "a.c"
theorem (in a_global_addresses) shows "\Gamma \turnstile {| True |} PROC f() {| True |}"
    apply vcg
    done

Simpl の式中では元の名前で参照できる｡

Frama-C/WP

Frama-C^framac^{framac_source} は､C 言語の静的解析フレームワークで､そのプラグインである WP^framac_wp が Verifast や CBMC のように C 言語に注釈をつけて条件を満たすか検証する機能を持っている｡

Installation

opam install frama-c

Why3 に証明器が登録されていないと言われたら､opam でインストールした場合証明器自体は入ってるはずなのでwhy3 config detectで why3 の設定を生成すれば動くと思われる｡

使い方

C 言語のコードに ACSL(ANSI/ISO C Specification Langage)という言語で注釈をつけて検査器にかける｡

swap の例:

/*@
   requires \valid(a);
   requires \valid(b);
   assigns *a;
   assigns *b;
   ensures *a == \old(*b);
   ensures *b == \old(*a);
*/
void swap(int *a, int* b);

void swap(int *a, int *b)
{
	int tmp = *a;
	*a = *b;
	*b = tmp;
}

\valid(x)はポインタ x はデリファレンスされても安全であることを表す ACSL のビルトインの述語
requres/ensures は事前･事後条件を表す
assigns は呼び手側にどの変数が変更されるかを教える
\old(x)は関数呼び出し前の x の値を表す

frama-c -wp swap.c

で検査できる｡

かなり充実したチュートリアルとして ACSL by Example がある｡^{acsl_by_example} また､プログラム検証の基本事項の解説を含むチュートリアルもあるらしい｡^{intro_cprog_framac}

CheckedC

C 言語を拡張して､安全にシステムプログラミングに使えることを目指しているプロジェクト｡^checkedc^{checkedc_source}

C の効率性や低レイヤの操作における自由度を下げない
最小限の拡張
読みやすいコード･分かりやすい拡張･最小限の型付け
既存のコードベースに対してインクリメンタルな使い方を可能にする

といった設計思想で作られている｡

Installation

Windows 向けにはバイナリ配布があるが､Linux にはないのでビルドする｡処理系は Clang をベースに作られていて､同じようにビルドできる｡^{checkedc_compiler_build}

mkdir $workdir && cd $workdir
git clone https://github.com/Microsoft/checkedc-clang src
cd src/llvm/projects/checkedc-wrapper/
git clone https://github.com/Microsoft/checkedc
cd $workdir
cmake -G Ninja -DLLVM_ENABLE_PROJECTS=clang \
          -DCMAKE_INSTALL_PREFIX=./install \
          -DCMAKE_BUILD_TYPE=Release \
          -DLLVM_ENABLE_ASSERTIONS=ON \
          -DLLVM_CCACHE_BUILD=ON \
          -DLLVM_INSTALL_TOOLCHAIN_ONLY=ON \
          -DLLVM_TARGETS_TO_BUILD="X86" \
          -DLLVM_LIT_ARGS=-v \
          ./src/llvm
ninja

使い方

C 言語に対して主に以下のように拡張された言語でプログラムを記述する｡

境界チェック付配列型･ポインタ型
generic struct
generic function
後方互換性(i.e. 既存の C 言語のコードベースがそのまま動く)
動的検査

境界チェック付配列型･ポインタ型

checked キーワードで境界検査付の配列が作れる e.g.

#include <stdchecked.h>↲
int out_of_bound(int a checked[2]) {
    return a[3];
}

これを先程ビルドしたコンパイラに通すと以下のようにエラーになる

例は一次元だが､多次元配列もchecked[n][m]のようにして定義できる｡他に null-terminated array のための型もある｡^{checkedc_spec}

generic struct/function

しょうもない例だが､このように書ける

#include <stdio.h>
#include <stdchecked.h>

struct BinTree _For_any(T) {
    T *elm;
    struct BinTree<T> *left;
    struct BinTree<T> *right;
};

_For_any(T) struct BinTree<T> new_bintree(T *elm) {
    struct BinTree<T> t =  {
        .elm = elm,
        .left = NULL,
        .right = NULL,
    };↲
    return t;
}

int main() {
    int e = 1;↲
    struct BinTree<int> t = new_bintree<int>(&e);
    printf("%i\n", *t.elm);
}

spec^{checkedc_spec}では､for_anyとされているが､GitHub wiki の記述では_For_anyとなっていて前者はコンパイルが通らなかった｡

動的検査

dynamic_checkでassertのように与えられた条件が実行時に満たされるかどうか検査できる｡ dynamic_checkで与えられた条件はコンパイラが仮定として受け取るため境界検査などを省略できる場合がある｡(^{checkedc_spec}, 2.11)

後方互換性

既存のライブラリを問題なくリンクできる他#pragma CHECKED_SCOPE ONで検査の適用範囲を管理できる｡また､CheckedC で既存のコードベースをコンパイルしたときも､ソースコードを書き換える必要も､勝手に意味論が変わることもないため､既存のコードベースに CheckedC を混ぜる場合も問題なく､相互運用性がある｡

VeriFast

C 言語に分離論理で事前･事後条件を書いて検証するツール｡^verifast^{verifast_source} マルチスレッドなプログラムにも対応している｡

また､しっかりしたチュートリアル^verifast_tutがある｡

Installation

Win/Mac/Linux に向けたリリースがある｡

wget https://github.com/verifast/verifast/releases/download/nightly/verifast-21.04-118-gc2cdad9a-linux.tar.gz
tar xf verifast-21.04-118-gc2cdad9a-linux.tar.gz
./verifast-21.04-118-gc2cdad9a-linux/bin/verifast --help

使い方

独自の仕様記述言語で C のソースコード上にコメントとして事前･事後条件を書くと､自動的に証明してくれる｡以下のような単純な swap 関数を例に説明する｡

void swap(int *a, int *b)
//@requires *a |-> ?x &*& *b |-> ?y;
//@ensures *a |-> y &*& *b |-> x;
{
	int tmp = *a;
	*a = *b;
	*b = tmp;
}

@requires ...;で事前条件を書く
@ensures ...;で事後条件を書く
事前･事後条件で引数に言及できる
ポインタ変数であれば"デリファレンス |-> 値"で指している値について主張出来る
- ?xとあるのは ∃x. ref ↦ x という意味でポインタ変数 ref が指している値をその名前で束縛できる
&*&は分離論理における separating conjunction で両隣の式が成り立ち､且つ言及しているメモリ領域が被らないことを主張する

これを踏まえれば上の記述は, "エイリアスでないポインタ a と b にそれぞれある値 x と y を格納して swap(a, b)を呼び出せば､互いの指す値が入れ替わっている"ということを主張している｡実際に verifast を使って検証するには

path/to/verifast -shared verifast_swap.c

-sharedで main 関数を要求しないようにしている｡出力:

おわりに

いくつか取り上げようと思って~~面倒くさくなって~~やめたやつ

Armada^armada^{armada_source}^{armada_install}: パフォーマンスを落とさずに安全な並列プログラミングが出来ることを目指したツール
- dotnet runtime 5.0.17 必要だが動かすことには成功
Bedrock^bedrock^bedrock_hp^{bedrock_source}: 低レイヤの自由度とパフォーマンスを犠牲にせず､Coq から C やアセンブリを Extraction する
- 証明が通らなかった部分を直したりしたが^owari1Coq コードのコンパイルが無限に終わらず断念
csolve^csolve^{csolve_source}^csolve_hp: C 向けの Liquid type ベースな検証器
- ビルドしてたらなんか内部的なところが型エラー起こしてて諦めた
vcc^vcc^vcc_source: C 言語の並行処理を検証できる

https://doi.org/10.1145/3453483.3454036 ↩
https://gitlab.mpi-sws.org/iris/refinedc ↩
個人的最推↩
https://gitlab.mpi-sws.org/iris/refinedc#installing-refiendc-and-its-dependencies ↩
主に iris のほうで割と活発に更新があるので switch を切っておくが吉↩
http://dx.doi.org/10.1007/978-3-540-24730-2_15 ↩
https://github.com/diffblue/cbmc ↩
https://www.cprover.org/cbmc/↩
https://github.com/diffblue/cbmc/blob/develop/TOOLS_OVERVIEW.md ↩
https://www.cprover.org/cprover-manual/cbmc/unwinding/↩
https://compcert.org ↩
https://doi.org/10.1145/3371091 ↩
後に言及するタクティクの開発など↩
他に 32bit 版(coq-compcert-32)とセットアップに coq-platform を使うパッケージがある(coq-compcert-64)↩
https://softwarefoundations.cis.upenn.edu/vc-current/toc.html ↩
こういうものも用意してあったhttps://github.com/unsoundsystem/sel4-nix一応動いた↩
https://www.isa-afp.org/entries/Simpl.html ↩
https://isabelle.in.tum.de/dist/Isabelle2022/doc/locales.pdf ↩
https://frama-c.com/html/overview.html ↩
https://frama-c.com/html/direct-source-distributions.html ↩
https://frama-c.com/fc-plugins/wp.html ↩
https://github.com/fraunhoferfokus/acsl-by-example(あまりメンテナンスされていない｡著者の所属が分野を転換したらしい)↩
https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf ↩
https://doi.org/10.1109/SecDev.2018.00015 ↩
https://github.com/Microsoft/checkedc ↩
https://github.com/microsoft/checkedc-clang/blob/master/clang/docs/checkedc/Setup-and-Build.md ↩
https://github.com/Microsoft/checkedc/releases ↩
https://doi.org/10.1007/978-3-642-20398-5_4 ↩
https://github.com/verifast/verifast ↩
https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf ↩
https://doi.org/10.1145/3385412.3385971 ↩
https://github.com/microsoft/Armada ↩
https://github.com/microsoft/Armada/blob/main/BUILD.md ↩
http://dx.doi.org/10.1145/2500365.2500592 ↩
https://plv.csail.mit.edu/bedrock/↩
https://github.com/mit-plv/bedrock ↩
仮定の名前を指定せずに intros.してたせいだった↩
https://doi.org/10.1007/978-3-642-31424-7_59 ↩
https://github.com/ucsd-progsys/csolve ↩
https://goto.ucsd.edu/csolve/↩
http://dx.doi.org/10.1109/ICSE-COMPANION.2009.5071046 ↩
https://github.com/microsoft/vcc ↩