@article{oai:ipsj.ixsq.nii.ac.jp:00232425,
 author = {Sai, Veerya Mahadevan and Yuuki, Takano and Atsuko, Miyaji and Sai, Veerya Mahadevan and Yuuki, Takano and Atsuko, Miyaji},
 issue = {2},
 journal = {情報処理学会論文誌},
 month = {Feb},
 note = {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
------------------------------, 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
------------------------------},
 title = {PRSafe: A Domain Specific Language Created with LLVM},
 volume = {65},
 year = {2024}
}