sail-ebpf

sail-ebpf is a Sail model of the eBPF ISA. The project provides executable instruction semantics, generated reference formal specifications, and Rocq/Coq extraction for formal reasoning.

The current model covers ALU instructions, jumps, calls and exits, tail calls, LDDW, regular memory accesses, Linux probe loads, acquire/release loads and stores, and word/double-word atomic read-modify-write instructions. Memory accesses are expressed through the Sail v1 concurrency interface. The Rocq side can instantiate those effects with a sequential CompCert-memory backend.

Project layout

.
+-- CMakeLists.txt              # top-level build entry
+-- model/                      # main Sail eBPF model
+-- model_manual/               # presentation-oriented Sail model for manuals
+-- handwritten_support/        # handwritten Rocq/CompCert support layer
+-- doc/
|   +-- sail-ebpf-manual.adoc   # manual template
|   +-- tools/                  # JSON post-processing for the manual
|   +-- generated/              # generated intermediate JSON files
+-- reference/                  # reference material

model/ is the semantic source model. model_manual/ is a presentation model used for the final manual; many helper functions are expanded there by hand so that the generated manual can show per-instruction semantics directly.

Environment setup

Install the basic system tools:

sudo apt install cmake ninja-build ruby graphviz z3

Install Sail and Rocq/Coq dependencies with opam:

opam init
opam switch create sail-ebpf ocaml-base-compiler.5.2.1
eval "$(opam env)"

opam repo add coq-released https://coq.inria.fr/opam/released
opam install sail coq coq-stdpp coq-compcert

Install the Ruby tools required for PDF manual generation:

gem install asciidoctor-pdf asciidoctor-diagram asciidoctor-sail

Configure the build directory:

cmake -S . -B build -G Ninja

Build commands

Build both PDF manuals:

cmake --build build --target docs

Outputs:

doc/sail-ebpf-manual-source.pdf
doc/sail-ebpf-manual-final.pdf

The first one (*-source.pdf) is generated directly from model/, while the second one (*-final.pdf) is generated from model_manual/ with some post-process on the encoding diagram. Hence doc/sail-ebpf-manual-final.pdf is the final specification document of the project.

Generate Rocq/Coq files and compile them successfully:

cmake --build build --target rocq_build