The Move Borrow Checker

TL;DR

The paper introduces a novel static reference safety analysis for the Move language that guarantees memory safety and prevents leaks, dangling references, and unsafe access in programs manipulating digital assets.

Contribution

It presents a new memory model and a modular static analysis that ensures memory safety in Move programs, including untrusted code, with formal proofs of safety properties.

Findings

Analysis guarantees absence of dangling references

Ensures referential transparency for immutable references

Prevents memory leaks in Move programs

Abstract

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.