| 研究課題/領域番号 |
22KJ0561
|
|---|
| 補助金の研究課題番号 |
21J20459 (2021-2022)
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 基金 (2023)
補助金 (2021-2022) |
|---|
| 応募区分 | 国内 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
松下 祐介 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| 研究期間 (年度) |
2023-03-08 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
2,200千円 (直接経費: 2,200千円)
2023年度: 700千円 (直接経費: 700千円)
2022年度: 700千円 (直接経費: 700千円)
2021年度: 800千円 (直接経費: 800千円)
|
|---|
| キーワード | プログラム検証 / 分離論理 / Iris / Coq / Rust / システムプログラミング |
|---|
| 研究開始時の研究の概要 |
システムソフトウェアとは、ハードウェアに近い階層で、高位のアプリケーションの基盤となる計算処理を提供するソフトウェアのことである。システムソフトウェアは、共有メモリ・スレッドに対する低レベルの操作を直接使い、高性能の計算を実現できる一方で、複雑な状態変化を伴うため動作の理解・論証が難しく、しばしば深刻なバグが忍び込んでしまう。
数多くのソフトウェアが社会を支えている現代において、システムソフトウェアのバグを未然に防ぐことはますます重要となっている。本研究では、Rust などの近年の動向から学びながら、システムプログラムを検証するための型システム・論理を理論・応用の両側面から探究する。
|
| 研究実績の概要 |
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月に出版された。
|
