Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows
2023年度研究会推薦博士論文速報
［プログラミング研究会］
松下 祐介
（京都大学大学院 情報学研究科 五十嵐・末永研究室 特定研究員（学振PD））
邦訳：不変条件とRust流の借用を扱える非Step-Indexedな分離論理
■キーワード
ソフトウェア科学／Rust／プログラム検証
【背景】Rustプログラムなどの検証のための一般的基礎がほしい
【問題】特に停止性などの高度な性質の論証が難しい
【貢献】不変条件や借用について検証するための一般的基礎を確立した
情報技術が大事な役割を果たす現代において，高品質のソフトウェアを開発するための一般的な方法論を探究する「ソフトウェア科学・工学」が注目されています．特に重要で面白いテーマのひとつが，「プログラム検証」，すなわちソフトウェアを記述するプログラムを解析して，コンピュータで正しく動作することを数学的に厳密に証明することです．
プログラム検証で立ちはだかる大きい壁のひとつが，グローバルに読み書きできる記憶装置，「メモリ」です．メモリを駆使することで高性能の計算を実現できる一方で，予期せぬ挙動が生じることがあり，深刻なセキュリティ脆弱性の要因となっています．こうした困難を解決するための中心的な道具が，可変なデータにアクセスするための独占的な権利，「所有権」です．メモリ全体の所有権を分割して管理することで，プログラムの動作について効率良く正確に論じることができます．特に，2015年に生まれた「Rust」は，それぞれのデータに所有権をタグ付けすることで，プログラムにメモリ関連のエラーがないことを自動的に検査してくれるプログラミング言語で，現実のソフトウェア開発で人気を集めています．ちなみにサムネイルの画像は，所有権を分けている様子を，Rustのマスコットの蟹のFerrisを使って描いたものです．
所有権にもとづくプログラム検証の基礎として活発に研究されているのが，「分離論理」です．この論理では，命題が可変なデータへの所有権を持ち共有が制限されることで，効率良く正しい推論を実現しています．現代的な分離論理では，分離論理の命題を使って記述された約束のもとで可変なデータを共有するための，「不変条件」や「借用」といった仕組みが導入され，広く使われています．特に借用は，Rustの基礎となっている，理論的にも実用上もとても大事な仕組みです．しかし，こうした仕組みは，素朴に扱うと論理が矛盾することが知られています．既存研究では共有対象を「later様相」というもので一律に弱めて矛盾を回避しましたが，このせいで「step-indexing」という道具が必要になってしまい，計算の停止性のような高度な性質を上手く検証することができませんでした．
私の博士論文の研究は，分離論理において不変条件や借用といった仕組みを，later様相を原則として使わずに実現できる，新しい手法「Nola」を提案しました．鍵となるアイデアは，共有のための仕組みを分離論理の命題を表すデータ型とその解釈について一般化することです．このデータ型・解釈を適切に選ぶことで，多くの場合に矛盾を回避しつつlater様相を使わずに済んで，さまざまな興味深い例について検証が上手くいく，ということを明らかにしました．特に，未来を先取りする「預言」という技術でRustプログラムを効率良く検証できる「RustHorn」の手法について，later様相を前提としない一般的な基礎を築きました．さらにNolaを「Coq」という証明を書くための言語の上のフレームワークとして実装して，手法の正しさを厳密に証明し，将来の研究のために使えるようにしました．図でNolaの概要を簡単にまとめました．さらに詳しい話については，ぜひ発表スライドや論文をご覧ください．
■Webサイト／動画／アプリなどのURL
発表スライド https://shiatsumat.github.io/talks/phd-thesis-talk.pdf
博士論文 https://shiatsumat.github.io/papers/phd-thesis.pdf
（2024年5月31日受付）
（2024年8月15日note公開）
ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー
取得年月：2024年3月
学位種別：博士（情報理工学）
大学：東京大学
正会員
ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー ー
推薦文［コンピュータサイエンス領域］プログラミング研究会
ソフトウェアの動作の正しさを保証する上で，スレッド間などで共有された可変な状態について賢く論じることが，理論・応用の両方で大きな課題となっています．この博士論文は，この問題に対して，Rustの所有権型などの近年の発展的なアプローチを包括する形で，将来性に富んだ一般的な解決法を提案しています．
研究生活 高校生のころにHaskellに出会いソフトウェア科学に興味を持ちました．大学1年のころにRustと出会い，理論から生まれたアイデアが現実の問題を解決していることに感動しました．大学4年でソフトウェア科学の研究室に入り，卒業研究で早速Rustプログラム検証に取り組みました．風呂場でふとRustHornの手法のアイデアを思いついて，我ながらこれは凄いと興奮したのを覚えています．この研究で自信を持ち，家族の応援もあり，博士課程に進学しました．
博士課程の3年間は，国内外の研究者と交流できて，私の研究アイデアを世界の研究者とともに発展させられて，とても充実していました．一方で，どうすれば将来につながる良い研究ができるのか，模索も続きました．Googleでのインターンなども経験しましたが，やはり基礎をしっかり研究したいな，という気持ちを新たにしました．そうして紆余曲折あって出来上がった博士論文は，やり残したと思う部分もあるものの，ひとつの確固たる基礎を提示できたはずだ，と感じています．