概要

■概要

1.背景

2.構成

 

参考資料・リンク集

 

●背景

地球規模のネットワーク基盤は整備された。いまや、インターネットに代表されるネットワークインフラストラクチャは、欠くことのできない社会(的)システムとして稼動している。

ネットワーク上において通信を行う場合、メッセージを交換するためのプロトコル(通信手順)が決められる。メッセージを交換し合うノードは(実装がハードウェアかソフトウェアに関わらず)、並行に各々のプロトコル手順を実行するためのプロセスを動かしている。

ネットワークシステムのセキュリティ(=安全性+堅牢性)を保証するためには、そのメッセージ交換時に使用するプロトコルが、仕様通りに正しく動作することを検証しておく必要がある。

例えば、TCPプロトコルにおいて、メッセージ受信誤りが発生した時、送信側へ再送処理を要求する(NACKメッセージ)が、これが送信側でどのように処理されるのだろうか?どのような状況においても、そのTCPフレームの正しい再送処理が実行されるのだろうか?などについての動作検証を考える。
仮に、もし、この動作のための実装に誤りが含まれていたならば、TCPレイヤ上の殆どのノードは、NACKを受信しても正しく再送処理が行えないだろう。結果、ネットワークシステムとしての可搬性の低下を招くであろう。

幸いに、TCPプロトコル(特にNACK受信時の再送処理手順)については、RFC仕様によって規定された手順が、様々な方法を用いて「検証」され、所謂「枯れた」プロトコルとして定着した。既にTCP/IPネットワークが稼動を開始し数十年が経過しており、上記のようなクリティカルな誤りは残っていないように見える。

しかしながら、ネットワーク上へ新たなプロトコルを導入する時、あらかじめ仕様検証を行い、手順の誤りをスクリーニングしておくことが求められる。ネットワークシステム上のノードには、プロトコルスタックの更新が容易な場合と、容易でない場合がある。前者はUnixマシンやWindowsPCに代表される更新時のアクセシビリティが高い環境である。後者は、宇宙空間に投入する通信衛星や、携帯電話などのモバイル端末である。更に、Voice-over IP(SIP/H323)をはじめとする次世代プロトコルの多くは、ネットワークゲートウェイ(ルータ)に、ファームウェアの形で供給されることが多く、それに誤りがあった場合、修正に伴う更新作業のコストは計り知れない。

以上の背景と理由により、プロトコル検証を実施することは、有意である。


●構成

この講義・演習マテリアルは、以下の内容について説明し、あるいはツールを用いて演習を実施し、システム検証への理解を深めることが目的である。


part 1

1. 並行プロセスのモデル化

1.1 セルオートマトン(cellular automaton, network automata)
練習問題1-1
1.2 ペトリネット(Petri net)
練習問題1-2
1.3 プロセス代数仕様(BLA : Basic-LOTOS oriented Algebra, CCS, CSP)
練習問題1-3

2. プロセスと木(Processes and Trees)

2.1 プロセスの定義(Definition of Process)
2.2 プロセス木表現(Process Trees)
2.3 木の等価性(Tree Equivalences)
2.4 木の操作(Operations on Process Trees)
2.5 諸定理(Laws)
練習問題2-1

3. プロセスの並列化構成(Parallel Compositions)

3.1 並列化構成の定義(Definition of Parallel Composition)
3.2 並列化プロセスの例(Parallel Process Examples)
3.3 諸定理(Laws and Propositions)
練習問題3-1

4. Basic LOTOS

4.1 Labelled Transition System (LTS)
4.2 toolbox による LTS生成
4.3 Basic LOTOS による操作の記述例
4.4 等価性のチェック
4.5 再び自販機の例
練習問題4-1
★演習問題1

5. 設計例(Introductory Applications)

5.1 簡単なプロトコル(Simple Protocol)
5.2 Alternating Bit Protocol (ABP)
5.3 通信路誤り無しの場合
5.4 通信路誤りありの場合
練習問題5-1
★演習問題2

6. Full LOTOS

6.1 Abstract Data Type (ADT)
6.2 Full LOTOS
6.3 Full LOTOS版 "Simple Protocol"
6.4 Full LOTOS版 "通信路誤り無しABP"
練習問題6-1
★演習問題3

7. プロトコル検証の例(ABP)

7.1 Alternating Bit Protocol (ABP)
7.2 通信路誤りありABPのFull LOTOS仕様
7.3 ABPのobservationalな仕様(SERVICE)
7.4 等価性の検証例
練習問題7-1
★演習問題4

付録A.CADPのインストール

A.1 インストールの概要
A.2 Linux環境へのセットアップ
A.3 bashシェル環境変数の設定
A.4 ライセンスファイルの取得と設置
A.5 アプリケーション起動確認
その他のセットアップ時の参考資料


part 2

※Concurrency and the Asynchronous Circuits


part 3

※Formal Verification by using Model Checking Technology


wasaki@cs.shinshu-u.ac.jp
Copyright(c) Katsumi Wasaki. All rights reserved.