- This Page
- Home
- 研究内容
Main Contents
高階モデル検査とそのプログラム検証への応用
モデル検査は，検証したいシステム（ハードウェアやソフトウェア）を有限状態遷移システム（またはプッシュダウンシステム）としてモデル化し，その状態を網羅的に探索することによって，与えられた性質を満たすかどうかを検証する手法です．もともとはハードウェアの検証技術として発展してきましたが近年ではソフトウェア検証にも応用され，2007年に発案者のClarkeらがチューリング賞（コンピュータ科学におけるノーベル賞に相当）を受賞するなど注目を集めています．
本研究室では従来のモデル検査を拡張した高階モデル検査とそのプログラム検証への応用について研究しています．これは，検証対象のシステムを有限状態システムではなく，高階再帰スキームと呼ばれる無限状態を記述できる文法で記述し，その性質を検証するもので，従来のモデル検査を包含し，高レベル言語で記述されたソフトウェアの検証に適しています．本研究室では2009年に世界初の高階再帰スキームのモデル検査器を実現し，現在それを利用したソフトウェア検証器の構築に取り組んでいます．
自動定理証明器を用いた依存型型推論
依存型とは通常の型システムでは表現できないような、複雑なプログラムの性質を表現する型です。例えば、ML言語などの通常の型システムでは整数配列は「int array」、としか表現できませんが、依存型システムでは{u : int array | length(u) = 10}（長さが10の整数配列）など論理式を含んだ型で、精密なプログラムの性質を表現できます。自動定理証明器の技術などを利用し自動的に依存型を推論する研究を行っています。
セキュリティプロトコルの検証
ネットショッピングなどの電子商取引や電子投票などでは，「暗号通信プロトコル」と呼ばれる暗号を用いた一定の通信手順に従ってクレジットカード番号などの機密情報をやりとりしています．そのような暗号通信プロトコルに誤りがあると機密情報の漏洩やサーバの乗っ取りなどの危険性があります．そこで，本研究室では暗号通信プロトコルの正しさをコンピュータを用いて自動検証するための手法について研究を行っています．
型に基づく並行・分散プログラムの解析
並行・分散プログラムを正しく記述することやデバッグを行うことは，逐次プログラムの場合に比べて困難です．そこで，通常の型システムを拡張することにより，並行・分散プログラム中の通信や同期が正しく記述されているかをプログラム実行前に解析するための型システムの研究を行っています．この型システムを用いると，プログラマが必ず成功してほしいと思っている通信や同期が（デッドロックやライブロックなどがおこらずに）実際に必ず成功するかどうか，あるいは一定時間以内に成功するかどうかをプログラム実行前に解析することができます．これにより，型検査を通ったプログラムは，例えば（１）クライアント・サーバモデルにおいて，サーバはクライアントからの要求をいずれ受理し，その後いずれクライアントに返事を返す，（２）ロックを獲得しようとしたプロセスはいずれ必ず獲得することができ，ロックを獲得後はいずれ必ずロックを解放する，といった性質を満たすことが保証されます．この研究をもとに TyPiCalというプログラム解析ツール を作成したのでこちらもご覧下さい．
双模倣と論理関係によるプログラム等価性の検証
あるプログラムXが他のプログラムYと「同じように振る舞う」という性質（プログラムの等価性）は，「プログラムの意味を理解する」という以外にも，小さなプログラムを組み合わせて大きなプログラムを作るときや（抽象型など），プログラムが扱う情報の保護を考えるときに（暗号化や情報流解析など），重要になる性質です．しかし，XとYを単独で実行した場合だけでなく，他のプログラムZと組み合わせたときにも「同じように振る舞う」ことの検証は容易ではありません．Zとして考慮しなければならないプログラムは無限に存在するからです．我々は，関数型言語や並行言語など様々なプログラミング言語において，「双模倣」「論理関係」といった手法によるプログラム等価性の検証について研究しています．この研究は国内や欧米でも注目され，様々なグループにより追従ないし関連する研究がなされています．
型システムを用いた XML 処理プログラムの効率化
| プログラムの可読性・開発効率 | メモリ効率 | |
|---|---|---|
| 木構造処理 | ○ | × |
| ストリーム処理 | × | ○ |
さまざまなデータを表現するための統一規格として，XMLが広く使われるようになっています．それに伴って，XMLを入力として計算を行うXML処理プログラムが多く開発されています．現在XML処理プログラムを作るための手法として，木構造処理手法とストリーム処理手法の二つの方法が多く使われていますが，この二つの手法には上の表に示したようなトレードオフが存在します．そこで，この二つの手法の長所を併せ持つ手法として，木構造処理プログラムをストリーム処理プログラムに自動変換する方法を設計しました．この新しい手法では，木構造処理プログラムのうちストリーム処理に変換できる部分を検出するために，順序付き線形型を用いた型システムを使用しています．この手法に基づいたXML用ストリーム処理プログラム生成器X-Pを作成しました．
型情報を利用した静的メモリ管理
プログラム実行中に必要となるデータを格納しておくためのメモリ領域の管理のことをメモリ管理と言います．C言語では，プログラマが明示的にfree, mallocという命令を用いてメモリ領域の確保，解放を行いますが，これを間違えると予測不能なバグにつながります．一方，MLやJavaではガベージコレクション(GC)という手法によって実行時のメモリ状態を見て不要になったメモリ領域を自動で回収しますが，GCによってプログラムの実行が一時的に止ったりすることがあります．「型情報を利用した静的メモリ管理」では，プログラムを実行前にあらかじめ解析しておいて，C言語のfreeやmallocの操作を自動的に挿入します．人間がfreeを挿入するのと異なって間違えることがなく，またGCと違って途中でプログラムを一時停止する必要がないなど効率のよいメモリ管理ができるというメリットがあります．ロボットや携帯電話などメモリの少ない組み込みシステムに向いているメモリ管理手法です．
Javaバイトコードの検証のための型システム
Javaのソースコードは通常，JavaバイトコードにコンパイルされJavaバーチャルマシンにより実行されます．しかし，ネットワーク上に提供されているバイトコードなどは，必ずしも信頼できるものであるとは限りません．Javaバイトコード検証器は，バイトコードを実行前に静的に検査することで正しく実行されないコードを検出し排除しています．しかし，現行のJavaバイトコード検証器で検証できる性質は，各命令のオペランドが適切な型を持つこと，分岐命令先が同じメソッド内に存在すること，各プログラムポイントでオペランドスタックは同じサイズを持ち含まれている値の型は変わらないことといった最低限のものに限られています．そこで我々は先進的な型システムを使って現状より強い性質を検証する方法の研究を行っています．これまでに，Javaバイトコードのロックの使用法（獲得したロックを必ず解放するかどうか）や情報流（機密情報を外部に漏洩しないかどうか）を検証する手法を確立し，それに基づいてJavaバイトコード検証器を拡張しました．