抽象モデル検査とその応用

1999 年度 実績報告書

• 研究課題/領域番号: 11480062
• 研究種目: 基盤研究(B)
• 研究機関: 東京大学
• 研究代表者: 萩谷 昌己 東京大学, 大学院・理学系研究科, 教授 (30156252)
• 研究分担者: 山本 光晴 千葉大学, 理学部, 助手 (00291295) ; 高橋 孝一 電子技術総合研究所, 主任研究官 ; 玉井 哲雄 東京大学, 大学院・総合文化研究科, 教授 (60217172)
• キーワード: 検証 / モデル検査 / 抽象解釈 / 定理証明 / グラフ探索 / 並行ゴミ集め / セキュリティ

研究概要

本年度の主な成果は以下の通りである。
抽象モデル検査の手法に関しては、従来から提案している並行ゴミ集めのための抽象化をより一般的にする試みを行った。この抽象化ではヒープが抽象セルの集合によって表現される。抽象セルはリンク先のセルの色、レジスタからの(直接)到達可能性、灰色セルからの到達可能性などの属性を持っているが、これらの属性を普遍的に表現するために、セルから前方および後方への連結状況を表現する正則表現を用いる方法を考案した。この方法により、適切な正則表現を与えれば種々の抽象化を自動的に得ることができる。
抽象モデル検査の応用としては、セキュリティ・プロトコルの検証のためのnonce解析の研究を行った。Needham-Schroederなどのセキュリティ・プロトコルを安全性の本質は、プロトコルのステップにおいて生成されたnonce(新しい乱数)が、以後の実行過程においてどのように漏れ出し得るかを解析することに他ならない。本研究では、このようなnonce解析を抽象モデル検査として定式化した。
モデル検査に用いたアルゴリズムの探索に関しては、従来から試みている並行ゴミ集めのアルゴリズムの探索をより完璧なものとし、結果として、on-the-flyとその二つの変種、snapshoptとその変種を発見した。また、相互排除のためのDekkerのアルゴリズムとPetersonのアルゴリズムの発見を試みた。特殊な状況(プロセスの実行速度が同じ)におけるDekkerのアルゴリズムの変種を発見した。
モデル検査アルゴリズムの検証に関して、従来から定式化および形式化を行っているグラフ探索アルゴリズムの検証の研究を発展させ、グラフのノードに抽象化関係を導入することにより、covering graph constructionなどの抽象モデル検査のアルゴリズムを包含する枠組を定式化した。

研究成果

• [文献書誌] 山本光晴,高橋孝一,萩谷昌巳: "モデル検査アルゴリズムの検証について"日本ソフトウェア科学会第16回大会論文集. 337-340 (1999)
• [文献書誌] 戸田洋三,萩谷昌巳: "タクティクからのプログラム抽出とその応用"情報処理学会論文誌プログラミング. Vol.40 No.S1G4(PRO3). 21-32 (1999)
• [文献書誌] Koichi Takahashi,Masami Hagiya: "Proving as Editing HOL Tactics"Formal Aspects of Computing. Vol.11 No.3. 343-357 (1999)
• [文献書誌] Naoyasu Ubayashi,Tetsuo Tamai: "An Evolutional Cooprrative Computation Based on Adaptation to Environment"Proc.Asia Pacific Software Engineering Conference'99. 334-341 (1999)
• [文献書誌] 萩谷 昌巳: "検証系を用いたアルゴリズムの発見"情報処理学会第41回プログラミング・シンポジウム報告集. 9-19 (2000)
• [文献書誌] 木下佳樹,高橋孝一,萩谷昌巳: "安全性の抽象モデル検査について"日本ソフトウェア科学会第2回プログラミングおよびプログラミング言語ワークショップ. (印刷中). (2000)