Abstract

General Purpose programming languages such as C++, Python suffer from resource management and input errors because they are Turing-complete. However, domain specific, Non-Turing complete languages are designed to always terminate and are statically verified for program safety. Hence, Domain Specific Languages(DSLs) have been created for resource-critical domains that prioritize safe execution and termination of programs.

One such critical domain, is the Linux Operating System's in-kernel module called eBPF - Extended Berkeley Packet Filter, a part of the Linux kernel to perform functions such as packet processing. The eBPF has an in-built verification module called the eBPF verifier. This eBPF verifier is a strict module that ensures that only safe programs; i.e. programs that definitely terminate and do not have unrestricted access to memory can be run inside the Linux kernel. Due to the safety properties needed to be ensured by the verifier, C programs written for the kernel need to massaged in order to be acceptable by the verifier. This puts an onus on the developer to modify the source code written in C to essentially make it behave as a Non-Turing complete language.

To overcome the fundamental developer-side issues while developing programs for the eBPF, such as usability, difficulties during debugging and lack of formal-foundation based verifier methods that ensure safety, alternate tools for development such as the P4 language (Non-Turing complete language) and alternate verifiers such as PREVAIL - a static analysis based user-space verifier, can be used. However, although the P4 alternative is comparable to using restricted C language for development, it is not the best option in terms of eBPF-domain specific usage. Also, PREVAIL is not the best verifier option in terms of safety properties.

In order to provide a user-friendly alternate solution towards the issues of the eBPF verifier, in this work, a proposal for the design of a DSL called PRSafe has been made. PRSafe is a syntactically and semantically restricted, Non-Turing complete language based on the memory and input properties of Primitive Recursive Functions (PRFs). PRSafe is modular and extensible. It is eventually intended to be a mathematically verifiable compiler with better user-friendly error-diagnostics than the conventional eBPF verifier. Currently, PRSafe has been implemented using Lex and Bison softwares for lexing and parsing respectively. For semantic analysis, Abstract Syntax Tree (AST) formulation and Code Generation, we use the LLVM compiler infrastructure.

Top