  The Move language provides abstractions for programming with digital assets
via a mix of value semantics and reference semantics. Ensuring memory safety in
programs with references that access a shared, mutable global ledger is
difficult, yet essential for the use-cases targeted by Move. The language meets
this challenge with a novel memory model and a modular, intraprocedural static
reference safety analysis that leverages key properties of the memory. The
analysis ensures the absence of memory safety violations in all Move programs
(including ones that link against untrusted code) by running as part of a
load-time bytecode verification pass similar to the JVM [12] and CLR [15]. We
formalize the static analysis and prove that it enjoys three desirable
properties: absence of dangling references, referential transparency for
immutable references, and absence of memory leaks.
