| 研究概要 |
本年度は、以下のことを行った。
・振舞モデル検査:移動コードの安全性を保証するための基礎技術として昨年度から研究を行っている振舞仕様を用いたモデル検査(振舞モデル検査)についての研究の一環として,モデル検査をインターネット上で並列処理をするシステムの設計と簡単な実装を行った.具体的には,モデル検査の収束判定に対応する含意式の証明を先読みしていくつかの計算機に割り当て,証明が成功した時点で不要な証明作業の枝刈りとそれに伴う再計算処理を行っている.この際,個々の証明は,代数仕様言語システムCafeOBJ上で開発された自動定理証明器PigNoseを用いて各計算機上で行われる.
・CafeOBJによる認証プロトコルの検証:UNITYとともに用いることで,並行・分散システムおよび実時間システムをCafeOBJで記述・検証してきた.こうした手法が,修正版NSPK(Needham-Schroeder Public-Key)認証プロトコルを例として,セキュリティプロトコルにも適用できることを示すことができた.このことは,CafeOBJとUNITYの組合わせで,広範囲のシステムを扱うことができることを意味しており,本手法の利点である.
・Java仮想機械のCafeOBJ仕様の開発:Java仮想機械のCafeOBJ仕様を作成するにあたって,基本的なデータ構造等の設計をやり直し,より洗練されたモジュール化となった.これらのモジュールは,Javaバイトコード検証器と共通のものであり,ライブラリとして整備することにより,一般的な仮想機械と検証器の仕様記述に応用可能であり,よりモジュール化され再利用性の高い仮想機械の仕様の開発が可能になる.
|
