As part of our work, we seek to understand how to eliminate vulnerability classes. Designing safer languages enables developers to write code with confidence. How exactly does Move lend itself to safer programming practices? What can we learn from Move to generalize secure design principles for other execution environments?

Lately, there appears to be many buzzwords floating around. Formal verification, type based safety, "rust but for blockchain".

In this piece I'll seek to discuss exactly how move lends itself to more secure programming practices, potential shortcomings, and practical design tips for protocol developers looking to build structurally safer programs.

Types

One of the key selling points of Move is the use of typed resources. Aptos and Sui have slight variations in how they materialize this pattern, but as an example take coin.move.

  /// Main structure representing a coin/token in an account's custody.
  struct Coin<phantom CoinType> has store {
      /// Amount of coin this address has.
      value: u64,
  }

aptos

  /// A coin of type `T` worth `value`. Transferable and storable
  struct Coin<phantom T> has key, store {
      id: UID,
      balance: Balance<T>
  }

sui

Pulling an example from Pontem Network's Liquidswap DEX implementation on Aptos, we can see that LiquidityPool natively embeds this type information into it's fields.

    /// Liquidity pool with reserves.
    struct LiquidityPool<phantom X, phantom Y, phantom LP> has key {
        coin_x_reserve: Coin<X>,
        coin_y_reserve: Coin<Y>,
        // ...
    }

This has the advantage of aligning type information at compile time. It would be difficult to accidentally pass in the wrong type of coin to a function.

      public fun mint<X, Y, LP>(
          pool_addr: address,
          coin_x: Coin<X>,
          coin_y: Coin<Y>
      ): Coin<LP> acquires LiquidityPool, EventsStore {
          // ...

          let (x_reserve_size, y_reserve_size) = get_reserves_size<X, Y, LP>(pool_addr);

As an aside, this generic type information is implemented at runtime in the ty_args at the vm level. This VM level implementation choice makes it rather difficult to iterate over arbitrary generic types, such as with summing the coins in a pool. We will be releasing a deep dive into move's VM internals shortly.

In pseucode, this checks that coin_x.type is equal to pool.x_type, and coin_y.type is equal to pool.y_type.

This type system has two advantages

1. It's required. The type parameter must be specified so it's impossible to forget such a constraint
2. It's concise. Constraints are done via type parameter alignment instead of verbose equivalence checks

However, this system isn't perfect.

In fact, I would go as far as to argue that using types to create such associations is an anti-pattern.

Using types to enforce relationships only works because types are uniquely associated with instances. For example, in Aptos's coin initialization function, they explicitly assert that there hasn't been a previously initialized CoinInfo<CoinType>.

  fun initialize_internal<CoinType>(
      // ...
  ): (BurnCapability<CoinType>, FreezeCapability<CoinType>, MintCapability<CoinType>) {
      // ...

      assert!(
          !exists<CoinInfo<CoinType>>(account_addr),
          error::already_exists(ECOIN_INFO_ALREADY_PUBLISHED),
      );

While this CoinInfo isn't returned directly, it still ensures uniqueness of the capability objects.

Similarly, consider Aries Markets, a lending/borrowing protocol building on Aptos.

Their ReserveCoinContainer struct stores all the relevant data and resources for managing a lending market.

  /// The struct to hold all the underlying `Coin`s.
  /// Stored as a resources.
  struct ReserveCoinContainer<phantom Coin0> has key {
      /// Stores the available `Coin`.
      underlying_coin: Coin<Coin0>,
      /// Stores the LP `Coin` that act as collateral.
      collateralised_lp_coin: Coin<LP<Coin0>>,
      /// Mint capability for LP Coin.
      mint_capability: MintCapability<LP<Coin0>>,
      /// Burn capability for LP Coin.
      burn_capability: BurnCapability<LP<Coin0>>,

      // ...
  }

When creating a ReserveCoinContainer, uniqueness is implicitly enforced by moving it into a hardcoded address.

  public(friend) fun create<Coin0>(
      lp_store: &signer,
      // ...
  ) acquires Reserves {
      lp::assert_is_lp_store(signer::address_of(lp_store));

      // ...

      move_to(lp_store, ReserveCoinContainer<Coin0> {
        // ...
      });

In both these instances, type association only works because we create exactly one instance per type.

On the other hand, consider if you have a Position<T> and a Market<T> where T is the coin type.

    struct Market<phantom T> {
        reserves: Coin<T>,
        // ...
    }

    struct Position<phantom T> {
        amount: u64,
        // ...
    }

If Market<T> isn't a unique type -- or in other words if you're able to create more than one instance of a market per type T -- you might be able to pass in the incorrect market for a given position. This is a common vulnerability pattern on Solana.

Dynamic iteration of types is also impossible (at least as currently designed by the Move VM) leading to massive headaches for developers. In these scenarios, we empirically observe developers defaulting back to type reflection APIs, complicating code unnecessarily. Security at the expense of usability comes at the expense of security.

    /// Get the price of the token per lamport.
    public fun get_price(type_info: TypeInfo): Decimal acquires Oracle {
        let oracle = borrow_global_mut<Oracle>(@oracle);
        let price = table::borrow_mut_with_default<TypeInfo, Decimal>(
            &mut oracle.prices,
            type_info,
            decimal::one()
        );
        *price
    }

Type association feels like a proxy for the intended pattern -- associating resources with instances. It's very useful being able to store a reference to an instance of another resource (which is possible in Diem style move).

In summary, when using type systems to bind resources to each other, it's important to either

1. Have unique initializers for your resources
2. Associate resources with instances directly

Formal Verification

Formal verification is another exciting feature.

As part of our work with protocols, we actively use formal verification to prove aspects of security.

However, this isn't a silver bullet. The key is figuring out what to prove.

One obvious idea might be a properties across a particular function. For example, we might want to ensure that a swap doesn't reduce the value of the pool -- similar to the Solana AMM rounding issue we reported.

However, this could also be checked with a simple runtime assert. For example, we recommended Pontem assert that liquidity pool token values are strictly increasing.

  let cmp = u256::compare(&lp_value_after_swap_and_fee, &lp_value_before_swap_u256);
  assert!(cmp == 2, ERR_INCORRECT_SWAP);

The move prover really shines when we're proving relationships between functions.

One example of a more complicated relationship that can't be proved easily via assertions would be the no_free_money_theorem in the move repository.

  // #[test] // TODO: cannot specify the test-only functions
  fun no_free_money_theorem(coin1_in: u64, coin2_in: u64): (u64, u64) acquires Pool {
      let share = add_liquidity(coin1_in, coin2_in);
      remove_liquidity(share)
  }
  spec no_free_money_theorem {
      pragma verify=false;
      ensures result_1 <= coin1_in;
      ensures result_2 <= coin2_in;
  }

There's no clean way to express this with an assert because this makes an observation across two functions which are temporally separated.

Invariant's are also extremely useful. For example, enforcing invariants about fee parameters (fee can never be greater than 100%) or pool supply makes it a lot easier to reason about the protocol.

For example, Ian uses invariants to clearly define core properties of his AMM state.

spec PoolState {
    invariant supply >= MINIMUM_LIQUIDITY;
}

Another useful pattern for the Move prover is aborts_if. More specifically, it can be very helpful to assert that a function never aborts, with aborts_if false.

Although loop invariants are a bit clunky, Ian is also able to prove that a relatively nontrivial function doesn't abort.

  fun multiply_vec_by_n_coins(input: vector<u64>): vector<u128> {
      let amounts_times_coins = vector::empty<u128>();
      let i = 0;
      let n_coins = vector::length(&input);
      while ({
          spec {
              invariant len(amounts_times_coins) == i;
              invariant i <= n_coins;
              invariant forall j in 0..i: amounts_times_coins[j] == input[j] * n_coins;
          };
          (i < n_coins)
      }) {
          vector::push_back(
              &mut amounts_times_coins,
              (*vector::borrow(&input, (i as u64)) as u128) * (n_coins as u128)
          );
          i = i + 1;
      };
      spec {
          assert i == n_coins;
          assert len(input) == n_coins;
      };
      amounts_times_coins
  }
  spec multiply_vec_by_n_coins {
      pragma opaque;
      aborts_if false;
      ensures len(result) == len(input);
      ensures forall j in 0..len(input): result[j] == input[j] * len(input);
  }

Closing Thoughts

In this post, we explored implications of Move's type system and formal verification, two powerful features of the Move language that enable safer programming languages.

While Move as a language is still a language in active development, it shows some exciting features that seem allows developers to create structurally safer programs.

We're passionate about pushing the edge of what's possible in Move security. If you have any thoughts, or would like to explore an audit, feel free to reach out to me @notdeghost.