Cointime

Download App
iOS & Android

Moving the Immovables: Lessons Learned From Our Aptos Smart Contract Audit

Validated Project

Move is a programming language specifically designed for building secure and formally verified smart contracts. Move’s language features provide a strong set of security protections through strict type enforcement and load-time verifications. Developers who master Move’s built-in resources and programming patterns can produce more secure projects than those developed in conventional languages that lack these features.

However, in the course of our work auditing smart contracts written in Move, most notably the novel Layer 1 blockchain Aptos, we have encountered multiple instances of developers either neglecting to use Move’s built-in protection mechanisms or adopting programming patterns that work counter to Move’s design philosophy. Such patterns are partially due to the relatively steep learning curve involved with adopting a new language, and partially a result of programmers simply “migrating” legacy code designs. We call such programming patterns immovables. This article presents a few such examples along with our suggestions for how to fix them.

Benefits of the Move Programming Language

(Note: This article summarizes some of our experiences in auditing Move smart contract code. It requires some basic knowledge about the Move language. See here for a detailed introduction to Move.

Some of the most important security features of Move include type safety, resource safety, and reference safety. Move embeds type information at the bytecode level, and provides mechanisms to specify and enforce resource ownership. The permitted behavior of each resource object is strictly verified at load time and enforced at run-time. In addition, the Move language design ensures no dangling references through ownership rules, similar to the Rust programming language. This article is not intended to be a review of the aforementioned features, but rather a discussion of the consequences and remediation of failing to utilize Move’s in-built features when writing smart contracts.

Aptos is a major blockchain project written using Move. Our team of expert engineers comprehensively reviewed Aptos's core code, and this blog post summarizes some of the issues encountered for the benefit of future projects leveraging the Move programming language.

Similar to Rust, Move provides a simplified and more restricted type system for developers to flexibly manage and transfer assets, while providing the security and protections against attacks on those assets. As shown in the example below, Move eliminates signed integer types from the primitive types, and only supports unsigned integers for built-in integer overflow detection.

Code Snippet 1: A simple u64 addition with built-in overflow detection

In Code Snippet 1, we define a function to add two u64 values. A runtime ARITHMETIC_ERROR will be triggered if the addition overflows, as shown in the test case below.

Move also provides a Prover that helps developers formally verify the properties of contract code. Developers can specify preconditions and postconditions for each function in spec blobs. After that, the Move Prover can prove whether the specified conditions are met, and provide concrete input if there is any violation. For example, we can verify the built-in overflow detection by writing the following spec.

 Spec 1. Specification for Code Snippet 1.

Immovables Resulting From Developers’ Legacy Burden

Despite having a number of powerful security features, Move developers still face the challenges of writing secure smart contracts. Inexperienced developers might use unsuitable legacy programming patterns with which they are more familiar or misuse some Move features due to the steep learning curve.

We noticed a few instances of programming patterns in recently developed projects written in Move that are countering the protection offered by the language’s strong type system and abstractions. Some of these patterns tend to bring back the same vulnerabilities that Move’s designers were trying to remove with novel language features. A couple of examples of these legacy patterns are:

  • Bringing back vulnerable types and avoiding the re-design of projects with Move types
  • Creating copyable objects and avoiding utilizing resources with ownership constraint

We call these legacy patterns the immovables in Move-based smart contracts. These immovables are especially common because many projects were ported by developers from projects built in other programming languages such as Solidity, which does not have the same strong type features (and constraints) in its language design. Below are a few examples of such patterns and their issues. We also provide some recommended remediations for each example.

Immovable #1: Resurrecting Vulnerable Types

Lots of smart contracts use signed integers for math in contract implementations. For developers that are used to implementing a contract using a signed integer, discovering that there are no signed integer types in Move might come as a surprise.

While experienced developers can choose to learn the built-in type in Move and reimplement the contract with only unsigned numbers, some developers choose to bring the signed integer type back to their Move code. We have observed a few cases in some Move projects. Below is a simplified version.

 Code Snippet 2: A vulnerable I128 implementation used in some Move contracts.

In this example, a developer chooses to implement their type of signed integer (i.e. I128). This is likely due to the fact that the reference implementation uses signed integers and the developer simply decided to keep the design. Using the above implementation actually introduces integer overflow problems.

Remediation

We advise developers not to import these unrecommended types to Move projects. The best practice is to redesign the application using the built-in Move types. However, for those cases where legacy patterns (such as signed integer objects) have to be used, we can leverage Move’s built-in prover to add a level of verification.

Below is an example of using the Move Prover to find property violations using the following specification. The spec ensures that the addition of two positive integers should result in a positive integer as well.

 Spec 2. Specification for Code Snippet 2.

With the above specification, we can run the built-in Move Prover. The outcome is shown below.

 Output 2. The Move Prover’s output for Spec 2 and Code Snippet 2.

The output shows that the Move Prover captured a violation of the spec. We recommend developers utilize the Prover to verify the self-defined type if they have to reintroduce legacy types.

Immovable #2: Misunderstood Reference Safety

The second example of an immovable pattern is related to the Move resource type. Move provides a new storage model that separates resource storages (defined as structs) under each account’s address, indexed by its type information. Developers need to add abilities annotations to control the copy, key, store, and drop properties of the resource.

The example below is a simplified buggy code that is supposed to manage a global resource Config. Multiple CoinStores are maintained in the Config indexed by coin_type. In each CoinStore, there is a fees field, specifying the fee rates for the current coin. In this example, the increase_fees function is intended to locate the global CoinStore resource and increases the fees field by 1.

 Code Snippet 3: Invalid update to global resource CoinStore.

The code contains a bug that results from the misuse of resource copy. The increase_fee function that calls the borrow_mut function, which should return a mutable reference of the CoinStore. However, it returns an owned object of CoinStore, which is a copy of the original one in the vector. As a result, any update in the increase_fees function doesn’t affect the global storage. Note that the implicit copy behavior of the CoinStore is allowed because that the developer assigns the copy ability to the structure definition.

 Spec 3. Specification for Code Snippet 3.

We can use the Move Prover to detect such bugs by specifying the Config resource to be modified by the increase_fees function. The Prover gives the unsatisfied error message as shown below, indicating that the increase_fees function does not change global resource Config.

 Output 3. Move Prover’s unsatisfied output for Code Snippet 3 and Spec 3.

Remediation

The above code can be simplified and made secure by adopting the Move resource ownership pattern. Below is an implementation using a config structure with a generic phantom type.

 Code Snippet 4: Recommended programming pattern to organize resources in Move.

We can further write the following spec to ensure the increase_fees function changes the global state.

 Spec 4. Specification for Code Snippet 4.

With the remediated implementation, the Prover proves the implementation satisfies the specification without raising any error.

 Output 4. Move Prover’s output for Code Snippet 4 and Spec 4.

Summary

This article highlights a few error-prone programming patterns we have encountered in Move projects. Such practices are mostly due to the porting of legacy programming designs from non-type-safe languages.

Fortunately, the Move language offers a built-in Prover that can help verify implementations. We show that some of the error-prone programming patterns can be verified and fixed by leveraging the Move Prover. A more thorough approach for developers is to learn and adopt the new design patterns in Move.

Stay tuned for an in-depth exploration of the Move Prover in an upcoming blog post.

Comments

All Comments

Recommended for you

  • SBF ordered to forfeit more than $11 billion

    SBF has been ordered to confiscate more than 11 billion US dollars. SBF has now been sentenced to 25 years in prison.

  • Former CEO of FTX and Alameda Research Sentenced to 25 Years in Prison for Fraud and Money Laundering

    Sam Bankman-Fried, the co-founder and former CEO of FTX and Alameda Research, has been sentenced to 25 years in prison for fraud and money laundering. The judge criticized Bankman-Fried's behavior during the trial and deemed a 25-year sentence to be sufficient. Bankman-Fried's sentence may send a message to the crypto industry and there is no possibility of parole, but he may earn "good time" credit for good behavior while incarcerated. Bankman-Fried was found to have misused over $8 billion in customer funds and will be serving time in prison for his actions. The trial emphasized the importance of not using customers' funds without their knowledge or approval.

  • Web3 AI training company FLock raises $6 million in seed funding

    Web3 artificial intelligence training company FLock has raised $6 million in seed funding led by Lightspeed Faction and Tagus Capital. FLock will use these funds to develop its team and build a federated learning-driven artificial intelligence training platform.

  • Prisma: Vault owners need to prohibit delegation of contracts related to LST and LRT

    The LSD stablecoin protocol Prisma Finance stated in a post that for vault owners, please prohibit delegating authorization of the LST contract starting with 0xcC72 and the LRT contract starting with 0xC3eA.

  • MAS: Singapore is working on global first-tier fund tokenization regulation

    Chia Der Jiun, Managing Director of the Monetary Authority of Singapore, introduced some fund tokenization pilots at an event for asset managers. These pilots are part of the Project Guardian and MAS Global Layer 1 (GL1) tokenization plans. Chia Der Jiun emphasized the advantages of tokenization in real-time settlement and process automation, which can improve efficiency and achieve greater customization of funds. UK asset management company Schroders and fund distribution platform Calastone are exploring this as part of the Project Guardian public blockchain trial in Singapore. A recent survey by Calastone showed that 96% of asset management companies in the Asia-Pacific region plan to launch tokenized products within three years. Chia stated that as these Project Guardian pilot projects approach commercialization, MAS is working with the pilot project managers to study the legal and regulatory treatment and impact of tokenized investment funds."

  • Indonesia's Financial Services Authority to Regulate Crypto Industry in 2025 with Evaluation in Regulatory Sandbox

    Indonesia's Financial Services Authority (OJK) will take over regulation of the crypto industry from the commodities agency Bappebti. Crypto firms must undergo evaluation in a regulatory sandbox before being licensed to operate in the country. The OJK aims to prioritize consumer protection and education, and firms operating without evaluation in the sandbox will be considered illegal. The sandbox provides a safe and isolated environment for testing and innovation development, helping to enhance security and responsible management in the financial sector. Once under OJK's oversight, crypto assets will likely be reclassified as financial instruments.

  • The Shenzhen Illegal Fund Raising Prevention Office issued a risk warning on the "DDO digital options" business

    The Shenzhen Office for Preventing and Dealing with Illegal Fundraising issued a risk warning regarding the "DDO digital option" business. The activities related to the DDO digital option business conducted in the name of Dingyifeng International are essentially the issuance and trading of virtual currencies. According to the "Notice on Further Preventing and Dealing with Risks of Speculation in Virtual Currency Trading" jointly issued by ten departments including the People's Bank of China in September 2021, it is clear that virtual currency-related business activities are illegal financial activities, and overseas virtual currency exchanges providing services to residents within China are also illegal financial activities. The activities conducted by Dingyifeng International in the name of serving residents within China are suspected of illegal fundraising and other illegal financial activities. Our office has organized relevant departments to carry out work, resolutely deal with illegal fundraising and criminal activities, and seriously investigate the legal responsibilities of relevant personnel. (Shenzhen Local Financial Supervision and Administration Bureau)

  • The Hong Kong Legislative Council plans to review the relevant stable currency consultation and sandbox legislation at the end of this year or next year

    Hong Kong legislator Wu Jiezhuang revealed that Hong Kong will release stablecoin consultation and sandbox (computer security mechanism), which will allow the industry to innovate digital asset projects in the sandbox environment. Relevant legislation will be reviewed in the Legislative Council at the end of this year or next year, which will help the entire digital asset industry ecosystem. Hong Kong has been improving the digital asset (virtual asset) market on different legal levels. Last year, there were regulations on virtual currency trading platforms and issuance systems.

  • Vitalik: Humanity needs to create a world where blockchain and artificial intelligence work together

    Vitalik Buterin, the founder of Ethereum, stated at BiddleAsia 2024 held at Signiel Seoul in the Songpa district on March 28 that artificial intelligence is a huge market and its importance is increasing day by day. We need to create a world where blockchain and artificial intelligence work together. Artificial intelligence can now create applications with 100 to 500 lines of code. Vitalik also stated that the ability to write 10,000 lines of code can eliminate most of the bugs in the Ethereum virtual machine.

  • South Korean RWA blockchain technology development company PARAMETA completed a new round of financing of approximately US$7.5 million

    South Korean RWA blockchain technology development company PARAMETA announced the completion of a new round of financing of KRW 9 billion (approximately $7.5 million), with Shinhan Hyperconnect Investment Fund under Shinhan Venture Investment and Korea Asset Investment & Securities participating. As of now, the company's total financing has reached KRW 25 billion (approximately $20.8 million). PARAMETA plans to use this investment to expand its own blockchain technology research and development capabilities to meet RWA technology needs and expand from core technologies such as engines/chains to service applications. Relevant services are expected to be launched within the year.