システムソフトウェアのための安全性と記述性に優れた領域特化言語とその構成法

Research Project

Project/Area Number	23K11055
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Multi-year Fund
Section	一般
Review Section	Basic Section 60050:Software-related
Research Institution	Meiji University
Principal Investigator	岩崎英哉明治大学, 理工学部, 専任教授 (90203372)
Co-Investigator(Kenkyū-buntansha)	中山泰一電気通信大学, 大学院情報理工学研究科, 教授 (70251709)
Project Period (FY)	2023-04-01 – 2026-03-31
Project Status	Granted (Fiscal Year 2023)
Budget Amount *help	¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000) Fiscal Year 2025: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000) Fiscal Year 2024: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000) Fiscal Year 2023: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Keywords	領域特化言語 / システムソフトウェア / セマンティックギャップ / 静的検査 / 関数型言語
Outline of Research at the Start	本研究は，計算機システムの根幹をなすシステムソフトウェアのうち，扱う対象データを構造に基づいて扱うのではなく，単なるバイト列としても扱う必要があるものに注目する．このようなシステムソフトウェアにおける安全性の問題と記述性の問題を解決するために，本研究は，目的に応じた領域特化言語の利用に注目する．各システムソフトウェアに合わせた領域特化言語を設計・実現し，その領域特化言語を用いてプログラムを記述する．目的の処理を行うプログラムを書きやすいような記述性を領域特化言語が支援し，誤りを静的に検出するなどの安全性をその領域特化言語の処理系が支援することを目指す．
Outline of Annual Research Achievements	本研究は，セマンティックギャップを意識する必要があるシステムソフトウェアを記述するための安全性と記述性に優れた領域特化言語 (DSL) の設計と実現の方法論を確立することを目的とする．2023年度は，関数型言語Haskellを親言語とし，Haskellの型検査機構により安全性を実現する埋め込みDSL (EDSL) の実現に焦点を絞って研究を進め，以下の成果を得た． (1) セマンティックギャップを埋め，外部からシステムソフトウェア内部への安全なメモリアクセスを実現するEDSLを設計し，実現した． (2) 本EDSLのひとつの適用例として，仮想マシン上で動作するゲストOSの内部状態をOS外部から観察・検査する Virtual Machine Introspection (VMI) の機能を，本EDSLにより実現するライブラリ HaVMI を設計・実装した． (3) 本EDSLのもうひとつ別の適用例として，GDB 等のデバッガにおいて，デバッグ対象プログラムの内部状態に安全にアクセスする HaDbg を，EDSL を用いて設計・実装した．このEDSLで実装した部分は，デバッガのフロントエンドとして動作する．これらふたつのシステムは二層構造になっており，VMI，デバッグ等の目的によらない共通の処理を，下層部にあるEDSLの核部分が担っている．一方上層部は，下層部が提供する機能を利用して，それぞれのシステムの対象に応じた処理を実装する．このような二層構造は，本EDSLの柔軟性・一般性，さらには有効性に大きく寄与している．なお (1)と(2)の部分については，プログラミング言語，特に関数型言語の研究領域で定評のある国際会議 Haskell Symposium において論文が採択され，口頭発表を行った．
Current Status of Research Progress	Current Status of Research Progress 2: Research has progressed on the whole more than it was originally planned. Reason 「研究実績の概要」にも記した通り，今年度は以下のような成果が得られている．第一に，Haskell を親言語とする EDSLを設計し，ふたつの異なるシステムソフトウェア (Virtual Machine Introspection とデバッガ)に適用した．その結果，提案する EDSLの有効性が示すことができた．第二に，親言語の基本的な機能である型検査機構を利用することにより，本研究の1つめの課題である安全性を達成した．また，宣言的なプログラム記述を行う関数型言語を採用し，副作用を伴うアクションについてはモナドを利用することにより，本研究の2つめの課題である記述性の問題を，十分とはいえないもののある程度達成した．以上を総合的に判断して，「おおむね順調に進展」と評価した．
Strategy for Future Research Activity	2023年度の研究を受けて，2024年度は，親言語と領域特化言語との間の協調機構，親言語の機能制限に焦点をあてた上で，以下の課題に中心に取り組む予定である． (1) 親言語の多様な機能のうち，EDSLが必要とするものだけを利用可能とするために，親言語側でその構文や機能を選別して再利用可能な形でEDSL側に提供する機構を検討する．具体的には，親言語中にEDSLと協調するためのアノテーション等を記述することを考えている． (2) 2023年度に実現したHaskellを親言語とするシステムソフトウェア向けのEDSLに対して，上で検討した機構を試験的に実装する．さらに，Virtual Machine Introspection とデバッガ以外の応用例も記述し，提案する機構がどの程度一般的になり得るかを検証する． (3) 記述性をさらに向上させるために，親言語の提供するメタプログラミング機構を利用することを検討し，その有効性を検証する．それぞれの課題に関しては，ある程度内容がまとまった段階で対外発表を行っていく．