| 研究課題/領域番号 |
21J20459
|
|---|
| 配分区分 | 補助金 |
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
松下 祐介 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| 研究期間 (年度) |
2021-04-28 – 2024-03-31
|
| キーワード | プログラム検証 / システムプログラミング / Rust |
|---|
| 研究実績の概要 |
国際会議 ESOP 2020 に採択された主著論文 RustHorn (松下, 塚田 & 小林) の拡大改訂版がトップ国際ジャーナル ACM TOPLAS の ESOP 2020 特別号に採択され、出版された。
この研究は、システムプログラミング言語 Rust のプログラムの機能正当性を自動検証するための新しい手法を提案し、その正当性を証明し、また、この手法の有用性を実験的に確かめた。この手法の特色は、未来の情報を先取りする「預言」というアイデアにより、可変借用という仕組みを通したメモリの破壊的な更新がある状況でも、メモリやアドレスを具体的に扱わずに、簡潔にプログラムの振る舞いをモデル化できることである。
このジャーナル版は、会議版と比べて、全体的に説明が丁寧になっており、形式化が改善され、手法の健全性・完全性についての証明が含まれており、かつ、実験が拡充されている。
研究プロジェクト RustHornBelt を MPI-SWS の RustBelt チームとともに進め、その研究成果をまとめた主著論文 RustHornBelt (松下, Denis, Jourdan & Dreyer) がトップ国際会議 ACM PLDI 2022 に採択された。
この研究では、様々な API を含む Rust の広いサブセットに対して、RustHorn 方式のモデルの正しさ (健全性) を検証することができる、初めての形式的な基盤を与えた。特に、RustHorn 方式の預言を正当化するために、新しい論理的機構「パラメトリック預言」を開発した。この基盤は定理証明支援系 Coq 上で機械化されており、特に、様々な API に対する RustHorn 方式のモデルの正しさを機械的に証明した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
RustHorn の預言を用いたモデル化によるシステムプログラムの検証手法を更に発展させていくことが研究の一つの軸であるが、それにあたって、預言を用いたモデル化の正しさを柔軟に証明できるような手法がないことが大きなネックとなっていた。
研究プロジェクト RustHornBelt で開発した「パラメトリック預言」という新しい論理的機構は、これを柔軟に解決するものであり、これからシステムプログラムを検証するための仕組みを更に色々と設計していくうえで、重要な基礎となると期待される。
この研究を通して、定理証明支援系 Coq で本格的に何千行もの証明を書く経験をしたが、ここで得た知見と技術はこれから堅牢な検証プラットフォームを作っていく上で活きていくと期待される。また、具体的に様々な Rust API について証明を書く経験を得たことで、プログラム検証における落とし穴や苦労についての実地的な肌感覚を得られたことも大きい。
RustHornBelt の研究プロジェクトを通して、COVID-19 パンデミックの影響でオンラインでのやり取りとはなったものの、国際的な共同研究を経験し、さらにトップ国際会議 PLDI に採択されたことは、研究者としての力となった。
まだ正式に発表した結果はないものの、Rust のような型システムに対する型検査 (借用検査) のアルゴリズムの研究や、強力な検証機構を組み込んだシステムプログラミング言語の設計も着々と進めている。これから芽が出ることが期待される。
|
| 今後の研究の推進方策 |
6月に開催される国際会議 PLDI 2022 に参加し、主著論文 RustHornBelt の発表を行う。ここで世界の研究者たちや企業の人たちと交流し、今後の研究に繋げていきたい。
また、高階幽霊状態 (higher-order ghost state) を扱えて、かつ停止性・活性のような無限の実行の絡む性質も柔軟に検証できる、強力な分離論理の設計を進めていく。既存研究 Iris のような純粋に意味論的なアプローチではなく、構文論と意味論をほどよく織り交ぜることで、このような柔軟性を実現する。特に、この論理を、依存型付きプログラミング言語 Agda の上で機械的に形式化していく。機械的形式化により、紙の上での人力のチェックに留まらず、機械によって検査された堅牢な証明が書けるようになる。また、これは他の研究者にとっても、この論理体系を理解することを助けるものであり、知見を活かしやすくするものである。Agda は Coq と似た論理体系にもとづいた言語で、定理証明支援系として使えるが、Agda はプログラミング言語としての機能が特に充実しており、今回考える構文論を交えたアプローチと相性がいいと考えている。
この論理を基盤としながら、更に、システムプログラミングのための様々な型システム・検証フレームワークを設計していく予定である。特に、Rust のような型システムに対する型検査 (借用検査) のアルゴリズムの研究や、強力な検証機構を組み込んだシステムプログラミング言語の設計を進めていく。現実の Rust や C++ におけるシステムプログラミングの実践から積極的に学びながら、堅牢なシステムソフトウェア開発のための色々なアイデアを探究していく。
|
