| Project/Area Number |
22KJ0561
|
|---|
| Project/Area Number (Other) |
21J20459 (2021-2022)
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Multi-year Fund (2023)
Single-year Grants (2021-2022) |
|---|
| Section | 国内 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
松下 祐介 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2023-03-08 – 2024-03-31
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 2023: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2022: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2021: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | プログラム検証 / 分離論理 / Iris / Coq / Rust / システムプログラミング |
|---|
| Outline of Research at the Start |
システムソフトウェアとは、ハードウェアに近い階層で、高位のアプリケーションの基盤となる計算処理を提供するソフトウェアのことである。システムソフトウェアは、共有メモリ・スレッドに対する低レベルの操作を直接使い、高性能の計算を実現できる一方で、複雑な状態変化を伴うため動作の理解・論証が難しく、しばしば深刻なバグが忍び込んでしまう。
数多くのソフトウェアが社会を支えている現代において、システムソフトウェアのバグを未然に防ぐことはますます重要となっている。本研究では、Rust などの近年の動向から学びながら、システムプログラムを検証するための型システム・論理を理論・応用の両側面から探究する。
|
| Outline of Annual Research Achievements |
3年間の研究期間にわたって、Rust の所有権型システム、および RustHorn の預言にもとづく検証手法を核として、特に、システムプログラムの検証について分離論理による基礎づけを与える、RustHornBelt や Nola といった研究プロジェクトを進めた。
2023年度は、主に Nola に取り組んだ。これは、分離論理（ヒープメモリなどについてスケーラブルに検証するための論理）において共有された可変な状態について論じるための「不変条件」や「借用」といった仕組みを、「共有対象を記述する命題の表現と解釈についてパラメトライズする」ことで柔軟に実現する、新しいアプローチを提案するものである。特に、Iris 分離論理フレームワークのライブラリとして定理証明支援系 Coq で機械化し、一般の検証プロジェクトで使えるようにした。これらの成果をまとめた博士論文 "Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows" を執筆・12月に提出し、審査に合格し、3月に博士号を得た。
9月には、スイス ETH Zurich の Peter Muller 教授・Ralf Jung 助教のグループを現地訪問し、自らの研究プロジェクト・今後の研究について1時間ほどのトークをし、さらに1週間ほどにわたり、グループのメンバーと研究について幅広く議論した。
また、研究室の後輩である中山崇氏の研究プロジェクトについても、素朴な手法の問題点の指摘・提案手法の正しさの証明・論文執筆などで貢献し、その成果をまとめた論文 "Borrowable Fractional Ownership Types for Verification" が国際会議 VMCAI 2024 に採択され、1月に出版された。
|
