Detecting Undefined Behavior Across Foreign Function Boundaries in Rust Programs

Master Thesis (2025)
Author(s)

J.P. de Jeu (TU Delft - Electrical Engineering, Mathematics and Computer Science)

Contributor(s)

Andreea Costea – Mentor (TU Delft - Programming Languages)

Jesper Cockx – Mentor (TU Delft - Programming Languages)

Mitchell Olsthoorn – Graduation committee member (TU Delft - Software Engineering)

Faculty
Electrical Engineering, Mathematics and Computer Science
More Info
expand_more
Publication Year
2025
Language
English
Graduation Date
10-09-2025
Awarding Institution
Delft University of Technology
Programme
['Computer Science']
Faculty
Electrical Engineering, Mathematics and Computer Science
Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Abstract

Memory access bugs exist in almost every compiled programming language. To solve this, modern programming languages like Rust use complex variable ownership systems that ensure memory safety. These kinds of ownership systems can be used to distinguish between variables that can only be read and ones that can be safely written to as well. These strict ownership rules are, however, limited when using external libraries. While the Foreign Function Interfaces (FFI) used to show what arguments external functions use can be written with these ownership requirements, enforcing them on the side of the external library is not required, potentially resulting in a discrepancy between what is expected on Rust's side and what happens in the external library.

To solve this problem we propose a novel mechanism for detecting memory safety violations across language boundaries. We implemented it in a tool called MiriPBT: a combination of MIRI, a tool that can enforce ownership rules at runtime, MiriLLI, an extension of MIRI that allows ownership rules to be enforced on the other side of the FFI boundary, and Property Based Testing, which allows us to greatly increase the size of the domain we can test. We use Rust's type system to generate inputs for the PBT and use the runtime checks of MIRI and MiriLLI to check if any ownership rules are violated. Finally we present the result of the PBT in a format an average Rust user can easily understand, helping them resolve any FFI related ownership bugs in their code.

Files

ThesisJuliusDeJeu.pdf
(pdf | 1.29 Mb)
License info not available