Resources: A Safe Language Abstraction for Money

TL;DR

This paper introduces a new resource-safe programming abstraction for digital currency in the Move language, enhancing security and expressiveness for smart contract development on blockchain platforms.

Contribution

It presents a novel linear resource type system with formal semantics and proves resource safety, improving security in smart contract programming.

Findings

Move's resource types prevent resource duplication and loss.

The bytecode language with resources is proven to be resource safe.

The approach enhances security in blockchain smart contracts.

Abstract

Smart contracts are programs that implement potentially sophisticated transactions on modern blockchain platforms. In the rapidly evolving blockchain environment, smart contract programming languages must allow users to write expressive programs that manage and transfer assets, yet provide strong protection against sophisticated attacks. Addressing this need, we present flexible and reliable abstractions for programming with digital currency in the Move language [Blackshear et al. 2019]. Move uses novel linear [Girard 1987] resource types with semantics drawing on C++11 [Stroustrup 2013] and Rust [Matsakis and Klock 2014]: when a resource value is assigned to a new memory location, the location previously holding it must be invalidated. In addition, a resource type can only be created or destroyed by procedures inside its declaring module. We present an executable bytecode language with resources and prove that it enjoys resource safety, a conservation property for program values that is analogous to conservation of mass in the physical world.