~ 大学院生からのメッセージ~
ソフトウェアの世界を切り拓く
 |
| 松下 祐介 |
| 情報理工学系研究科 博士課程2年生 |
| 出身地 大阪府 |
| 出身高校 私立灘高等学校 |
| 出身学部 東京大学理学部情報科学科 |
私たちの暮らしは，たくさんの「ソフトウェア」によって支えられている。まずパソコンやスマホの色々なアプリケーションが思い浮かぶだろうか。その裏側でマウスやタッチパネル，グラフィクス，ネットワークを動かすのもソフトウェアだ。さらには，身の回りの家電，銀行のATM，街を走る自動車，交通を守る信号機，病院のMRI，航空機や人工衛星，それらを制御しているのもソフトウェアだ。
ソフトウェアの開発は人間と機械の共同作業だ。プログラマ達は，欲しいソフトウェアを実現するための具体的な計算方法を，プログラミング言語，すなわち人間と機械の共通語で，プログラムとして表現する。もちろん，意図せぬ挙動，いわゆる「バグ」がないように，注意して工夫して開発する。それでも人間の仕事であるから，しばしばバグが生まれ見逃されてしまう。これを防ぐ手法の一つが，プログラムが意図した仕様を満たすことを論理的に証明する，「検証」だ。
一般にアプリケーションはいくつかの抽象化の階層を重ねて得られるが，そのなかでもハードウェアに近い低層のソフトウェアを，「システムソフトウェア」という。特に，メモリを直接操作することで，高性能の計算を実現できる。一方でこうしたソフトウェアは，エラー検出などによる保護が薄いため，深刻なバグが埋め込まれる危険性が高い。
私は，ソフトウェア科学，特にシステムソフトウェアの検証を研究している。
2015 年，「Rust」という言語が誕生し，システムソフトウェアを堅牢に開発できる言語として，急速に産業で使われ出している。Rust は強い静的な「型システム」により，プログラムのメモリ安全性を自動で検査してくれる。その鍵となるのが，メモリの特定 領域へのアクセス権限，「所有権」。所有権にもとづく型は長らく研究されてきたが，Rust は所有権を一時的に渡す「借用」という仕組みを導入し，実用的なレベルへと高めた。
型の保証を上手く使って，Rust プログラムを効率よく検証できないだろうか？ Rust では事前に期限を決めて所有権を借用できる。所有権があれば自由にメモリ上の値を更新できる。また，借用した所有権は分割でき，自由に捨てられる。そのあと，貸し手が所有権を回復したとき，更新後のメモリ上の値がわかるように，計算をモデル化すること。これが問題だった。
私の主著論文「RustHorn」は，未来のメモリ上の値を先取りする「預言」というアイデアでこれを解決した。概略を図にまとめた。
RustHorn による検証の例
RustHorn では，この手法がさまざまなRust プログラムを厳密にモデル化できることを証明し，自動検証への有用性も実験的に示した。この研究の影響として，これにもとづく本格的なRust の半自動検証器をフランスの学生が作っている。私の別の主著論文「RustHornBelt」では，広いクラスのRust プログラムに対するRustHorn の手法の正当性を，Coqという証明支援システムで証明した。私は今，借用と預言をもちいた，新しいシステムソフトウェア開発の形を探っている。
実際のソフトウェア開発は，とても人間的な営みで，時に泥臭い。だからこそ，理学の尖ったアイデアが現場を切り拓く光となる。そう信じて，私は今日も研究する。