Kの紹介と検証器の話

adventk.asc

Semantic-Based Program Verifiers for All Languages

前置き

このgistは今年読んだ一番好きな論文2017 Advent Calendarの1日目の記事です。

去年、覚え書きのような記事で参戦したら、歓迎の言葉に加えて参加賞まで貰ってしまった者です。あれで終わらせるのは申し訳ない以前に悔しいので、今回はよそゆきの文章でガッツリ書いてリベンジすることで感謝の言葉に替えたいと思います。

この記事では、読者としてC言語に触れた経験がある人を想定しています。他の言語でもプログラミング経験があればさほど難しくはないと思いますが、「プログラミング言語って何？」という人が理解するのは厳しいかもしれません。

文献情報

タイトル

Semantics-Based Program Verifiers for All Languages

著者

• Andrei Stefanescu

• Daejun Park

• Shijiao Yuwen

• Yilong Li

• Grigore Rosu

出典

OOPSLA 2016

去年発表のもので申し訳ないですが、11月開催なのでほぼ今年みたいなものでしょう。

OOPSLAは プログラミング言語学会四天王^[1]なんて呼ばれたことがあるようなトップカンファレンス^[2]なので、十分に期待できるものだと思っていいでしょう。

ざっくりした内容としては「複数のプログラミング言語に対応可能な共通検証基盤を作って実験しました」といったところでしょうか。複数言語対応というところがミソで、この研究が初ではないでしょうか^[3]。

𝕂 flamework

論文の内容に入る前に、背景となるツールを紹介したいと思います。個人的にはこれだけでも覚えて帰ってもらえれば満足です。

筆者らの研究室で作っている K framework というプログラミング言語作成ツールがあります。公式の言葉を借りれば「rewrite-based executable semantic framework」とのこと。
ひどい名前^[4]に反して実は画期的なツールであることを、プログラム言語のつくりと共に説明しましょう。

プログラミング言語は、形を表す シンタックス（文法） と動作を表す セマンティクス（意味論） からできています。例えば、「 if(b) B1 else B2 というコード片はbが数値、B1とB2がブロックで、全体として文を表す」というのがシンタックスで、「 if(b) B1 else B2 はbが0でないときはB1、それ以外はB2と同じ意味である」というのがセマンティクスです。
一般に、シンタックスはyaccやPEGといったツールによって記述されます。広く使われる形式であるため一度書いてしまえば再利用もし易く、扱い易いと言っていいでしょう。一方、セマンティクスは普通、数十〜数百ページに及ぶ仕様書や、コンパイラ・インタプリタといった処理系（つまりプログラム）によって定められ、形式的な定義は必要になった時に後から作られる場合がほとんどです。

Kでは、シンタックスとセマンティクスの両方を定められた形式で書くことで言語を作っていきます。
シンタックスとセマンティクスが揃えば言語定義はもうできたと言っていいので、処理系やデバッガといった諸々のツールを作るのは 自動で やってもらおう、というのがKのコンセプトです。筆者らの研究室のウェブサイトでは、このコンセプトの表現に以下のような図を用いています^[5]。

この図における『verifier（検証器）』の生成機能を作ろう、というのがK側から見たこの研究の目的となります。

ちなみに、Kの開発チームは言語定義作成をかなり頑張っていて、githubを見ると20近い既存言語についてリポジトリがあります。大雑把に言えば、この研究で20言語分の検証器を一度に作成したということですね。

プログラム検証

プログラム検証 とは、プログラムを検証することです。形式検証とも呼ばれます。
世間ではプログラムの動作を保証したい時に、実際に入力を流し込んで期待する出力が得られるか確認するテストがよく用いられます。これは多数の入出力例を用意する必要があり、また普通は実際にプログラムを動かさなければ検査できません^[6]。
一方でプログラム検証は、無限通りの入力パターンがあっても漏れなく確認でき、また実行することなく検証可能であることが強みです。その分手法として重かったりはしますし、単純にどちらが強いと言える話ではありませんが。

世の中にプログラム検証器は既に色々ありまして、例えばC言語ならVCCとかFrama-CとかVerifastとか……本当に色々あります。
これらのツールは、基本的に中間言語を使います。つまり、プログラムを検証し易い言語に変換し、検証したいことを同じく分かり易いように変換して、汎用的な検証器に投げるというわけです。ただし、この変換は自明なものではなく、バグを生みがちです。

プログラミング言語のセマンティクスをそのまま流用できるような論理体系を構築し、その中で検証したい条件を書くことができれば、そんな間違いは起こらないはず……というのが、検証側から見たこの論文の目的です。

具体例

以下に、二分木構造nodeと、そこに値を挿入する関数insertを定義したC言語のプログラム片を示します。これが今回の検証対象です。ポインタを扱っているあたりが挑戦的ですね。

struct node{
  int value;
  struct node *let, *right;
}

struct node* new_node(int v){
  struct node *node;
  node = (struct node *)malloc(sizeof(struct node));
  node->value = v;
  node->left = NULL;
  node->right = NULL;
  return node;
}

struct node* insert(int v, struct node *t){
  if(t == NULL) return new_node(v);
  if(v < t->value) t->left = insert(v,t->left);
  else if(v > t->value) t->right = insert(v,t->right);
  return t;
}

このinsertは、引数の木が二分探索木（BST）だった場合、返り値もBSTになるように作られています。例えば、次の図はinsertを[8,3,6,10,14,1,13,7,4]の順で行った時にできるBSTです。

となれば当然、insertが本当にBSTを作るのか検証したくなりますね。……なりますよね？
本研究で作成した検証器では、このことを以下のような仕様として書くことができます。

rule
  <functions>FUNCTIONS:Map</functions>
  <structs>STRUCTS:Map</structs>
  <mem>...MEM:Map(tree(L1, T1:Tree) ⇒∀ tree(?L2, ?T2:Tree))...</mem>
  <threads>
    <thread>...<k>
      insert(tv(V:Int, int), tv(L1:Loc, struct node))
        ⇒∀ tv(?L2:Loc, struct node)...
    </k>...</thread>
  </therads>
requires bst(T1) ∧ -2147483648 ≦ V ∧ V ≦ 2147483648
ensures bst(?T2) ∧ tree_keys(?T2) = {V}∪tree_keys(T1)

いきなりXMLが出てきて面食らったかもしれません。これはシステムの状態を表すK特有の記法ですが、プログラムを表す <k>〜</k> に注目すれば雰囲気が掴みやすいかもしれません。
この仕様は端的にいえば、BSTであるL1^[7]に対してinsert(L1,V)を行った時、L1にVを加えたBSTになるということです。214783648はint型で表現できる範囲を表しており、?Xは「その条件を満たすようなXが存在する」くらいの意味で捉えてください。

ここで一つ重要なのは、 <mem>〜</mem> の部分でメモリの状態を直接示していることです。このmemは（検証器が用いる論理体系ではなく）KにおけるC言語のセマンティクスで定義されたもので、名前も中身も各言語が好きに決められます。

論文では他言語対応であることを示すために、さらにJavaとJavaScriptで同様のプログラムと仕様を書いていますが、ここでは割愛します。

理論

この論文の中核にあるのは、 Matching Logic と呼ばれる論理体系です。これは以下のような特徴を持ちます。1はMatching Logicの使い方の話で、2は定義上の話、3は2から導かれる性質なので、ちょっと不揃いではありますが。

1. configurationと呼ばれる、システムの状態を表す論理式を持つ

   • 上で見たXMLに相当するもので、実行途中のプログラム・変数の値・関数テーブルなど、それぞれの言語に必要な情報を全て含むことができる

2. 真理値ではなく値の集合を論理式に割り当てる

   • configurationの場合、そのプログラムが取りうる状態の集合になる

   • <k> 2 * ?N </k> なら{0,2,4…​}とかいうノリ

3. configurationとそれが持つ条件を並べて書ける

   • <k> 2 * ?N </k> ∧ (?N < 10) とか

先ほどの仕様例で言えば bst(T1) ∧ 〜 などがMatching Logicの一つの論理式になります。

そして、Matching Logicにおける論理式間の関係reachabilityを定義することで、Reachability Logicが生まれます。reachabilityとは簡単に言えば「論理式φからルールに従って論理式φ’にすることができるか」というもので、 φ ⇒∀ φ' のように書きます。
φが状態を表すので、「φという状態から実行するとφ’になるか^[8]」という仕様を表すことができるわけです。

Reachability Logicの特徴としては以下のものがあります。

1. セマンティクスをほぼそのままの形で使える

   • セマンティクスにおけるルール定義がそのままReachability Logicのルール定義になる

2. 非決定的なプログラムに対して検証可能

   • 現実に評価順などが不定な言語仕様は多い

セマンティクスをそのまま使えて仕様が書けるような論理体系を作ることができたので、あとはこれに対して自動推論することができれば、それが検証器になります。

Matching LogicやReachability Logicの詳細は推敲前の版で書いているので、気になる方はどうぞ。

実装と評価

冒頭で述べた通り、この理論を用いた検証器生成器がKに実装されています。2.5人年^[9]かけて3万行ほどのJavaを書いたとのこと。基本はシンボリック実行^[10]なので、SMTソルバZ3を利用しています。

評価としては、連結リストおよび木に対する18の基本的操作について、その性質を検証して時間を計測しています。例として示したinsertもその一つですね。
結果を見ると、検証にかかる時間は1秒未満から5分程度。それなりに複雑なプログラムも入っていることを考えると、まずまずの結果ではないでしょうか。筆者らはこの結果から、本システムは十分に実用的であると結論しています。

続いて、Kにおける各言語のセマンティクスおよび今回の仕様の記述コストについて。表でまとめます^[11]。

	C	Java	JavaScript
セマンティクス開発期間（ヶ月）	40	20	4
セマンティクス行数	17,791	13,417	6,821
セマンティクス修正期間（日）	7	4	5
セマンティクス修正行数	468	95	49
仕様数	36	31	31
定義数	27	27	27

各言語のセマンティクスは今回の研究とは無関係に開発されたものですので、こちらに要した手間はあまり気にしないことにしましょう。
今回使うにあたってバグに気付いたとか検証しにくかったといった理由からセマンティクスに一部変更を加えており、それが『セマンティクス修正』の項です。仕様数は読んで字の如く。定義数というのは、上であげたbstなどの定義をいくつ書いたかを意味します。

Kに対象言語のセマンティクスが存在するという前提下においては、1週間もあれば検証器が作れてしまうわけです。「言語非依存の検証基盤を作る」という目的は十分に達成されたのではないでしょうか。

後書き

次のことについて見てきました。

• セマンティクスを重視したプログラミング言語開発ツールK

• セマンティクスとプログラム仕様を同じところに落とし込むReachability Logic

• それらを利用した言語非依存の検証基盤の実用性

個人的に、3つのアイデアはそれぞれ非常に興味深く、かつ実用性もあり、「今年読んだ一番面白い論文」に相応しいと思っています。
実際にこの検証器を使いたいかというと……今後に期待ですね。K自体については勉強中なので、そのうち何かしらアウトプットできるかもしれません。

今年読んだ一番好きな論文2017 Advent Calendarは現時点でまだ募集中のようです。異様に豪華な賞品ラインナップにも関わらず、前半スッカスカで寂しいです。
全く面識の無い人間が当日に飛び込んでも歓迎されることは去年実証されているので、明日以降、これを読んでいる皆さんの論文紹介に出会えることを楽しみにしています^[12]。

ここまでお付き合いいただきありがとうございます。お粗末様でした。

---

1. 4つともACM（情報系最大手学会） SIGPLAN（プログラミング言語系分科会）のpremier forum/conferenceです。ざっくりPOPL:理論、PLDI:実装、ICFP:関数型、SPLASH/OOPSLA:応用という認識。

2. 「トップカンファレンス」という概念ってもしかして情報系以外にはあまり通じなかったりするのでしょうか。

3. 例えばWhy/JessieはCとJavaの2言語に対応していると言えるのかもしれませんが、「もう1言語追加してみよう」とはあまりならないように思えます。セマンティクスから定義する手間を考えても、1言語追加する手間は既存手法に比べて抑えられているのではないかと推測します。

4. 名前空間が枯渇していくのは世の常ですが、それでも識別性の低い名前は悪だと思います。kframeworkだと長いしググラビリティ低いしkを見逃してしまいそうなので、適当な公式略称が欲しいところ。

5. 現状ではこれらのツールが全て生成できるわけではありません。要になるだろうコンパイラ生成機能も作られていないようです。

6. プログラム検証などを指して「静的テスト」などと言ったりすることもあるようですが、単に「テスト」と言った場合にはここで述べたような動的テストのことを指すのが普通でしょう。

7. 正確に言えば、L1はBSTを指す参照（ポインタ）としているような気がしますが、話がややこしくなるので気にせずいきましょう。

8. 何を実行するのか不明瞭な表現にも見えますが、ここで状態というのは「これから実行しようとしているプログラム片」も含むことに注意してください。

9. 「人月」はよく聞きますが、「人年」はあまり聞かない気がします。英語論文を読んでると「実装にX人年かかった」みたいな記述は時々見かけますが、日本語ではあのみずほ案件ですら「20万人月」と頑なに月を重んじています。やはり語呂でしょうか。

10. 実行時まで確定しない入力値などは変数としておいたまま、分岐の際に「こっちへ行くならxは4以上」など条件式を覚えながら網羅的に実行する手法です。シンボリック実行にはSMTソルバがつきもの。

11. なぜかgistでは表中の右寄せ指定が効かないようです。汚い図ですが、ご容赦ください。

12. 院生でない方はすみません。クリスマスを過ぎてから読んでいる方は是非来年に。

gradver.asc

『Gradual Program Verification』紹介

3行で

• 手続き型言語における契約プログラミングの新しい検査手法である漸進的検査を提案する

• 静的検査と動的検査を効果的に、かつ配分を制御可能な形で組み合わせた

• 漸進的型付けのアイディアを基礎としており、その利点を継承している

前置き

このgistは(大人版)今年読んだ一番好きな論文2018 Advent Calendarの1日目の記事です。

学生版の方は喜ばしいことに今年ついに満員を果たしましたが、こっちはまだ僕しかいないので寂しいです。
ハードルを下げる^[1]ために書いておくと、僕は3月まで学生でしたが、今はただの会社員です。研究職という訳ではなく、就職してからは論文なんて趣味で数本読んだ程度です。

この記事の想定読者は、多少プログラミングの心得がある人です。具体的には、何かしらの手続き型言語でFizzBuzzが書ける程度。
それを満たしているのに内容がよくわからなかった方は、僕の文章力を詰る権利があります。

文献情報

タイトル

Gradual Program Verification (Springer)

著者

• Johannes Bader

• Jonathan Aldrich

• Éric Tanter

出典

VMCAI2018

VMCAIはPOPLという超大手フォーラムのco-located conferenceです。VMCAI自体は「その筋の人には知られている」くらいの感じかなと。

論文の立ち位置としては第一著者の修論から核の部分を引き抜いてきたような内容になっています。

契約プログラミング

この論文では暗に「検査といえば契約」という感じで話を進めているので、とりあえず契約プログラミングとは何かという話から始めます。論文の話ではないので、知ってる人は読み飛ばして大丈夫です。

契約プログラミングとは

契約プログラミング とは、コード中に満たすべき性質(契約)を書く手法です。
論文では例として以下のようなコード(C風の独自言語)を載せています。

// 銀行口座(balance)から指定した金額(amount)を引き出し、残高を返す関数
int withdraw(int balance, int amount)
  requires (balance ≥ amount) ensures (result ≥ 0)
{
  return balance - amount;
}

requires と ensures が契約を表すキーワードで、関数� withdraw は「開始時に balance ≥ amount」であり、その関係を守る限り「終了時に result ≥ 0 ^[2]」であるということを表しています。
このように、関数の 開始時に満たされているべき前提(事前条件) と、関数の 終了時に満たされる性質(事後条件) をコードに記すのが、契約プログラミングの基本です。

関数の前提と性質を明示することで、その関数がやるべきことを明確にするわけですね。要はユニットテストで検査するようなことを、具体的な値ではなく性質によって示す手法と思ってください。

契約プログラミングは様々な言語で利用することができますが、専用構文を持っている(言語仕様レベルでサポートしている)言語の中ではD言語あたりがそこそこ知られています。
契約ライブラリは詳しくないですが、.Net系のCode Contractsとか。

契約の検証方法

契約は多くの場合、実行時に検査(動的検査)されます。実際に関数が呼ばれた時に、条件を満たしているかチェックし、違反していたらエラーを出して終了する、ということです。

このような検査はごく自然な方法ですが、例えば以下のような明らかに契約違反するコードでも、 実行してみないとわからない 、ということになります。

int withdraw(int balance, int amount)
  requires (balance ≥ amount) ensures (result ≥ 0)
{
  return balance - amount - 10; // balance=amount=0の場合などに事後条件違反
}

withdraw(-10, 0);  // 事前条件違反

まあ大抵は1回実行するだけで済む話ではあるのですが、しかし無視できる問題でもありません。+ もう少し複雑だったりしてたまにしか契約違反しないプログラムだと、バグに気付かないままリリースしてしまうことだって当然あるわけです。

というわけで、先ほど紹介したCode Contractsなど、一部の契約プログラミング用システムでは、これを補うために、プログラムを実行しない検査手法(静的検査)も用意しています。
静的検査では、実際にプログラムを動かす代わりに、ツールが何かしらの手法でプログラムを解析します。^[3]

先ほどの違反例で言えば、静的検査は以下のような検査をします。^[4]

• withdraw(-10,0) の事前条件は -10 ≥ 0 だからどう見てもアウト

• withdraw の事後条件は balance - amount - 10 ≥ 0 になり、これを balance ≥ amount から導けるかチェック

ちゃんとは説明はしませんが、それぞれの長短を雑にまとめるとこんな感じですね。

	動的検査	静的検査
利点	実行したパターンに対しては誤検出も見逃しも無い	実行や入力をしなくても検査できる
欠点	違反する入力が来ないと検出できない	契約の書き方に敏感

漸近的検査

ここからが本題です。

モチベーション

次に示すコードは、動的検査はうまくいくのに静的検査が通らない例です。

int withdraw(int balance , int amount)
  requires (balance ≥ amount) ensures (result ≥ 0)
{
  return balance - amount;
}

int balance := 100;
balance := withdraw(balance, 30); // balanceが70になる
balance := withdraw(balance, 40); // balance ≥ 0 という情報しかないため事前条件を満たさない

静的検査では、関数呼び出しに対して、契約のみを見ます。 withdraw の返り値は0以上であることしか保証してくれないため、静的検査では「balance は40より小さいかもしれない」と(実際は70であるにも関わらず)思ってしまうわけです。

なんでこんなことが起きるかといえば、事後条件が実際よりも不正確であることが原因です。
ensures (result = balance - amount) などと書けば静的検査が通るようになりますが、つまり関数の実装を2回書いているわけで、もっと複雑な処理や乱数が入ったらどうするのか、という話になります。他人の書いたライブラリとかだと気軽に書き換えるわけにも行きませんしね。

そういう事情のため、既存のツールにおいては静的検査では、確実に間違っていると判断できる部分^[5]に対してのみ警告を出すようになっています。
明らかに間違っている部分はその時点で直して、残りは動的検査するという形です。

この論文が提唱する 漸進的検査(Gradual Verification) では、こういったツールで発生する以下の問題点を解決します。

• 全ての契約を正確に書いても動的検査に任せてしまう場合がある

• 静的検査を通った部分を動的検査でもう一度チェックしてしまう

手法

結論から言えば、以下のようなコードが書けるようになります。

int withdraw(int balance , int amount)
  requires (balance ≥ amount) ensures (result ≥ 0 ∧ ?) // ← "∧ ?" が増えた!
{
  return balance - amount;
}

int balance := 100;
balance := withdraw(balance, 30); // こちらの呼び出しについては動的検査しない
balance := withdraw(balance, 40); // balance ≥ 40 を動的検査

記述としては事後条件の result ≥ 0 が result ≥ 0 ∧ ? に変わっただけです。これは、「実際の返り値は result ≥ 0 よりも強い制約を満たす(けど敢えて書かない)」ことを意味します。

これによって何が起こるかというと、全体を静的検査しても不要な警告が出なくなります。? が関わる部分に対してのみ警告を出さないようにすればよいだけです。
条件をどれくらい詳しく書くかは開発者次第で、

そして、漸進的検査では静的検査時の情報をフル活用し、最低限の部分のみを動的検査するようにします。
1回目の withdraw の呼び出しでは事前条件を満たしていることが静的検査でわかるため動的検査は行いません。

また、2回目の呼び出しでも amount が40であることは静的検査の時点でわかっているため、最初から balance ≥ 40 のみを動的検査します。
まあ、これだけではあんまり旨味を感じないかもしれません。もう少しわかりやすい例だと、 A ∧ B という契約に対して、静的検査によって A は満たすとわかったら、 B のみを動的検査します。

具体的にどうやって実現しているか一言で言うと、 withdraw の契約の静的検査時に最弱事前条件というものを計算するのですが、これの計算過程に一手間加えることで動的検査条件が導き出せるという話です。
論文的にはこの辺りが本題なのでちゃんと説明したかったのですが、時間的制約により割愛させてください。^[6]

感想

名前がずるい。やりたいことの雰囲気はわかるけど具体的に何をやっているかは読まないとわからない感じで、興味をひかれました。
あと、著者らはConclusionで"We have developed the formal foundations"と述べているのですが、そういうパイオニア精神は大好きです。というかそういう論文ばっかり読んでます。

正直、「動的検査と静的検査を組み合わせる」という発想はそんなに珍しい話ではないと思うのですが、それを契約という文脈でこういう形にまとめたのは個人的に面白かったです。
特に、単に ? という式を書けるようにするわけではなく、 ∧ ? という形のみを許すようにしたのは工夫かなと。

他にも似たような話はあったりするのですが、著者らは(関数型ではなく)手続き型言語を想定していることが大事だと主張しています。
また、今回は紹介しませんでしたが、この手法は「静的検査手法を作る→漸進的解析に拡張する」という段階を踏んでおり、拡張方法は割と一般的に書かれているため、他の静的検査手法への応用も期待できそうです。

一方で、静的検査から動的検査へ引き渡す情報の計算がそこそこ重いような気がするので、その辺りって実用的なプログラミング言語に適用するとどうなんだろうという辺りは気になりますね。

漸進的検査を動かせるウェブページも公開されているので、興味のある方は覗いてみてください。
まあ、対象言語が違うので、今回挙げた例とかは試せないのですが。

以上、お粗末様でした。 登録はお早めに。

---

1. 投稿を悩んでいる人たちの投稿へのハードル、という意味で書きましたが、この記事に対するハードルも下がってる気がしますね。それはそれで望ましい話です。

2. ここで result は返り値、つまり balance - amount を表すキーワードです。元論文では balance と書いていますが、こっちの方が正しいはず。

3. 論文では特に 形式手法 による静的検査を考えていますが、あまり気にしなくていいです。ちなみに形式手法とは、プログラムを数学的に理解・表現する手法です。

4. ここでの静的検査は一度に1つの関数定義のみしか見ないような手法を想定しています。まあ契約があるなら関数の境界はそっちに任せたいですよね。

5. 定数しか使っていない場合なんかは確実に検査できます。

6. 研究の面白みで言えばHowよりもWhatの方が大事なので、これはこれでいいかなとも思っていますが、余裕があったら後日加筆するかもしれません。