システムソフト（OS）の信頼性、安全性向上に賭ける
コンピュータ科学専攻　前田俊行 助手

型理論とモデル検査理論を組み合わせて
検証ツールなど２つの方法で実現目指す

　コンピューターは、WindowsやLinux、Solarisなどの基本となるシステムソフト（OS）上に各種のアプリケーションソフトを走らせて計算などの仕事をさせるが、問題なのは、OSの安全性や信頼性を確保するのが困難なこと。ここに研究のメスを入れて、OSの高信頼化に挑戦している29歳の若い研究者がいる。コンピュータ科学専攻の前田助手だ。「立派な大きな城に見えるOSも、ポンと押すと、すぐにでも倒れそうな脆さがあるんです。それを改善し、信頼性に裏打ちされたOSづくりに貢献できたら」―この言葉が、前田助手の心意気を表している。

安全性に欠けるC言語の問題点を衝く

　OSは、コンピューターのメモリー資源やCPU資源などを管理する最も重要なソフト。ところが、メモリーをプログラムに割り当てたり、逆にプログラムに割り付けたメモリーを回収したりするメモリー管理機構に問題があると、コンピューターが異常終了したり、機密情報が漏れ出したりする可能性がある。最悪の場合、悪意を持った攻撃者によって乗っ取られてしまう恐れもある。その要因は、主に30年以上も前に設計された「C言語」で構築されているためだ。Java言語やML言語などの数学的理論に裏づけされた安全な言語とは異なり、C言語で構築されたプログラムが実行時に異常動作してしまうかどうかを事前に検証することは非常にむずかしい。「マイクロソフトは、自社のOSなどの安全性向上のために、約2年間で約2億ドルも投じたと言われているほど。まだOSの安全性や信頼性を守る抜本的な解決策は見いだされていないんです」と前田助手は指摘する。

　それはなぜか。メモリー管理機構を記述するのに、C言語よりも適した言語がなかったこと、また、複数のプログラムが同時に実行されるような環境をあまり考慮していなかったことから、プログラムの安全性を厳密に保証、検証することがむずかしかった点が挙げられる。しかも、C言語で記述したOSを安全な言語で書き直すには、膨大なコストがかかる。 たとえば、既存のLinuxカーネルは、C言語などで書かれた700万行ものソースコードから成っている。これを新しい言語で書き直すのは、安全性、信頼性が向上するにしても現実的ではない。これに対し、OS上で実行するWWWブラウザ、メールサーバーなどのアプリケーションソフトの場合は、Java言語など安全な言語が広く使われ始めている。

　「ならば、OS用の安全なプログラミング言語や検証ツールを提供できたら」。前田助手は、研究の視点をこの点にフォーカスした。機械語(コンピューターが直接理解できる言語)や、それに近いアセンブリー言語を安全化することによって、OSの安全性を高め、高信頼化を目指すことが第１点。具体的には、型理論にもとづいた安全な「型付きアセンブリー言語」を、メモリー管理機構などOSの重要な機能を実装できるように拡張、改良し、これを使ってOSを構築する。型理論は、プログラム中の変数やメモリー上のデータがどのような「型」を持つかを解析し、実行時に変数が誤って利用されて異常が発生しないかどうかを検査する方法である。これに加え、既存のOSのソースコードを低コストで検証するために、C言語を型付きアセンブリー言語に変換するツールの研究も進める。

　もう１つは、モデル検査にもとづいた検証ツールの開発。モデル検査は、プログラムが実行時に取りうる状態を網羅的に検査し、異常の発生を検査する手法だ。これによって、複数のプログラムが同時に実行されても、そのプログラム間で不整合が生じたり、デッドロック(異常停止)したりすることなどを防ぐことが可能になる。

技術の本質を探ることの重要さ

　前田助手は、テレビゲーム世代。高校生のとき、数十万円もする高価なパソコンを買ってもらった。ゲームで遊んでいてはバチがあたる、もっと上手に使いこなしたいと考えて中身を探っていくと、プログラミング言語がキーになっていて、OSが全体を支配しているのがわかった。その勉強を始めていくうちに、先人たちがつくり上げたものを追試しているだけではないかと気づく。しかし、それは無駄ではなかった。もはや研究の余地は残っていないかに見えたOSに、安全性というキーワードが欠落しているのを見つけるトリガーになったのだ。

　東大理学部でOSのプログラミング言語研究に着手し、修士・博士課程で型理論などを駆使して、メモリー誤動作などを防ぐ研究を行った。2006年4月に助手になったばかりだが、幸運にもここまで積み上げた研究が、実際に産業界に役立つように仕上げるプロジェクトに発展した。2006年10月にスタートした科学技術振興機構のCREST（戦略的創造研究推進事業）のチーム型研究に取り上げられたのだ。東大（2チーム）、筑波大、慶大、早大の5チームが産業界の協力を得て、5年計画で情報家電や携帯電話などへの組み込み用の高信頼性OSを実用化する研究である。4チームのリーダーは教授が務めるのに対し、前田チームのリーダーは、言うまでもなく前田助手。研究の斬新性が評価されたものと言えるだろう。

　「次の研究のテーマですか。10年、20年のスパンで考えれば、オリジナルOSですかね」。前田助手は笑いながら答えるが、実際は、10年先のことよりも、今のOSの信頼性を確実に上げたいというのが本音に違いない。技術の完成度が高いシステムでも、見方を変えれば、まだまだ新しい風を吹き込めることを、前田助手の研究姿勢は教えている。