
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
