My Bachelor's Thesis (including source sode): Testing the Red-Black Tree Implementation of the Linux Kernel against a Formally Verified Variant

Abstract

This thesis shows how to construct evidence of correctness for the Red-Black tree (RBT) implementation of the Linux kernel through testing and formal verification. First, it describes how to verify the results of kernel RBT operations by comparing them against the results of a formally verified RBT variant. Second, it shows how modifying this verified implementation and identifying new invariants makes it possible to prove the correctness of the kernel RBT insert algorithm in Isabelle/HOL.

Structure

• module hosts the Linux kernel module.
• harness hosts the testing harness together with the verified RBT Haskell variant.
• HOL-RBT hosts the Isabelle/HOL formalization and proof of the Kernel RBT insert routine. It also includes an Isabelle file to export the original verified Isabelle/HOL RBT to Haskell.
• userspaceRBT hosts the modified kernel RBT implementation that I lifted to userspace, a Makefile to start a symbolic execution with KLEE using make symbolic STDIN_SIZE=<N> (where <N> is even; requires KLEE & LLVM). In the thesis' evaluation I used N=14. The final test cases of this execution are in userspaceRBT/klee-out_STDIN_SIZE=14. cov.sh reproduces the coverage data shown in the thesis.