COE Research Monograph Series

COE Research Monograph Series, Vol. 1「オブジェクト指向理論による ファイアウォールサーバの検証」
矢竹　健朗

B5判　200ページ
ISBN4-903092-04-6

※非売品です。入手を希望される方は，jaist-p@kagasaisei.co.jpまでご連絡下さい。

本書のテーマは，定理証明によるオブジェクト指向分析モデルの検証である．定理証明は，モデル検査と並び，近年，情報産業界でも注目されつつあるシステム検証技術の1 つである．我々は，定理証明器HOL においてオブジェクト指向モデルを検証するためのツールObjectLogic を実装した．本書では，ObjectLogic の紹介，及び，ファイアウォールサーバの検証事例について述べる．

　情報システムが社会インフラとなっている現在，情報システムの欠陥が社会に甚大な被害をもたらすようになっている．最近では，銀行システムや証券取引システムのダウンが記憶に新しい．情報インフラの脆弱性は，単に企業の損失だけでなく，国家の信頼性の低下をも招いてしまう．我々が安全に，安心して暮らせる社会を構築するためには，情報システムが正しくつくられ，要求仕様通りの動作をすることを保証する必要がある．
　これまで，システムの正しさの検証は主にテストによって行われていた．テストとは，システムに対して具体的な入力を与え，予期される結果が出力されるかどうかを確認する手法である．テストの問題点はそのカバレッジを100%にすることが不可能な点である．つまり，システムの入力値は一般に無限であり，それらのケースを一つづつ確認していくことは理論的に不可能である．確認されなかったケースについてはシステムの穴となりうる．テストのもう1 つの問題点として，ある程度システムが完成してからでないと行えないことが挙げられる．実装段階で発見されたバグの修復には大きなトラックバックが発生する．最悪の場合，一からやり直しということもありうる．また，発見されない場合は，製品に欠陥をもたらし，回収や事故による大きな金銭的損害，あるいは人的損害が生じてしまう．
　これを克服する手法として最近では，厳密な数学に基づく検証法が注目されつつある．代表的なものは，モデル検査，定理証明である．これらはいずれも隙間のない，網羅的な検証が可能である．モデル検査ではシステムの振る舞いを有限状態機械によって表し，探索アルゴリズムによりシステムのとりうる全状態の検査を行うことが可能である．定理証明ではシステムに出現するデータ型に対し帰納法を適用することにより，すべての値に関して求める性質が成立することを証明可能である．これらの検証法を分析段階において適用することにより，欠陥を早期発見することが可能である．
　我々はこれまでに，定理証明に基づく検証法として，高階述語論理に基づくオブジェクト指向分析モデルの検証ツールObjectLogic を実装した．ObjectLogic では，定理証明器HOL[2] に実装されたオブジェクト指向理論において，モデルが要求仕様を満たすことを検証することが可能である．また，関数型言語moscow ML[3] においてモデルのシミュレーション実行も可能である．コストの高い定理証明に先立ち，比較的コストの小さいシミュレーション実行によってできる限りバグを取り除くことにより，検証プロセス全体でのコ ストを削減することができる．実際の製品の論理的な振る舞いを実行可能モデルとして構 築することは，特に大規模システムの場合，システム全体の振る舞いを把握するために有 用である．