abstract.tex

\begin{abstract}
% eBPF has become the de-facto kernel extension mechanism in the Linux kernel
%   and have been leveraged extensively in domains of networking, system
%   debugging and event tracing, as well as, security.
% The core value proposition of eBPF is the unprecedented promise of safety
%   through its static verification scheme: the kernel performs symbolic
%   execution on the compiled eBPF bytecode to examine various safety properties.
% Despite its safety guarantees, the price of kernel verification of eBPF
%   programs is high.
% The restricted expressiveness of eBPF on loops or complex logic often leads to
%   splitting the program into small pieces, or limitation in functionality when
%   logic cannot be expressed.
% On the other hand, static verification is fundamentally limited in verifying
%   certain safety properties -- a verified eBPF program can still overflow
%   the kernel stack or hold the CPU for a long time.

Kernel extension is an essential component of modern operating systems and has
  been increasingly leveraged in the domains of file systems, networking,
  and security.
%  of file systems, consensus protocols, key-value storage, and security, often
%  in the form of large and complex programs.
The de-facto kernel extension mechanism in the Linux kernel is eBPF.
However, eBPF is constrained by its static verifier, which provides
  safety as its core value proposition but at the same time creates usability
  challenges.
%, especially with the increasingly complex use cases.
%  makes it hard to
%  support the increasingly complex use cases due to limited expressiveness.
% The restriction of eBPF on loops or complex logic often leads to splitting the
%   program into small pieces, or limitation in functionality when logic cannot
%   be expressed.
% Developers are often forced to heavily massage their code -- splitting the
%   program into small pieces and implementing cumbersome conditions, in order
%   to pass the verifier.
% On the other hand, static verification is fundamentally limited in verifying
%   certain safety properties -- a verified eBPF program can still overflow
%   the kernel stack or hold the CPU for a long time.
% At the core of the problem is a large gap between the programmer and the
%   verifier.
In this paper, we identify the root of the problem to be a large gap between
  the programming language and the verifier.

We make the observation that the enhanced usability and the
  needed safety properties can be obtained from a safe language,
%   effectively eliminating the verifier and closing the gap.
  effectively closing the \gap{} by eliminating the extra layer of verification.
We design and implement a new Rust-based kernel extension abstraction:
  \projname{}, where safe Rust programs run in
  the place of verified eBPF programs.
% The use of Rust achieves both Turing-Completeness and runtime-safety.
Our Rust layer provides a \textit{safe} program interface for kernel extension
  programs and runtime safety mechanisms that ensures type/memory safety,
  resource management, and exception handling.
\mvle{what about bounded execution?}
% We implement several state of the art eBPF programs with comparable
%   performance to JITed eBPF programs, demonstrating there is no need to split
%   programs or limit their processing data size.
We evaluate \projname{} both on its usability and performance, demonstrating
  %that \projname{} is able to address most of the usability issues from current
  that \projname{} is able to eliminate most of the usability challenges from current
  Linux eBPF without sacrificing performance.
% \jinghao{Shall we mention BMC specifically here?}

\end{abstract}