NuSMVでコンセンサスアルゴリズム (の超一部) をモデル検査する

お知らせ

2019-02-08: もう少しちゃんと書いたので、こっちを見てください https://qiita.com/shinsa82/items/cd4d95c616bf1da852ce

概要

なんとNuSMVに関する最初の記事のようだ。

シンボリックモデルチェッカのNuSMV (http://nusmv.fbk.eu/) を使って、ブロックチェーン実装の1つであるHyperledger Fabricのv1.xで使われているコンセンサスプロトコルの一部を検査してみる、試みの途中である。
なぜFabricを選んだかは聞いてはいけない。

セットアップ

• NuSMVをインストールする。商用でなければZCHAFF付属版でいいと思われる。
• bin/nusmv にパスを通す。

Fabric v1のコンセンサスプロトコル (一部)

クライアントの仕事がやたら多いのが特徴である。

− クライアントは複数のピアにトランザクション・プロポーザルを送る。これにはトランザクションの関数名と引数が書かれている。

• プロポーザルを受け取ったピアはトランザクションをシミュレーション (仮実行) する。
• シミュレーション結果をエンドースメントとしてクライアントに返送する。これにはトランザクションの返り値とworld stateへのread/write setが含まれる。
• クライアントが必要な数のエンドースメントを集めたら、それらをまとめてオーダラーに送る。
• (以下略)

ピアが正しく動作することは盲信できないし、ネットワークが正常であることも必ずしも期待できない。これは分散コンセンサスの一種である。

モデル定義

以下のようなモデルファイルを用意した (なんとsyntax highlightingが可能である)。

fabric1.smv

--
-- Simple version of Fabric endorsement model.
--   all communication are synchronous
--   all peers are non-faulty
--
-- by @shinsa82
--

MODULE main
	VAR
		c: client(3);
		p0: peer();
		p1: peer();
		p2: peer();

	ASSIGN
		next(c.started) := TRUE;

		-- send TX proposals from client to peers
		next(p0.recv_proposal) := c.sent_proposal[1];
		next(p1.recv_proposal) := c.sent_proposal[2];
		next(p2.recv_proposal) := c.sent_proposal[3];

		-- send endorsements from peers to client
		next(c.recv_endorsement[1]) := p0.sent_endorsement;
		next(c.recv_endorsement[2]) := p1.sent_endorsement;
		next(c.recv_endorsement[3]) := p2.sent_endorsement;
		next(c.endorsement[1]) := next(c.recv_endorsement[1]) ? p0.endorsement : c.endorsement[1];
		next(c.endorsement[2]) := next(c.recv_endorsement[2]) ? p1.endorsement : c.endorsement[2];
		next(c.endorsement[3]) := next(c.recv_endorsement[3]) ? p2.endorsement : c.endorsement[3];

	-- eventually get all endorsements (and its negation)
	LTLSPEC F c.got_all_endorsements;
	LTLSPEC G ! c.got_all_endorsements; -- try to find a counterexample

	-- possible to be consensus to 0
	CTLSPEC EF (c.got_all_endorsements & c.decision = 0); 
	-- possible to be consensus to 1
	CTLSPEC EF (c.got_all_endorsements & c.decision = 1); 

MODULE client(N) -- N: number of peers
	VAR
		started: boolean;
		sent_proposal: array 1..N of boolean;
		recv_endorsement: array 1..N of boolean;
		endorsement: array 1..N of 0..1;
		decision: 0..1;

	DEFINE
		got_all_endorsements := count(recv_endorsement[1], recv_endorsement[2], recv_endorsement[3]) = 3;

	ASSIGN
		init(started) := FALSE;
		init(sent_proposal[1]) := FALSE;
		init(sent_proposal[2]) := FALSE;
		init(sent_proposal[3]) := FALSE;
		init(recv_endorsement[1]) := FALSE;
		init(recv_endorsement[2]) := FALSE;
		init(recv_endorsement[3]) := FALSE;

		next(sent_proposal[1]) := started;
		next(sent_proposal[2]) := started;
		next(sent_proposal[3]) := started;

		next(decision) := (endorsement[1] + endorsement[2] + endorsement[3]) >= 2 ? 1 : 0;

MODULE peer
	VAR
		recv_proposal: boolean;
		endorsed: boolean;
		endorsement: 0..1;
		sent_endorsement: boolean;
 
	ASSIGN
		init(recv_proposal) := FALSE;
		init(endorsed) := FALSE;
		init(sent_endorsement) := FALSE;

		next(endorsed) := recv_proposal ? TRUE : endorsed;
		next(endorsement) := recv_proposal ? {0, 1} : endorsement;
		next(sent_endorsement) := endorsed;

MODULE net

モデル概説

• ここではピアの数を3つとして、悪意のあるピアはいないとする。ピアはシミュレーションの結果として0か1を非決定的に返す (実際はFabricのスマートコントラクトで非決定的なコードを書いてはいけない)。クライアントは多数決で合意結果を決める。
• プロセスはsynchronousに動くとする。分散並列システムにおいてはasynchronousに書きたいところだが、NuSMVのv2.5以降では非推奨となったためやむなくsyncに書く。
• ネットワークは常に正常であるとする。

NuSMVにはモジュールの概念がある。SPINのプロセスと思ってもらってもいい。しかしNuSMVはモジュールのモジュール化がいまいちで、他のモジュールの変数にアクセスできるし、モジュール間の通信についても特段の仕組みがないのは上のソースを見ていただくとわかると思う。

ここでは、いわゆるI/O automataをどう表現するかを考慮してモデルを作成した。
モジュールとしてはピアを表す peer とクライアントを表す client、そして必須であるメインの main を用意した。
モジュールの駆動、モジュール間の通信および検査条件の記述を main に担当させており、その他のモジュールはある意味reactiveに動くようにした。例えば main がモジュールインスタンスc (peerモジュール) のstarted変数を操作することによりクライアントをスタートさせている。また peer モジュールのsent_endorsement変数に連動させて client の recv_endorsement を変化させている。

ここでは全ての状態遷移が1 tickで済んでいる。つまり各処理にともなう状態変化は直後のステップにおいて起きる。本来は並列性を表すため、数ステップかかる (ただし無限に終わらないことはない) ように記述するのが通常である。これについては次回以降で説明する。

検査条件

	-- eventually get all endorsements (and its negation)
	LTLSPEC F c.got_all_endorsements;
	LTLSPEC G ! c.got_all_endorsements; -- try to find a counterexample

	-- possible to be consensus to 0
	CTLSPEC EF (c.got_all_endorsements & c.decision = 0); 
	-- possible to be consensus to 1
	CTLSPEC EF (c.got_all_endorsements & c.decision = 1); 

まずLTL式で、いずれは全てのエンドースメントが得られることを確認している。検査結果が true の場合は何もtraceが表示されないので、条件を満たすtrace例を表示させたければ2つめのLTL式のように否定形を与えて反例を出力させればよい。

次にCTL式で、合意結果が0になる場合、1になる場合、がそれぞれ存在することを確かめている。この条件はLTLでは表現できないことに注意する。

なお、NuSMVはマクロ的に使える式を追加することができる。これが DEFINE セクションである。ただし型の部分に来る式を DEFINE で定義することはできない。

検査

nusmv fabric1.smv とすると CTLSPEC や LTLSPEC で指定した条件が検査される。

• 条件を満たす場合には -- specification ... is true と表示される。
• 満たさない場合には以下のように反例となるtraceが表示される:

-- specification ...  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample 
Trace Type: Counterexample 
...

シミュレーション

nusmv -int で起動して、traceを対話的にシミュレートすることもできる。書いたモデルに自信がないときにお勧めである。

ToDo

まずは仮実行が全ピア同時に終わるのはおかしい、ということでそこに非決定性を入れてタイミングをずらす。その際には検証のためにある種のfairness条件を設定することが必要になる。つまりfairness条件を満たすパスに対してだけ検査条件をチェックする、という仕組みになる。これは分散計算のモデル化でよくある考え方である。