WEKO3
アイテム
PRSafe: A Domain Specific Language Created with LLVM
https://ipsj.ixsq.nii.ac.jp/records/232425
https://ipsj.ixsq.nii.ac.jp/records/23242517f44553-a621-4927-a081-4503532da3d2
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-JNL6502039.pdf (2.0 MB)
2026年2月15日からダウンロード可能です。
|
Copyright (c) 2024 by the Information Processing Society of Japan
|
|
| 非会員：¥0, IPSJ:学会員：¥0, 論文誌:会員：¥0, DLIB:会員：¥0 | ||
| Item type | Journal(1) | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2024-02-15 | |||||||||||
| タイトル | ||||||||||||
| タイトル | PRSafe: A Domain Specific Language Created with LLVM | |||||||||||
| タイトル | ||||||||||||
| 言語 | en | |||||||||||
| タイトル | PRSafe: A Domain Specific Language Created with LLVM | |||||||||||
| 言語 | ||||||||||||
| 言語 | eng | |||||||||||
| キーワード | ||||||||||||
| 主題Scheme | Other | |||||||||||
| 主題 | [特集:ネットワークサービスと分散処理] eBPF, Domain Specific Language (DSL), LLVM, network, user-space | |||||||||||
| 資源タイプ | ||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||||||
| 資源タイプ | journal article | |||||||||||
| 著者所属 | ||||||||||||
| Osaka University | ||||||||||||
| 著者所属 | ||||||||||||
| TIER IV, Inc. | ||||||||||||
| 著者所属 | ||||||||||||
| Osaka University | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Osaka University | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| TIER IV, Inc. | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Osaka University | ||||||||||||
| 著者名 |
Sai, Veerya Mahadevan
× Sai, Veerya Mahadevan
× Yuuki, Takano
× Atsuko, Miyaji
|
|||||||||||
| 著者名(英) |
Sai, Veerya Mahadevan
× Sai, Veerya Mahadevan
× Yuuki, Takano
× Atsuko, Miyaji
|
|||||||||||
| 論文抄録 | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | The eBPF (Berkeley Packet Filter) in the Linux OS is a virtual machine for injecting user-space programs written in C language inside the Linux kernel, to perform a range of network processing functions, by attaching them to kernel level hooks such as system calls. Despite being a revolutionary replacement to in-kernel programming and being increasingly adopted by kernel-focused applications, developers struggle to understand and use eBPF directly. This is due to the conditions that for C programs to be able to run inside the Linux kernel, they need to be Non-Turing complete and successfully pass the safety checks of the eBPF verifier module inside eBPF. As C is a Turing-complete language, this puts the onus on developers to design a C program with restricted, Non-Turing complete functionality. In order to reduce the burden on developers, a Domain Specific Language called PRSafe was created. In this paper, we aim to provide an introduction to PRSafe and provide a qualitative evaluation between programs written for eBPF with conventional development toolchains vs PRSafe. We go further to use PRSafe in conjunction with K2, a synthesis compiler used for optimization and verification of eBPF code. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.32(2024) (online) DOI http://dx.doi.org/10.2197/ipsjjip.32.207 ------------------------------ |
|||||||||||
| 論文抄録(英) | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | The eBPF (Berkeley Packet Filter) in the Linux OS is a virtual machine for injecting user-space programs written in C language inside the Linux kernel, to perform a range of network processing functions, by attaching them to kernel level hooks such as system calls. Despite being a revolutionary replacement to in-kernel programming and being increasingly adopted by kernel-focused applications, developers struggle to understand and use eBPF directly. This is due to the conditions that for C programs to be able to run inside the Linux kernel, they need to be Non-Turing complete and successfully pass the safety checks of the eBPF verifier module inside eBPF. As C is a Turing-complete language, this puts the onus on developers to design a C program with restricted, Non-Turing complete functionality. In order to reduce the burden on developers, a Domain Specific Language called PRSafe was created. In this paper, we aim to provide an introduction to PRSafe and provide a qualitative evaluation between programs written for eBPF with conventional development toolchains vs PRSafe. We go further to use PRSafe in conjunction with K2, a synthesis compiler used for optimization and verification of eBPF code. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.32(2024) (online) DOI http://dx.doi.org/10.2197/ipsjjip.32.207 ------------------------------ |
|||||||||||
| 書誌レコードID | ||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||
| 収録物識別子 | AN00116647 | |||||||||||
| 書誌情報 |
情報処理学会論文誌 巻 65, 号 2, 発行日 2024-02-15 |
|||||||||||
| ISSN | ||||||||||||
| 収録物識別子タイプ | ISSN | |||||||||||
| 収録物識別子 | 1882-7764 | |||||||||||
| 公開者 | ||||||||||||
| 言語 | ja | |||||||||||
| 出版者 | 情報処理学会 | |||||||||||
