2015年09月09日情報システム学専攻・ソフトウェア論講座
関研究室（関 浩之 教授）
本研究室では，最先端のソフトウェアシステムに関する諸問題，特に，信頼性が高く効率も良いソフトウェアはどのようにしたら作成できるかを解明するために，「計算」がもつ基本的な性質を明らかにする基礎研究を進めています．理論研究では，λ算法や項書換え系を基本とする関数型プログラムのモデル，および，有限オートマトンや文脈自由文法等を基本とする形式言語理論をはじめ様々な計算モデルを駆使し，新しいモデルも提案しつつ研究を展開しています．またこれらの基礎理論の応用として，例えば，セキュリティやプライバシ保全に関する実世界の問題解決に取り組んでいます．さらに，現実の問題解決で得られた知見を基礎理論にフィードバックして，理論自体を展開させることにも興味をもっています．本研究室は今後10年先，20年先を見据えた研究に積極的に取り組んでゆきたいと思っています．
【研究テーマ】
現在は下記のテーマについて研究を実施しています．
- CFGより生成能力の大きい形式文法の理論とその応用
- 高信頼性プログラムの自動生成
- モデル検査に基づくソフトウェア検証
- XMLデータの圧縮，情報保存，推論攻撃耐性
- セキュリティ・プライバシーの定量的尺度
- 書換え型計算モデルの解析
【研究環境】
本研究室では基礎となる理論研究とその実装を行っています．理論研究では，対象とする問題に関連した重要な性質の証明や判定・計算アルゴリズムの考案を行います．考案した手法などの実装・評価については主に個人に割り当てられた計算機上で行い，時間がかかる評価実験などは計算専用のサーバマシンを用います． 研究成果は研究会や国内外の会議などで発表を行っています．
輪講（研究に関係する本の輪読）やセミナー（研究の進捗報告や研究発表の練習等）をそれぞれ週に1回程度行っています．セミナー等は計算機数理科学専攻の酒井研究室と一緒に行っています．
ヨーロッパで研究が盛んである項書換え系の分野において，日本も研究が盛んな国の一つです．本研究室は，インスブルック大学（オーストリア），ウィーン工科大学（オーストリア），バレンシア工科大学（スペイン）など海外の研究グループとの共同研究を多く実施しています．
【研究内容の紹介1：言語ベースセキュリティ・プライバシ 】
言語理論の知見をソフトウェアの信頼性向上，特にセキュリティに応用する研究を行ってきました．例を二つ紹介します． 現在，ネットワークからダウンロードしたプログラムを手元の計算機上で実行するということが日常的に行われていますが，それらの中には悪意あるコードが含まれている可能性があります． JDK等の実行時環境では，そのようなコードから情報を保護するためのアクセス制御機能が提供されています．しかし，アクセス制御をプログラムのどの部分でどのように行うのかは設計者の直観に委ねられています．そこで私達は，アクセス制御を含むプログラムが本当に安全かを検証する方法や，セキュリティ要求を満たすようにアクセス制御をプログラムに自動挿入する手法を提案し，ツールを実装してその有効性の評価も行ってきました．
また，共同研究者と協力し，XML文書変換の情報保存性や，XMLデータベースへの推論攻撃に対するセキュリティ耐性の研究を行っています．
最近，k-匿名性，量的情報流，差分プライバシーなど，セキュリティ強度・プライバシー保全の度合を計る新しい概念が提案されていますが，今後はこれらの概念を考慮に入れた研究を行いたいと考えています．
【研究内容の紹介2：定理自動証明によるソフトウェア検証】
近年，Haskell，F#，OCamlなどの関数型プログラミング言語が普及してきています． 関数型言語の計算モデルの一つとして項書換え系（term rewriting system）があります． 項書換え系ではオブジェクトを項と呼ばれる木構造のデータで表現し， 項の対である等式に方向付けをした書換え規則により計算を表現します． 項書換え系では関数型プログラムの性質解析などへの応用をめざして， さまざまな研究が盛んに行われています． 例えば，プログラムの計算が必ず止まることを保証する性質として停止性があります． 関数型プログラムをモデル化した項書換え系が停止性を持つことがわかると， 元の関数型プログラムも停止性を持つことを保証できます．
最近の計算機の性能の向上に伴い， 項書換え系のさまざまな理論に基づいた検証を大規模なシステムへ適用することが能になってきています． 論理式の充足可能性を判定するSATソルバーの性能向上は飛躍的であり， さらに項書換え系の分野ではSATソルバーを利用した停止性証明ツ可ールの開発はますます盛んになっています． また，2008年ごろからHaskellやPrologなどの関数型プログラム， JavaやCのような命令型プログラムの停止性証明への応用などの研究も盛んになり， 書換え理論を実用的なプログラムの検証へ応用する研究が注目されるようになってきました．
研究室では，制約付き項書換え系（constrained term rewriting system）の定理自動証明を利用したソフトウェア検証技術の開発を行っています． C言語で書かれた関数が数学的に書かれた仕様を満たすかどうかを， 関数と仕様を変換して得られる制約付き項書換え系および仕様を満たすことを表す等式を入力として定理自動証明器に与え， 証明に成功することで関数が仕様を満たしていることを保証します． 右図は現在開発中の検証ツールのインタフェースであり， Webブラウザを介して利用できます． 左上のテキストボックスにプログラムを， 左下のテキストボックスには仕様を数式で入力し， 検証を開始するボタンをクリックすると検証結果が右側のテキストボックスに証明過程とともに表示されます． このアプローチでは，検証を行う人が特別な操作，情報を与えることなく 検証を行えるような枠組みの構築をめざしています．
現在は配列などを扱わない小規模なプログラムを対象としていますが， 大規模なプログラムを扱えるように開発を進めることで， 本手法の実用的なソフトウェア検証への応用が期待できます． また，プログラミング演習の課題で作成されたプログラムの検証を支援する応用に向けての開発にも取り組んでいます．