4 papers
Adding Compilation Metadata To Binaries To Make Disassembly Decidable
Daniel Engel, Freek Verbeek, Pranav Kumar +1
The binary executable format is the standard method for distributing and executing software. Yet, it is also as opaque a representation of software as can be. If the binary format…
BeePL: Correct-by-compilation kernel extensions
Swarn Priya, Frédéric Besson, Connor Sughrue +4
eBPF is a technology that allows developers to safely extend kernel functionality without modifying kernel source code or developing loadable kernel modules. Since the kernel gover…
Augmented Weak Distance for Fast and Accurate Bounds Checking
Zhoulai Fu, Freek Verbeek, Binoy Ravindran
This work advances floating-point program verification by introducing Augmented Weak-Distance (AWD), a principled extension of the Weak-Distance (WD) framework. WD is a recent appr…
Formally Verified Binary-level Pointer Analysis
Freek Verbeek, Ali Shokri, Daniel Engel +1
Binary-level pointer analysis can be of use in symbolic execution, testing, verification, and decompilation of software binaries. In various such contexts, it is crucial that the r…