Robust Safety for Move

TL;DR

This paper defines and formalizes robust safety for the Move programming language, introducing a static verification framework with an encapsulator that ensures security properties hold in open-world scenarios, demonstrated on real-world Move programs.

Contribution

It presents a theoretical framework for robust safety in Move, including an encapsulator and escape analysis, and implements a practical toolchain that certifies over 99% of analyzed modules.

Findings

The framework achieves high certification rates on real-world Move modules.

The encapsulator effectively generalizes static verification results to open-world settings.

The approach enhances Move's security guarantees for smart contracts.

Abstract

A program that maintains key safety properties even when interacting with arbitrary untrusted code is said to enjoy \emph{robust safety}. Proving that a program written in a mainstream language is robustly safe is typically challenging because it requires static verification tools that work precisely even in the presence of language features like dynamic dispatch and shared mutability. The emerging \move programming language was designed to support strong encapsulation and static verification in the service of secure smart contract programming. However, the language design has not been analyzed using a theoretical framework like robust safety. In this paper, we define robust safety for the \move language and introduce a generic framework for static tools that wish to enforce it. Our framework consists of two abstract components: a program verifier that can prove an invariant holds in a closed-world setting (e.g., the Move Prover), and a novel \emph{encapsulator} that checks if the verifier's result generalizes to an open-world setting. We formalise an escape analysis as an instantiation of the encapsulator and prove that it attains the required security properties. Finally, we implement our encapsulator as an extension to the Move Prover and use the combination to analyze a representative benchmark set of real-world \move programs. This toolchain certifies $>$99\% of the \move modules we analyze, validating that automatic enforcement of strong security properties like robust safety is practical for \move.