discussion.tex

\section{Discussion}
\label{sec:discussion}
% \begin{itemize}
%     \item Unsafe code in rt crate
%     \item Verified Rust extension using Verus
%     \item Dynamic allocation (if we end up not doing it)
%     \item Cross-Language Attacks from NDSS 2022
%     \item Rust memory ordering in kernel (\url{https://lwn.net/SubscriberLink/967049/66bfb6f365d164aa/})
%     \item Compatibility \projname{} across kernel versions.
%     \item Memory usage for usecases with loads of programs defined in the same
%         file (e.g. KCFI)
% \end{itemize}

\para{Incorporating Verification} In this paper, we have argued to
close the language/verifier gap by leveraging inherent safety
properties of the Rust language.  However, this approach defers the
checking of some safety properties to runtime (e.g., termination,
integer errors, etc.).  It may be possible to reduce the number of
possible runtime errors by incorporating Rust-based verification
tooling to, for example, ensure freedom from
panics~\cite{verus,paniccheck,rvt}.  However, we note that push-button
techniques such as PanicCheck~\cite{paniccheck} are likely to
reintroduce the language/verifier gap.  Instead, we suspect that using
frameworks that combine proofs and programming~\cite{coq,dafny}, such
as Verus~\cite{verus} (for Rust) may allow \projname{} to reduce
runtime errors without the language/verifier gap.

\para{Unprivileged Extensions} In our safety model, extensions are
installed by a privileged user; they are trusted but may be buggy.
There have been proposals to support untrusted, unprivileged
extensions for various use cases, including system call
filtering~\cite{jia2023}.  Though these scenarios will also
suffer from the language/verifier gap, it is not clear that a
language-based approach like \projname{} is an adequate solution in
this case, since the Rust compiler and toolchain form a larger trusted
computing base than an in-kernel verifier to provide safety
properties.  We note that, even with the in-kernel verifier,
guaranteeing safety remains a
challenge~\cite{untenableVerification,ebpf-stackoverflow,ebpf-termination}.



\para{Unsafe Rust code in \projname{} kernel crate:}
% Unsafe code is required to interact with low-level kernel code/data and be
%   compliant with certain kernel ABIs
%   - Kernel helper functions requires FFI call
%   - converting unsafe C types into safe Rust types
%   - accessing kernel per-CPU definition
% All unsafe Rust code presents in the kernel crate
%   - set to be developed by trusted and experienced maintainers
%   -
% The program is always implemented by only safe Rust, thereby making the
%   program subject to all safety checks in Rust.
% Recent works like verus employs formal verification on Rust code and provides
%   further guarrantees.
As \projname{} kernel crate serves as an interface to the kernel for the
    extension programs, it inevitably employs unsafe Rust code.
This is needed because interacting with low-level kernel code and data requires
    kernel crate to access unsafe C types and invoking kernel functions through
    the FFI interface.
Furthermore, certain ABIs of the Linux kernel also makes unsafe code a
    necessity -- accessing per-CPU data requires inline assembly code as well
    as direct pointer arithmetics.
\projname{} limits all unsafe code to the kernel crate which is implemented by
    trusted and experienced maintainers.
The extension program itself is always implemented only in safe Rust, thereby
    making the program subject to all safety checks in Rust.
At the same time, recent work~\cite{verus} has explored formal verification
    techniques on Rust code, which provides additional safety guarantees
    for the correctness of unsafe code beyond these provided by the compiler.

\para{Dynamic memory allocation:}
% eBPF supports dynamic allocation since 6.2
%   - dedicated all-context memory allocator
%   - as kfunc
%   - alloc and free need to match
% Rex currently does not support dynamic allocation
%   - still possible to back the Rust memory allocator using eBPF allocator
%   - allows more advanced use cases
%   - makes more components of Rust standard library, e.g. collection types
%   - usability: drop is handled automatically by compiler
Since Linux kernel v6.2, eBPF supports dynamic allocations in extension
    programs~\cite{Dwivedi-958cf2e273f0}.
Programs can request memory from the kernel using the allocation kfuncs.
Similar to memory management in C, the verifier requires any allocated memory
    to be manually freed.
The allocation API is based on the dedicated, all-context eBPF memory
    allocator~\cite{bpf-mempool-lwn}, which internally uses a memory pool
    implementation.
\projname{} currently does not support dynamic memory allocation.
However, we expect it to be possible to integrate memory allocation of Rust
    with the eBPF all-context allocator, effectively granting \projname{}
    dynamic allocations.
Dynamic allocation enhances programmability of extension programs and opens
    up more advanced use cases.
Furthermore, dynamic allocation will also make more components of the Rust
    standard library available, notably the collection and smart pointer types.
With these types the extension developer no longer needs to manage memory
    manually, as the compiler will handle the lifetime of these objects and
    drop them automatically.

\label{discussion:versions}\para{Version Mismatches:}
% rex fixes mismatches between compiler and verifier by removing the verifier
% for mismatches between kernel versions, Rex's kernel crate itself does not
%   contain kernel version-specific code
% rex's model requires the programs to be compiled on the target kernel,
%   and the build process generates kernel version specific bindings for the
%   programs
There are three sources of versioning that eBPF currently has, that may lead to issues: kernel interface, verifier, and the compiler.
Kernel interface version problems are resolved by the use of BTF and CO-RE~\cite{bpf-core} in BPF.
However, the version issues differences between the compiler and verifier are not dealt
    with in any way.
The compiler and verifier are decoupled in their development, so there will
    always be gaps between them.
\projname{}'s elimination of the in-kernel verifier effectively eliminate the
    mismatch issue between the compiler and the verifier.
As for the problem of API changes across kernel versions, \projname{}'s kernel
    crate does not contain any kernel-version-specific code.
\projname{}'s deployment model requires the programs to be compiled on the
    target kernel and build process generates Rust bindings specific to the
    target kernel.

%In the current eBPF system, the compiler and the verifier are decoupled.
%As development proceeds, implementation details about the compiler and verifier change.
%Problems can also arise from different verifier versions.
%If an eBPF program verifies on one version, there is no guarantee that it verifies on a different version.
%Examples of this include backwards compatibility for features like loops.
%There is no way to fully resolve the issues of versioning in the eBPF system as
%    each component is a constantly moving target.

% \para{Static memory efficiency:}
% % from eval: memory is more efficient when there are more programs defined in
% %   the same program
% % Use cases like KCFI require a lot of programs, rex's ability of pack the code
% %   together without forced code duplication is more effecient (we expect)
% As discussed in \S\ref{eval:mem-footprint}, the static memory footprint of
%     \projname{} is more efficient when more programs are defined togetherc in
%     the same project.
% Recent work has proposed use cases that require potentially a large number of
%     programs~\cite{ebpf-kcfi}, where different programs share a common, central
%     logic.
% We expect \projname{} to be more effecient in static memory footprint under
%     such conditions, given its ability of packing the program and data together
%     without forced code duplication that happens in eBPF.

% \para{Program nestings}
% \jinghao{TODO}