ソフトウエア科学領域【小川研究室】

プログラムやセキュリティモデルの 解析・検証 教授：小川　瑞史 mail ： メール（クリックするとメールソフトが立ち上がります） URL ： http://www.jaist.ac.jp/~mizuhito

■研究概要

　現在，計算機科学の成熟により現実の問題へ応用可能性を広げています。例えばモデル検査系や定理証明系はその顕著な例であり，現在のCPU開発はそれに大きく依存しています。本研究室は，上記の手法に限らずいろいろな計算機科学の理論的成果を現実の問題へ応用する可能性を追求しています。具体的な理論分野は，組み合わせ理論（特にグラフ理論や順序構造），書換え系，形式言語理論，モデル検査・充足可能性検査，定理証明などであり，応用先はプログラムやセキュリティモデルの検証などを想定しています。その際，SMV，Weighted PDS, miniSAT，yices，E，Isabelle，Maude など既存ツールの使いこなしと，他分野の研究者との積極的な交流による問題発掘を重視しています。

 

■研究のトピック

１．組合せ理論に基づく効率的アルゴリズム

　解析や検証の問題では，しばしば状態遷移や依存関係のグラフ上で結果が収束するまで追跡する不動点計算型のアルゴリズムが用いられます。グラフを代数的に表現できれば，深さ・幅優先探索，分割統治法，動的プログラミングなど典型的な効率的プログラミング手法の適用が可能となります。一般にはそれは不可能ですが，現実の問題に現れるグラフは「木幅」という複雑さの尺度でみて比較的単純なものが殆どです。この観察に基づきレジスタ配置や充足可能性検査を例とした効率的アルゴリズムの研究を進めています。

２．書換系

　１．で用いる木幅が有限なグラフの代数的構成法の完全な公理系，ならびに計算モデルとして病的な振る舞いをする非線形項書換え系の二点に加え，停止性自動証明の理論とシステム開発の研究を進めています。

３．定理証明系を用いた形式的証明

　順序構造に関するKruskal型定理の形式的証明を定理証明系Isabelle/HOLを用いて進めています。その第一歩としてHigmanの補題のopen inductionによる形式的証明を進めています。これらの実例を通して，古典的証明（特にZornの補題を用いたもの）の計算的な意味を明らかにしたいと考えています。

４．モデル検査に基づくJavaプログラム解析

　プログラム解析を抽象化とモデル検査とみなすことができます。現在，動的に定まるJavaのポインター（オブジェクトやフィールド）を解析するPoints-to解析を対象として，プッシュダウンモデル検査を用いた定式化と実装を進めています。この実装には中間言語への変換系SOOT およびプッシュダウンモデル検査ライブラリWeighted PDSを用いています。このような既存のツール類をうまく組み合わせて用いるセンスは重要と考えています。

５．セキュリティプロトコルのモデル検査

　セキュリティプロトコルのモデル検査による検証の研究を進めています。プロセス代数によるセキュリティプロトコルの記述を行い，プロトコルの実行に必要な部分だけにメッセージを抽象化することで，有限モデル検査による検証を実現しました。さらに代数仕様記述処理系Maudeにより実装しています。

６．形式言語理論に基づくモデル検査の拡張

　プッシュダウンオートマトンを拡張したスタックオートマトンや，実時間概念を含む時間オートマトンなどを対象としたモデル検査の拡張を研究しています。スタックオートマトンは60年代に提案され忘れ去られた概念であり，温故知新を大事に考えています。

 

■今後の研究の方向

　上記トピックに加え，他分野の問題の証明や検証を積極的に行いたいと考えています。

 

■代表的な著書・論文

• Ken Mano, Mizuhito Ogawa : Unique normal form property of compatible term rewriting systems -A new proof of Chew's theorem-, Theoretical Computer Science, 258(1-2), pp.169-208, 2001.
• Mizuhito Ogawa : A Linear Time Algorithm for Monadic Querying of Indefinite Data over Linearly Ordered Domains, Information and Computation, Vol.186, No.2, pp.236-259, 2003.
• Mizuhito Ogawa : Well-Quasi-Orders and Regular Omega-languages, Theoretical Computer Science, 324(1), pp.55-60, 2004.
• Guoqiang Li, Mizuhito Ogawa, On-the-fly Model Checking of Fair Non-repudiation Protocols, 5th International Symposium on Automated Technology for Verification and Analysis, ATVA07, LNCS 4762, pp.511-522, 2007.