This report explores potential benefits that Rust’s
borrowing system might confer to static analyses.
Furthermore, this report showcases some of these
benefits via application in a static taint analysis.
We did this by first establishing an overview of the
borrowing system, the stages of the Rust compiler,
and exploring the novel non-lexical lifetimes con-
cept which is the current basis for the borrowing
system.
We then established a definition for what ’borrow-
ing’ means in a Rust context, and what precisely this
entails. Next, we defined predicates in natural lan-
guage, to limit the broader borrowing definition pre-
sented before. After this, a syntax and instrumented
semantics for Rust’s MIR compilation layer is pre-
sented. This is followed by definitions for some of
the predicates, written in more precise boolean alge-
bra.
A static taint analysis is presented to ascertain
whether the instrumentation and boolean algebra
holds. Furthermore, we presented the basis for an
analysis based in non-lexical lifetimes. The analysis
is never implemented, but we present the theoretical
basis for possibly reducing the state space needed to
search through for a given program.
The report concludes with an evaluation of the the-
ory presented. We conclude that analyses may ben-
efit from the borrowing system, by leveraging it to
possibly reduce the total amount of program that re-
quires analysis. However, nothing conclusive can be
drawn from the results due to the lack of proper im-
plementation. We deem the project a partial success,
both deserving of and requiring additional work.