~ 大学院生からのメッセージ~

ソフトウェアの
世界を切り拓く

 

松下 祐介

 Yusuke Matsushita
(情報理工学系研究科 博士課程2年生)

私たちの暮らしは,たくさんの「ソフトウェア」によって支えられている。まずパソコンやスマホの色々なアプリケーションが思い浮かぶだろうか。その裏側でマウスやタッチパネル,グラフィクス,ネットワークを動かすのもソフトウェアだ。さらには,身の回りの家電,銀行のATM,街を走る自動車,交通を守る信号機,病院のMRI,航空機や人工衛星,それらを制御しているのもソフトウェアだ。

ソフトウェアの開発は人間と機械の共同作業だ。プログラマ達は,欲しいソフトウェアを実現するための具体的な計算方法を,プログラミング言語,すなわち人間と機械の共通語で,プログラムとして表現する。もちろん,意図せぬ挙動,いわゆる「バグ」がないように,注意して工夫して開発する。それでも人間の仕事であるから,しばしばバグが生まれ見逃されてしまう。これを防ぐ手法の一つが,プログラムが意図した仕様を満たすことを論理的に証明する,「検証」だ。

一般にアプリケーションはいくつかの抽象化の階層を重ねて得られるが,そのなかでもハードウェアに近い低層のソフトウェアを,「システムソフトウェア」という。特に,メモリを直接操作することで,高性能の計算を実現できる。一方でこうしたソフトウェアは,エラー検出などによる保護が薄いため,深刻なバグが埋め込まれる危険性が高い。

私は,ソフトウェア科学,特にシステムソフトウェアの検証を研究している。

2015 年,「Rust」という言語が誕生し,システムソフトウェアを堅牢に開発できる言語として,急速に産業で使われ出している。Rust は強い静的な「型システム」により,プログラムのメモリ安全性を自動で検査してくれる。その鍵となるのが,メモリの特定 領域へのアクセス権限,「所有権」。所有権にもとづく型は長らく研究されてきたが,Rust は所有権を一時的に渡す「借用」という仕組みを導入し,実用的なレベルへと高めた。

型の保証を上手く使って,Rust プログラムを効率よく検証できないだろうか? Rust では事前に期限を決めて所有権を借用できる。所有権があれば自由にメモリ上の値を更新できる。また,借用した所有権は分割でき,自由に捨てられる。そのあと,貸し手が所有権を回復したとき,更新後のメモリ上の値がわかるように,計算をモデル化すること。これが問題だった。

私の主著論文「RustHorn」は,未来のメモリ上の値を先取りする「預言」というアイデアでこれを解決した。概略を図にまとめた。

RustHorn による検証の例

RustHorn では,この手法がさまざまなRust プログラムを厳密にモデル化できることを証明し,自動検証への有用性も実験的に示した。この研究の影響として,これにもとづく本格的なRust の半自動検証器をフランスの学生が作っている。私の別の主著論文「RustHornBelt」では,広いクラスのRust プログラムに対するRustHorn の手法の正当性を,Coqという証明支援システムで証明した。私は今,借用と預言をもちいた,新しいシステムソフトウェア開発の形を探っている。

実際のソフトウェア開発は,とても人間的な営みで,時に泥臭い。だからこそ,理学の尖ったアイデアが現場を切り拓く光となる。そう信じて,私は今日も研究する。

    Profile
出身地 大阪府
出身高校 私立灘高等学校
出身学部 東京大学理学部情報科学科


 

理学部ニュース2022年5月号掲載



理学のススメ>

  • このエントリーをはてなブックマークに追加