計算機ネットワーク構成の設計,検証及び管理のための形式手法

点击翻译按钮获取中文摘要

ネットワーク構成/経路の設計において、セキュリティの確保などを目的としたパケットフィルタは重要な要素の一つであり、今年度は、その設計、記述、検証の問題を研究した。1.要求仕様レベルの記述通信プロトコルの知識を仮定しない、サービスの利用/提供とその禁止を記述するようにした。ネットワーク構成の抽象度に対応して、段階的詳細化が可能である。一般に相反する条件が含まれるので、must permit、must deny、may permit、may denyの条件クラスを設定した。また、must、mayだけでなく任意の深さの優先度を考えることができる。2.実現仕様レベルの宣言的記述と操作的記述パケットフィルタは、通過するパケットの属性(始点、終点、フラグ等)を見て通過の許可/不許可やログの有無を決定するシステムであるので、1.の要求仕様に対して、ネットワークサービスを実現する通信プロトコルの知識に対応するルールベースの導出規則によって、論理関数による仕様の表現が生成できる。その際、例えばmust permit条件とmust deny条件とが矛盾していれば、それは1.の仕様が実現不可能なものであったことがわかる。複数フィルタの合成/分解や、包含/等価性の検証などはすべて論理関数の計算に帰着できる。また、実際のパケットフィルタでは、動作を決定する条件(マッチング規則)をある順序で逐次適用するものであるから、宣言的な論理関数から、積項の列としての、操作的記述を生成できる。そして、この規則列から、元の論理関数としての意味を変えずに、より望ましいフィルタ(実行効率やメモリ効率など)を探していくための等価変換則を導いた。3.現実のルータやファイアウォールでの記述言語との対応このような汎用的なパケットフィルタ記述が、現実のルータやファイアウォール(CISCO、富士通、IPFilterなど)でのパケットフィルタ記述にマッピングできることを検証した。