概要 | |
■概要
|
●背景地球規模のネットワーク基盤は整備された。いまや、インターネットに代表されるネットワークインフラストラクチャは、欠くことのできない社会(的)システムとして稼動している。 ネットワーク上において通信を行う場合、メッセージを交換するためのプロトコル(通信手順)が決められる。メッセージを交換し合うノードは(実装がハードウェアかソフトウェアに関わらず)、並行に各々のプロトコル手順を実行するためのプロセスを動かしている。 ネットワークシステムのセキュリティ(=安全性+堅牢性)を保証するためには、そのメッセージ交換時に使用するプロトコルが、仕様通りに正しく動作することを検証しておく必要がある。 例えば、TCPプロトコルにおいて、メッセージ受信誤りが発生した時、送信側へ再送処理を要求する(NACKメッセージ)が、これが送信側でどのように処理されるのだろうか?どのような状況においても、そのTCPフレームの正しい再送処理が実行されるのだろうか?などについての動作検証を考える。 幸いに、TCPプロトコル(特にNACK受信時の再送処理手順)については、RFC仕様によって規定された手順が、様々な方法を用いて「検証」され、所謂「枯れた」プロトコルとして定着した。既にTCP/IPネットワークが稼動を開始し数十年が経過しており、上記のようなクリティカルな誤りは残っていないように見える。 しかしながら、ネットワーク上へ新たなプロトコルを導入する時、あらかじめ仕様検証を行い、手順の誤りをスクリーニングしておくことが求められる。ネットワークシステム上のノードには、プロトコルスタックの更新が容易な場合と、容易でない場合がある。前者はUnixマシンやWindowsPCに代表される更新時のアクセシビリティが高い環境である。後者は、宇宙空間に投入する通信衛星や、携帯電話などのモバイル端末である。更に、Voice-over IP(SIP/H323)をはじめとする次世代プロトコルの多くは、ネットワークゲートウェイ(ルータ)に、ファームウェアの形で供給されることが多く、それに誤りがあった場合、修正に伴う更新作業のコストは計り知れない。 以上の背景と理由により、プロトコル検証を実施することは、有意である。 ●構成この講義・演習マテリアルは、以下の内容について説明し、あるいはツールを用いて演習を実施し、システム検証への理解を深めることが目的である。 part 1 1. 並行プロセスのモデル化 1.1 セルオートマトン(cellular automaton, network automata) 2. プロセスと木(Processes and Trees) 2.1 プロセスの定義(Definition of Process) 3. プロセスの並列化構成(Parallel Compositions) 3.1 並列化構成の定義(Definition of Parallel Composition) 4. Basic LOTOS 4.1 Labelled Transition System (LTS) 5. 設計例(Introductory Applications) 5.1 簡単なプロトコル(Simple Protocol) 6. Full LOTOS 6.1 Abstract Data Type (ADT) 7. プロトコル検証の例(ABP) 7.1 Alternating Bit Protocol (ABP) 付録A.CADPのインストール A.1 インストールの概要 part 2 ※Concurrency and the Asynchronous Circuits part 3 ※Formal Verification by using Model Checking Technology |
wasaki@cs.shinshu-u.ac.jp |