Pointer assertion logic & data structure invariant of MIR programs
Author
Boelt, Anders Hahn
Term
4. term
Education
Publication year
2023
Submitted on
2023-06-16
Pages
71
Abstract
Rust is a programming language designed to prevent many memory errors. In this work, we explore whether the Pointer Assertion Logic Engine (PALE) can be used to check properties of Rust programs. Our approach is to translate Rust’s Mid-Level Intermediate Representation (MIR), a middle-layer form of the code, into PALE to enable semi-automatic formal reasoning about a program’s memory. Using program annotations and so-called Graph Types, we aim to prove that data-structure invariants are preserved. As a case study, we model an intrusive, circular, doubly linked list from the Rust-for-Linux project in PALE. We define invariants for this structure and attempt to show the absence of memory faults. We conclude that PALE, together with monadic second-order logic, is a promising direction for further study, but our MIR-to-PALE translation does not yet have a formal proof of correctness, so the results should be viewed as preliminary.
Rust er et programmeringssprog, der er designet til at undgå mange hukommelsesfejl. I dette arbejde undersøger vi, om Pointer Assertion Logic Engine (PALE) kan bruges til at kontrollere egenskaber ved Rust-programmer. Vores idé er at oversætte Rusts Mid-Level Intermediate Representation (MIR), en mellemliggende form af koden, til PALE for at muliggøre semi-automatisk, formel ræsonnering om programmets hukommelse. Med programannoteringer og såkaldte Graph Types forsøger vi at bevise, at datastrukturers invarianter bevares. Som case modellerer vi en intrusiv, cirkulær, dobbeltkædet liste fra Rust-for-Linux-projektet i PALE. Vi definerer invarianter for denne struktur og forsøger at vise fravær af hukommelsesfejl. Vi konkluderer, at PALE kombineret med monadisk andenordens logik er en lovende retning for videre arbejde, men vores MIR-til-PALE-oversættelse mangler endnu et formelt bevis for korrekthed, så resultaterne er foreløbige.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords