米澤研究室 助手さんアンケート


回答者:住井助手

Q 現在、どのような研究をなさっていらっしゃるのですか?

一言でいうと「プログラミング言語システム」です。もう少し長ったらしく言えば、「逐次/並列/分散プログラミングの理論・実装・応用」でしょうか。ここでいう「プログラミング」はかなり広い意味で、たとえばインターネットを介した広域分散計算の研究なども行っています。

プログラミング言語というのは、コンピュータに「あれをしろ」とか「これをしろ」とか指示するための人工言語です。世間では各種のマシン語, アセンブリ, C, C++, Java等が有名ですが、研究のレベルではScheme, ML, Haskellなど、より進んだ言語も使われています。

「コンピュータ、ソフトがなければただの箱」といわれるように、どんなにすごいコンピュータでも、プログラムを与えないと何もしてくれませんし、プログラムが間違っていたら間違ったことをしてしまいます。皆さんもパソコンを使っていて、「このプログラムは不正な処理をしたので強制終了します云々」みたいなエラーが出て、それまで書いていた文章等が闇に消え去ってしまう、といった経験はないでしょうか。あるいは、もっと深刻な問題として、コンピュータがウィルスに感染して動作しなくなったり、悪人にのっとられてクレジットカード番号等の個人情報が漏洩してしまったり、といった事件も多発しています。このような問題のほとんどは、オペレーティングシステム, ブラウザ, メーラ, ワープロ等のプログラムの間違い(バグ)が原因です。

今の世の中では、そういう間違いを減らすために

  • プログラムを作る人(プログラマ)が、できるだけ気をつける
  • 作ったプログラムは、頑張ってテストする
  • テストして問題が見つかったら直す
  • 見つかる問題が少なくなったらリリースする
  • リリースした後に問題が見つかったら、また直したバージョンを出す

という、とても場当たり的なアプローチがとられています。結果として、ソフトウェアを開発する現場の人々には大変な負担がかかっていて、デスマーチ(死の行進)などといわれたりするほどです。

我々は上述のような問題を、場当たり的なやり方ではなく、正確な知識・理解と慎重な考察にもとづいてシステマティックに解決するべく、次のようなテーマで研究を行っています。

  • 複雑な処理が簡単に記述でき、間違いが起きにくい言語
  • ある種の間違いは決して起きないことが、数理論理学的に証明されている言語
  • 従来の言語において、プログラムのいろいろな間違いを防ぐ、あるいは見つけてくれるような仕組み
  • プログラマがあまり頑張らなくても、プログラムを速くしてくれるような仕組み

Q 研究室で行われているプロジェクトについて教えて下さい。

2002年2月現在では、以下のようなプロジェクトが進行しています。ただし、一つ一つのテーマはそれなりのペース(数ヵ月〜数年)で少しずつ変わっていきますので、最新情報を詳しく知りたい人は

  • 関係者(住井田浦さん小林さんなど)のホームページを見る
  • 卒論・修論の発表(9月上旬および2月上旬)を聞きに来る
  • アポをとって見学に来る

等するのが良いと思います。(なお、研究室全体のホームページはあまりきちんと更新されていません。皆が研究で忙しいので…)

(1) 安全なプログラミング言語にもとづくコンピュータアーキテクチャ

現在のコンピュータは、マシン語やC言語といった、古典的な低水準の言語で記述されたプログラムを実行するために設計されているのが普通です。たとえば、それらの言語は様々な意味で「安全ではない」ので、プログラムに間違いがあったときの被害を少しでも小さくするために、CPUやオペレーティングシステムにいろいろなセーフティネットが張り巡らされています。

ところが、そのようなセーフティネットはあくまで「被害を少しでも小さくする」だけであって、根本にあるプログラムの間違いを減らすわけではありませんから、コンピュータウィルスや不正侵入を防止するのに十分ではありません。そればかりか、コンピュータの設計が複雑になったり性能が低下したりする原因にもなっています。

そこで我々は、数理論理学的な基礎理論(「操作的意味論」や「型理論」など)にもとづき、ある特定の意味で「安全である」と証明された言語を中心に、信頼できるコンピュータシステムの設計方式を確立しよう、という研究をしています。

このプロジェクトはまだ始まったばかりですが、とりあえず今は「Linux/TAL」というシステムを、修士二年の前田君が作ってくれたところです。このLinux/TALは、オープンソースのオペレーティングシステム(のカーネル)として有名なLinuxを改造して、Typed Assembly Language (型付きアセンブリ言語)で提供されたユーザプログラムをカーネルモードで実行できるようにしたシステムです。これにより、ユーザプログラムは安全かつ従来より高速に、ファイル操作やネットワーク通信といったカーネルの機能を利用できます。

今後の方向としては、さらなる改造による性能の向上や、従来の保護機構が十分ではない携帯電話やPDAへの応用などがあります。

(2) Fail-SafeなC言語処理系

上のほうで「C言語は安全でない」と書きましたが、これは本当はあまり正確な表現ではありません。確かに今の世の中に出回っているC言語の処理系は安全でないのですが、C言語の仕様(いわゆるANSI C)をよく気をつけて読むと、(ある特定の意味で)安全な処理系を実装することも、理屈としては可能であることがわかります。しかし、そのような処理系は今まで「遅すぎて使い物にならない」と信じられてきました。

ところが、最近ではプログラム解析手法の発展やハードウェアの性能向上により、そういう安全な実装がそれなりの効率で現実に可能となってきました。そこで、実際にそういう処理系を開発しよう、というのがこのプロジェクトです。

ただし、C言語はTALやMLと違って、そもそも安全であることを目指して作られてはおらず、「プログラムが(ある種の)誤りを決して含まない」ことを事前に保証することは原理的に不可能です(これは計算不可能性という議論にもとづいて厳密に証明できます)。そこでこの研究ではちょっと妥協して、「プログラムを実行している<b>最中に</b>検査をして、バッファオーバフローや互換性のない型変換などの誤りが起きたら(暴走するのではなく)すぐに停止する」という方針を採用しています。fail-safeというのは、この「何か変になったら、暴走するのではなくすぐに停止する」というポリシーのことです。

このプロジェクトも始まったばかりなのですが(そもそも私が助手になったのがついこの間なので)、博士一年の大岩くんが、一部の実装と簡単な予備実験をしてくれたところです。それによると、適当な最適化を利用すれば、普通の安全でない処理系と比較した速度低下は数十%〜数倍程度でした。現実社会では速度よりもセキュリティ等のほうが深刻な問題となっていることを考慮すれば、(使い道にもよりますが)そんなにひどくはないといえるでしょう。

今は、proof carrying codeという数理論理学的なアプローチにもとづいて、(ちょっとややこしい言い方になりますが)「上のような実行中の検査のやり方が正しいことを、実行前に確かめる」方式を開発しています。

(3) インターネットを利用した動的再構成可能な広域分散計算方式

これは東大工学部講師の田浦さん(前米澤研助手)を中心に進行している共同研究で、物理的・地理的に世界中に分散した多数のコンピュータを利用する計算(global computing)のためのプラットフォームを構築しよう、という研究です。究極の目標は、

インターネットを一つのコンピュータのように使う

ことにあります。NapsterやGnutellaなどのいわゆるP2P (peer-to-peer)方式によるファイル共有が、利用方法によっては著作権の関係で社会問題になるほど強力であることは、報道等で皆さんもご存じだと思います。そのようなP2P のパワーをファイル共有だけでなく、「計算一般」に応用することを可能にしよう、というプロジェクトです。

ここで鍵となるのは、今までのただの並列・分散計算と違って、global computingでは計算に参加するコンピュータが頻繁に増減するので、たとえプログラムを実行している最中であっても、容易に構成を変更できる必要がある、という問題です。また、よくあるクライアント/サーバ方式のような、ボトルネックが発生しやすい方式も×です。さらに、ファイアウォールのような現実の制限にも、きちんと対応する必要があります。このプロジェクトでは、そのような問題を解決するタスク割り当てやメッセージ配送の方式を研究しています。

(4) リソース使用解析

これは「ファイルをopenしたら、いずれはcloseする」とか「UNIXのソケットに対し、open, bind, connect, shutdown, etc.が正しい順に行われる」とか、一般に「プログラムにおける計算資源に対する操作が、順序や回数も含めて正しく実行される」ことを事前にチェックしてくれるような型システムを構成しよう、という研究です。東工大助教授の小林さん(前々米澤研助手、元東大理情講師)と京大講師の五十嵐さん(米澤研OB、元東大教養学部助手)を中心とする共同研究で、修士二年の浜中君が一つの実例としてJavaバイトコードを対象とした型システムを定義しました。今後は他の言語を対象としたり、デバッグ, セキュリティ, メモリ管理など様々な用途に応用したり、といった発展が期待できます。

(5) 暗号化と抽象化

コンピュータシステムにおいて、暗号化は情報秘匿のもっとも基本となる手段ですが、たとえ暗号系自体が完璧でも、それを利用した通信プロトコルやプログラムに間違いがあるせいで、クレジットカード番号等の秘密情報が漏洩してしまうという問題が頻発しています。そこでこのプロジェクトでは、プログラミング言語の世界で大昔から研究されてきた「抽象化」という情報秘匿の手法と暗号化との関係を研究し、抽象化に関する理論を暗号化に関する議論に応用することを目標としています。現在までに、λ計算という体系における抽象化と暗号化の関係についての理論を構築し、それを利用していくつかのセキュリティプロトコルが実際に秘密を漏洩しない(あるいは漏洩してしまう!)ことを証明しました。

このプロジェクトは米ペンシルバニア大助教授のBenjamin Pierce氏との共同研究です。余談ですが、米澤研は海外の研究者とかなり密接な交流があって、研究室の学生が一時的ないしは恒久的に留学することもよくあります(私自身もそうでした)。

Q 所属していらっしゃる研究室ならではの特徴がありましたら、教えて下さい。

僕個人としては「楽で楽しい、けれどもレベルの高い研究室」を目指しています。どれぐらい成功しているかは皆さんの判断におまかせしますが…(笑)

「楽な」というのは、もちろん「何も研究しないで遊んで暮らそう」という意味ではなくて、「徹夜とか無理をしないで、普段からやるべきことをやれるようなシステム」です。そのために、企業人事のマニュアル本(笑)なども参考にしながら、少人数ミーティングとかペア研究(pair programmingという開発手法のパクリです)とか人間負荷分散表とか、いつもいろいろと試行錯誤しています。

「楽しい」というのは、以下のような意味です。そもそも勉強や研究というものは、「今まで自分がわからなかったことがわかる」とか「今まで誰も思いつかなかったことを考える」とか、探検や開拓と同じで、本来は楽しいことのはずです。それなのに、学校教育が悪いのか、どうも「親や先生や助手にいわれて、嫌々ながら勉強・研究している」という人が目立つように思います。なので、ミーティング, 論文推敲, 発表練習等の場を通じて、少しでも研究の楽しさが伝わるように頑張っているつもりです。

最後に、「レベルの高い研究室」というのは客観的事実:-)です。修士・博士課程の学生はもちろん、卒論生でも国内外の学会に多数の論文を投稿し、倍率が2倍〜5倍にも及ぶ厳しい査読を経て採択されています。「研究室の中でOKが出れば、国内の学会には間違いなく通る」といわれるほどです。ただし、上で述べたように、そのために大変な努力が必要というよりは、ミーティング等の活動に普通に参加していれば、(そもそもこの学科/専攻に進学/入学できた人なら)誰でもそれぐらいは当たり前にできるようになる…ことを目指しています。逆に、およそコンピュータやプログラミングの勉強や研究が嫌いで、家に引き籠もって大学に来たくもない、という人にはあまり向かないかもしれません。

Q 研究室を目指す学生にひとことお願い致します。

コンピュータの世界は基礎が脆弱なまま、その場その場の勢いだけでここまで来てしまったような面があると思います。勢いがあることは悪いことではありませんが、結果として2000年問題やコンピュータウィルスのような問題が続出したり、一部では詐欺のような「技術」や企業の宣伝文句が横行しているのも現状です。今の世の中で流行っている「最新技術」が、研究としては数十年の昔に済んでいる話である、というケースも少なくありません(というか、多くのケースがそうです)。そういうことを知らないと、「大学の研究は、今の世の中の流行りと違うので、役に立たない」という、非常に近視眼的な考えにとらわれてしまうことになります。別に米澤研究室を目指していない、あるいは研究者になるつもりがない人でも、コンピュータの業界で働く人は、そういう「その場の勢い」に流されない論理的思考力をぜひとも備えてほしいところです。

〔トップページへ〕 〔「研究室紹介」のindexページへ〕


<vu@is.s.u-tokyo.ac.jp>
Last updated on 8 Feb., 2002