Rust's Borrow System in Static Analysis: Exploring Usages and Benefits of Rust’s Borrow System Through Static Taint Analysis
Authors
Kristensen, Mathias Knøsgaard ; Petersen, Felix Cho ; Andersen, Simon Vinberg
Term
4. term
Education
Publication year
2022
Submitted on
2022-06-16
Pages
60
Abstract
Dette projekt undersøger, om Rusts lånesystem (de regler, som borrow-checkeren håndhæver for, hvem der må læse og skrive data, og hvor længe referencer er gyldige) kan gøre statiske programanalyser mere effektive. Statisk analyse undersøger kode uden at køre den; en taint-analyse sporer for eksempel, hvordan ikke-betroede data flyder gennem et program. Vi gennemgår faserne i Rusts kompilator, forklarer ikke-leksikale levetider (en funktion der lader kompilatoren spore levetider mere fleksibelt end blot efter kodeblokke), og giver en præcis definition af 'lån' i Rust. Vi indsnævrer denne definition med klare regler i naturligt sprog, bygger en enkel model af Rusts mellemniveau-repræsentation (MIR) med ekstra annoteringer, og oversætter nogle af reglerne til boolsk logik. Med en taint-analyse som case undersøger vi, om denne instrumentering og logik hænger sammen. Vi skitserer også, hvordan ikke-leksikale levetider kan danne grundlag for en analyse, der reducerer antallet af programtilstande, analysen skal gennemgå. Analysen er ikke implementeret, så resultaterne er teoretiske. Vores evaluering antyder, at udnyttelse af Rusts låneinformation kan reducere mængden af kode eller tilstandsrummet, der skal analyseres, men uden en implementering er beviserne uklare. Arbejdet er en delvis succes og et grundlag for videre arbejde.
This thesis asks whether Rust's borrowing system (the rules enforced by the borrow checker about who can read and write data and how long references stay valid) can make static program analyses more effective. Static analysis checks code without running it; taint analysis, for example, tracks how untrusted data flows through a program. We review the stages of the Rust compiler, explain non-lexical lifetimes (a feature that lets the compiler track lifetimes beyond simple block scopes), and give a precise definition of borrowing in Rust. We narrow this definition with clear natural-language rules, build a simple model of Rust's mid-level IR (MIR) with extra annotations, and translate some of the rules into Boolean logic. Using a taint analysis as a case study, we test whether this instrumentation and logic are coherent. We also outline how non-lexical lifetimes could form the basis of an analysis that reduces the number of program states an analysis must explore. We do not implement the analysis, so our results are theoretical. Our evaluation suggests that leveraging Rust's borrowing information could reduce the amount of code or state space that needs to be analyzed, but without an implementation the evidence is inconclusive. We consider the work a partial success and a foundation for further research.
[This summary has been rewritten with the help of AI based on the project's original abstract]
Keywords
Documents