| 研究課題/領域番号 |
23K11055
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 明治大学 |
|---|
研究代表者 |
岩崎 英哉 明治大学, 理工学部, 専任教授 (90203372)
|
|---|
| 研究分担者 |
中山 泰一 電気通信大学, 大学院情報理工学研究科, 教授 (70251709)
|
|---|
| 研究期間 (年度) |
2023-04-01 – 2026-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
4,810千円 (直接経費: 3,700千円、間接経費: 1,110千円)
2025年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2024年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2023年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
|
|---|
| キーワード | 領域特化言語 / システムソフトウェア / セマンティックギャップ / 静的検査 / 関数型言語 |
|---|
| 研究開始時の研究の概要 |
本研究は，計算機システムの根幹をなすシステムソフトウェアのうち，扱う対象データを構造に基づいて扱うのではなく，単なるバイト列としても扱う必要があるものに注目する．このようなシステムソフトウェアにおける安全性の問題と記述性の問題を解決するために，本研究は，目的に応じた領域特化言語の利用に注目する．各システムソフトウェアに合わせた領域特化言語を設計・実現し，その領域特化言語を用いてプログラムを記述する．目的の処理を行うプログラムを書きやすいような記述性を領域特化言語が支援し，誤りを静的に検出するなどの安全性をその領域特化言語の処理系が支援することを目指す．
|
| 研究実績の概要 |
本研究は，セマンティックギャップを意識する必要があるシステムソフトウェアを記述するための安全性と記述性に優れた領域特化言語 (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 において論文が採択され，口頭発表を行った．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
「研究実績の概要」にも記した通り，今年度は以下のような成果が得られている．
第一に，Haskell を親言語とする EDSLを設計し，ふたつの異なるシステムソフトウェア (Virtual Machine Introspection とデバッガ)に適用した．その結果，提案する EDSLの有効性が示すことができた．
第二に，親言語の基本的な機能である型検査機構を利用することにより，本研究の1つめの課題である安全性を達成した．また，宣言的なプログラム記述を行う関数型言語を採用し，副作用を伴うアクションについてはモナドを利用することにより，本研究の2つめの課題である記述性の問題を，十分とはいえないもののある程度達成した．
以上を総合的に判断して，「おおむね順調に進展」と評価した．
|
| 今後の研究の推進方策 |
2023年度の研究を受けて，2024年度は，親言語と領域特化言語との間の協調機構，親言語の機能制限に焦点をあてた上で，以下の課題に中心に取り組む予定である．
(1) 親言語の多様な機能のうち，EDSLが必要とするものだけを利用可能とするために，親言語側でその構文や機能を選別して再利用可能な形でEDSL側に提供する機構を検討する．具体的には，親言語中にEDSLと協調するためのアノテーション等を記述することを考えている．
(2) 2023年度に実現したHaskellを親言語とするシステムソフトウェア向けのEDSLに対して，上で検討した機構を試験的に実装する．さらに，Virtual Machine Introspection とデバッガ以外の応用例も記述し，提案する機構がどの程度一般的になり得るかを検証する．
(3) 記述性をさらに向上させるために，親言語の提供するメタプログラミング機構を利用することを検討し，その有効性を検証する．
それぞれの課題に関しては，ある程度内容がまとまった段階で対外発表を行っていく．
|
