Sui Move Security: What the Language Guarantees and What It Misses

Where does Move arithmetic stop checking on Sui?

Move’s overflow checks do not detect bits lost during a shift. In the Sui Move VM, << and >> abort only when the shift amount is at least the width of the type, never because bits fell off the end. The shift amount is a u8, so a shift on a u256 cannot abort at all (VM source).

On May 22, 2025, an attacker drained about $223 million from Cetus, a decentralized exchange on Sui, and validators froze about $162 million of it (incident report). According to SlowMist's analysis, the attacker added about 10^34 units of liquidity to one pool and paid 1 base unit of the deposited token for it. The pool priced the deposit with checked_shlw from Cetus's integer-mate library, which reports whether shifting a u256 left by 64 bits would overflow:

public fun checked_shlw(n: u256): (u256, bool) {
    let mask = 0xffffffffffffffff << 192;
    if (n > mask) {
        (0, true)
    } else {
        ((n << 64), false)
    }
}

The mask is (2^64 - 1) x 2^192 instead of 2^192, so every input from 2^192 up to the mask passed the check and lost its top bits in the shift. The Move VM checked every other arithmetic operation on that path, down to a final cast to u64, but not the shift: it kept the low 256 bits and reported nothing.

Cetus's first fix set the mask to 1 << 192 but kept n > mask, which still let 2^192 through: it shifts to 2^256 and wraps to 0. A second commit the same day changed > to >=.

P1. If checked_shlw reports no overflow, shifting the result back by 64 bits returns the input. As a Certora Sui Prover rule, written in Move:

public fun p1_shlw_first_patch(n: u256) {
    let (r, overflow) = shlw_versions::checked_shlw_first_patch(n);
    if (!overflow) {
        cvlm_assert_msg((r >> 64) == n, b"bits lost with no overflow flag");
    };
}

The rule ranges over every u256 input. It is violated on the original version and on the first patch, and verified on the final version (run). On the first patch the counterexample is n = 2^192, and the same assertion, with n = 2^192 excluded by an assumption, is verified, so that value is the only counterexample (run).

Signed values are the second gap. Move on Sui has no signed integer types, so libraries store signed values in unsigned integers, and the type system sees a u256 either way. Aftermath Finance lost about $1.14 million on April 29, 2026 through an integrator fee that could be negative. The attacker set its own fee cap to 0 and a fee of 2^256 - 10^23, which a signed less_than_eq read as -100,000 in the protocol's 10^18 fixed-point scale and let through (OpenZeppelin). Settlement subtracted that negative fee from the attacker's collateral, which added to it.

P1b. A fee the check accepts is not negative when read as a signed value. On a fee check modeled on BlockSec's description, violated without a sign check and verified with one (run).

Rounding is left to the protocol: division truncates, and the type system has no view on which way a protocol should round. The fixed-point types in Sui’s standard library truncate as well: std::uq64_64::int_mul and int_div, for example, drop the fractional part. (Sui documentation), while OpenZeppelin's math library for Sui takes the rounding direction as an argument to mul_div (OpenZeppelin). In Certora's verification of Suilend, a double rounding in minting let a user operation lower the cToken ratio (M-01). After the fix, the rule that user operations never decrease that ratio is verified under assumptions the report lists, among them the permissioned forgive function left out, at most one deposit and one borrow per obligation, and loops unrolled once.

How does access control work in Sui Move?

Authorization in Sui Move is enforced through a function's signature or its body: a privileged function takes a capability object such as an AdminCap, which only its owner can pass into a transaction, or asserts that tx_context::sender() is an address the protocol configured. The sender is the address that signed the transaction, and every command in a programmable transaction block (PTB) runs with that same sender (tx_context). In a sponsored transaction the sender is still the user, not the address that pays for gas (Sui documentation). The type system enforces what the signature asks for and nothing more. A public or entry function that takes no capability and checks no sender is open to every address, and any transaction can reference a shared object.

Typus Finance lost about $3.44 million on October 15, 2025 because update_v2, in an oracle module outside the scope of its May 2025 audit, lacked an assert and let any address update prices (post-mortem).

A public function can also pay the wrong party with no access check missing. In Certora's review of TradePort's Gold Strategy, the permissionless apply_strategy swapped protocol fees through a router that refunds unspent input to tx_context::sender(), so any caller could force a partial swap and collect the leftover USDC (M-01, fixed). Any PTB can call a public function, so in a permissionless function the sender is whoever chose to call it.

P2. A price update that succeeds was sent by the oracle's updater. On an oracle modeled on the Typus post-mortem, violated without the sender check and verified with it (run).

Objects that do not belong together: the Scallop exploit

Move checks the type of each argument, not how two arguments relate, so a function that takes an account and a pool has to compare their IDs itself. DeepBook v3 does this for its flash loans: the FlashLoan hot potato carries the pool's ID (Trail of Bits), and return_flashloan_base aborts with EIncorrectLoanPool unless the loan goes back to the pool it came from (Sui documentation).

Scallop lost about 150,098 SUI, about $142,500, on April 26, 2026 because one function skipped that check. spool::user::update_points was the one user function in its module that did not call spool_account::assert_pool_id. The attacker staked 0.2 SUI, passed a fresh sSUI account together with a deprecated sWETH pool whose reward index was about 891 trillion, and was credited about 162 trillion points.

P3. update_points succeeds only for an account whose pool ID equals the ID of the pool passed with it. On a rewards pool modeled on Blockaid's analysis, violated without the pool check and verified with it (run).

What happens to old code after a Sui package upgrade?

Old code stays callable after a Sui package upgrade. An upgrade publishes a new package and leaves the old one on chain, and nothing prevents a transaction from calling the old version's functions. Objects do not belong to a package version, so a shared object is reachable from every version, and without versioning an attacker can keep calling the version 1 functions on it (Move Book).

The documented defense is a version field on each shared object, a VERSION constant in the package, and a check at the top of every function that touches the object. Adapted from the Sui documentation:

public fun swap(pool: &mut Pool, /* ... */) {
    assert!(pool.version == VERSION, EWrongVersion);
    // ...
}

After an upgrade, an admin-gated migrate function sets the field to the new VERSION, and the old package's functions abort on that object. Nothing in the type system puts the check into every function, and one that leaves it out keeps working from every old version.

The upgrade path belongs in the audit scope too. Nemo lost about $2.59 million on September 7, 2025 through code added after its audit and never audited: a flash loan function left public and a query function that could change state (incident report). That code shipped through a single-signature upgrade address. Deprecating a pool does not remove it either: Blockaid describes the sWETH pool in the Scallop exploit as deprecated, and the attacker could still pass it to update_points.

P4. A deposit succeeds only on a pool at the package's current version. On a pool with one function that has the version check and one that leaves it out, violated on the second and verified on the first (run).

Nine properties for Sui protocols, from shifts to liquidations

P1 to P4 extend the rules above to every function they apply to. P5 to P8 are invariants of the protocol itself, which must hold after every call, whoever makes it. Each one can be written as a Certora Sui Prover rule:

• P1. Every left shift on a value path keeps all of its input's bits, or the transaction aborts.
• P1b. A quantity that must not be negative, such as a fee, is never negative when the code reads it as a signed value.
• P2. Only the matching capability or the configured address changes fees and configuration, and prices change only through that path or through an oracle update the protocol verifies. A function anyone can call pays its caller only what the protocol intends.
• P3. Every function that takes two related objects checks that they belong together.
• P4. Every function that touches a versioned shared object checks its version.
• P5. The amount a protocol records as held in each pool or reserve never exceeds the balance it holds.
• P6. A share's value never decreases outside a recorded loss or a documented fee, and minting rounds against the depositor.
• P7. Adding liquidity and removing it again, with no trade, flash loan, reward accrual or donation in between, never returns more of either token than was deposited.
• P8. Outside price and interest updates, a healthy position stays healthy after any user operation, and a liquidation never raises the loan-to-value ratio of a position with more collateral than debt.

Certora's Suilend report includes rules for versions of P6 and P8. It also found that on the original code, liquidating a position whose loan-to-value ratio was above 1/(1 + bonus) raised that ratio instead of lowering it (M-02, fixed). A lending market with a fixed liquidation bonus raises the ratio the same way when it liquidates a position whose ratio is between 1/(1 + bonus) and 1, so it fails the second half of P8 by design, and an audit reports it as a design finding. Suilend's fix caps the bonus based on the current loan-to-value ratio.

Testing the five gaps with test_scenario and the Sui Prover

In Move unit tests, test_scenario can play the attacker: scenario.next_tx(attacker) starts a transaction from an address that holds no capability, and take_shared gives that transaction the shared objects any address can reference (Sui documentation). Each gap gets a test in which the attack must fail. Where the fix aborts, #[expected_failure(abort_code = ...)] makes the test fail if the call goes through:

• For P1, call every function that shifts or casts with inputs at 2^64, 2^128 and 2^192, and one above and one below each, and assert that each call returns the exact result, reports the overflow or aborts.
• For P1b, call every function that reads a value as signed with a fee whose top bit is set.
• For P2, call every privileged function that takes a &mut reference to a shared object, from the attacker's address. Check that every permissionless function pays its caller only what the protocol intends.
• For P3, call every function that takes two related objects with objects from two different pools.
• For P4, after an upgrade and a migration on testnet, call each function of the old package on the migrated object, for example with sui client call --dry-run against the old package ID.

Running sui move test --coverage shows which functions none of these tests reached. Formal verification checks a rule for every input that meets its assumptions, including inputs tests do not reach. The Certora Sui Prover takes rules written in Move with Certora's CVLM library: a rule is a Move function whose arguments the Prover chooses, and it reports a counterexample when an assertion can fail on a path that does not abort. A parametric rule checks one property against every function the spec lists as a target (documentation). The eleven rules for P1 to P4 ran as one job, each on a version of its example with the bug or without it, on certora-cli 8.20.3 with basic sanity checks (job). P1 ran on the three versions of checked_shlw. P1b to P4 ran on small models written from the public analyses and the Sui documentation, not on the code Aftermath, Typus or Scallop deployed.

A verified rule covers one property under the assumptions of its job. The verified P3 rule shows that the model with the pool check pairs each account with its own pool, and says nothing about how the model, or Scallop, computes rewards. No rule in this article covers an oracle that reports a wrong price or a key that signs what it should not (how verified code still goes wrong).

What to write down before Certora writes Sui Prover rules

Before Certora writes rules for a Sui package, the team should write down the fact each rule needs:

• For P1, the expected range of every value that is shifted or cast.
• For P1b, every signed value stored in an unsigned integer, and the library that reads it.
• For P2, the capability or address behind each privileged function, and what each permissionless function may pay its caller.
• For P3, the field that ties together the objects each function takes.
• For P4, the version field and migrate function of each shared object, and who holds the UpgradeCap.
• For P5 to P8, the invariants the protocol must keep, with the losses, fees and rounding it accepts.

Ask Certora to turn that list into Prover rules if needed. The team knows what the code is meant to do. Certora's engineers write each item as a Certora Sui Prover rule, run it against every function it applies to, and report a counterexample for each rule the code breaks, as they did for Suilend. Move checks the types, and the rules check what the team wrote down.

Sui Prover documentation and Sui security resources

Certora Sui Prover documentation

Formal verification of Suilend, with the lending and liquid staking reports

Security resources for Sui builders, including free sessions with Certora's Sui team

Frequently asked questions

Does Move prevent integer overflow?

For +, -, * and casts, yes: they abort instead of wrapping. Shifts are the exception: << drops the bits that leave the top, and a u256 shift never aborts.

Can a Sui Move contract be reentered? 

No. Sui Move has no closures or function pointers, so a module never calls code it did not name, and because module dependencies cannot form a cycle, that code cannot call back into it. A PTB can still chain public calls in one transaction, which tests should cover.

What is a hot potato in Sui Move?
A hot potato is a struct with no abilities at all: no copy, drop, store or key. The transaction cannot copy it, discard it or keep it, so it has to consume the value before it ends. Flash loans use this to force repayment. In DeepBook v3, the FlashLoan hot potato carries the pool’s ID, and return_flashloan_base aborts with EIncorrectLoanPool unless the loan goes back to the pool it came from.

Are old package versions still callable after an upgrade on Sui? 

Yes. An upgrade leaves the old package on chain, and a shared object stays reachable from every version unless each function that touches it checks a version field.

How do you formally verify a Sui Move package?
Write each property as a rule in Move with Certora’s CVLM library, run it with the certoraSuiProver command, and read the result: verified, violated with a counterexample, or a timeout, which is inconclusive.. A rule is a Move function whose arguments the Prover chooses, so it covers every input that meets the rule’s assumptions. For example, rule P1 says that if checked_shlw reports no overflow, shifting the result back by 64 bits returns the input. The Prover returns n = 2^192 as the counterexample on Cetus’s first patch and verifies the final version (run). A verified rule covers one property under the assumptions of its job.

What is the Certora Sui Prover? 

A formal verification tool for Sui Move packages, shipped in Certora Prover 8.5.1 in November 2025. Rules are written in Move, and the Prover checks each one for every input that meets its assumptions, with a counterexample when it can fail.