Certora Formal Verification

.github/workflows/certora.yml

@@ -0,0 +1,70 @@
+name: Certora Prover 
+
+on:
+  pull_request:
+    branches:
+      - main
+      - certora
+  workflow_dispatch:
+
+jobs:
+  certora_run:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Install sui
+        run: |
+          curl -sSfL https://raw.githubusercontent.com/Mystenlabs/suiup/main/install.sh | sh
+          export PATH="$HOME/.local/bin:$PATH"
+          suiup install -y sui@1.65.2 
+      - name: Sui version
+        run: |
+          sui -V
+          sui move -V
+      - name: Apply patch
+        run: ./certora/munges/munge.sh
+      - name: Submit Jobs to Certora Prover (Part I)
+        uses: Certora/certora-run-action@v2
+        with:
+          cli-version: "8.10.1"
+          cli-release: beta
+          ecosystem: sui
+          working-directory: certora/spec/
+          configurations: |-
+            confs/supply_control_decreases.conf
+            confs/supply_control_increases_p1.conf
+            confs/supply_control_increases_p2.conf
+            confs/accounting_no_lst_no_sui.conf
+            confs/accounting_total_sui_supply.conf
+            confs/accounting_value_conservation.conf
+            confs/fees.conf
+          job-name: "Verification Part I"
+          certora-key: ${{ secrets.CERTORAKEY }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      - name: Submit Jobs to Certora Prover (Part II)
+        uses: Certora/certora-run-action@v2
+        with:
+          cli-version: "8.10.1"
+          cli-release: beta
+          ecosystem: sui
+          working-directory: certora/spec/
+          configurations: |-
+            confs/no_arbitrage.conf
+            confs/solvency.conf
+            confs/solvency_monotonicity.conf
+            confs/validators_consistency_p1.conf
+            confs/validators_consistency_p2.conf
+            confs/validators_integrity.conf
+          job-name: "Verification Part II"
+          certora-key: ${{ secrets.CERTORAKEY }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

certora/.gitignore

@@ -0,0 +1,7 @@
+# certora
+.certora_internal
+.venv/
+emv-*/
+build/
+Move.lock
+package_summaries

certora/README.md

@@ -0,0 +1,87 @@
+# Certora Formal Verification: Suilend Liquid Staking
+
+This directory contains Certora's formal verification of the Suilend liquid staking protocol, written in Move on Sui.
+
+## Directory Structure
+
+### `spec/`
+
+The primary verification package. Contains all specification files (written in Move using the `cvlm` framework), per-rule configuration files, and package metadata.
+
+- `spec/sources/`:Specification modules. Each `.move` file encodes one or more verifiable properties as rules.
+- `spec/confs/`:Per-rule Certora Prover configuration files (`.conf`), one per property group.
+- `spec/Move.toml`:Package manifest for spec sources. References the `liquid_staking` contract, the `cvlm` (Certora Verification Language for Move) library, Certora Sui framework summaries, and overrides for Sui system packages.
+
+### `munges/`
+
+Code modification scripts and patch files. These make internal functions accessible to the Prover by widening their visibility, and reduce `MAX_VALIDATORS` to make verification tractable.
+
+- `munge.sh`:Applies all patches before running verification.
+- `unmunge.sh`:Reverts all patches.
+- `record_patches.sh`:Regenerates patch files from current working-directory diffs against HEAD.
+- `fees.patch`:Makes `validate_fees()` public.
+- `storage.patch`:Widens visibility of view functions and internal helpers; reduces `MAX_VALIDATORS` from 50 to 5.
+
+> [!NOTE]
+> The patches are applied as git patches and must be kept in sync with the source code. If the patched files change, `munge.sh` will fail to apply and verification will not run. Use `record_patches.sh` to regenerate the patches after updating the source.
+
+### `assumptions/`
+
+A separate package that verifies assumptions made by summaries in the main spec. Currently contains one rule proving that `liquid_staking::storage::get_sui_amount` is equivalent to `sui_system::staking_pool::get_sui_amount`.
+
+- `assumptions/sources/assumptions.move`:Assumption validation rules.
+- `assumptions/Move.toml`:Package manifest.
+- `Assumptions.conf`:Prover configuration for running assumption checks.
+
+## Certora Prover
+
+The Certora Prover is a formal verification tool for smart contracts. It statically proves or disproves properties expressed as rules in the Certora Verification Language for Move.
+
+## Running Instructions
+
+0. Install the latest certora prover by following the [installation guide](https://docs.certora.com/en/latest/docs/user-guide/install.html).
+
+1. From the repository root, apply the munges:
+
+    ```sh
+    sh certora/munges/munge.sh
+    ```
+
+    This only needs to be done once per working copy. **Do not commit the munged files.**
+
+2. Change into the `certora/spec/` directory and run the desired verification job (see table below for all scripts). Example:
+
+    ```sh
+    certoraRun confs/solvency.conf
+    ```
+
+    Note that `certora/spec/` must be the working directory for `certoraRun`, otherwise it will fail to compile.
+
+3. To revert munges:
+
+    ```sh
+    sh certora/munges/unmunge.sh
+    ```
+
+## High-Level Properties
+
+See the doc-comments in each spec file for detailed descriptions of individual rules.
+
+- **Solvency and Exchange Rate Monotonicity** (`solvency.move`, `solvency.conf`, `solvency_monotonicity.conf`): `total_sui_supply >= total_lst_supply` always holds; SUI/LST exchange rate is non-decreasing
+- **Total SUI Supply Accounting** (`accounting_total_sui_supply.move`, `accounting_total_sui_supply.conf`): `total_sui_supply` equals the sum of the liquid SUI pool, active stake (via exchange rate), and inactive stake principal
+- **Token Supply Initialization Invariants** (`accounting_no_lst_no_sui.move`, `accounting_no_lst_no_sui.conf`): zero LST implies zero SUI backing and vice versa
+- **Value Conservation** (`accounting_value_conservation.move`, `accounting_value_conservation.conf`): no value is created or destroyed; on `mint`, deposited SUI equals backing increase plus fees; on `redeem`, SUI decrease equals SUI returned plus fees
+- **Fee Accounting Integrity** (`fees.move`, `fees.conf`): accrued fees never exceed total SUI supply, grow monotonically except during collection, and never fully consume a deposit or redemption
+- **Supply Control Authorization** (`supply_control.move`, `supply_control_decreases.conf`, `supply_control_increases_p1/p2.conf`): only `mint` can increase supplies; only `redeem`/`custom_redeem` can decrease them
+- **No Arbitrage** (`no_arbitrage.move`, `no_arbitrage.conf`): a back-to-back `mint` then `redeem` never yields more SUI than was deposited
+- **Validator Registry Consistency** (`validators_consistency.move`, `validators_consistency_p1/p2.conf`): no duplicate validators, registry never exceeds `MAX_VALIDATORS`, no-stake validators have zero `total_sui_amount`
+- **Validator Registry Integrity** (`validators_integrity.move`, `validators_integrity.conf`): validators added only by authorized operations, removed only by `refresh`, at most one per call; `refresh` leaves no inactive stake or empty validators
+- **Assumption Validation** (`assumptions/sources/assumptions.move`, `Assumptions.conf`): validates assumptions made in summaries
+
+## General Assumptions
+
+- **Loop unrolling.** All specs use `optimistic_loop: true`. `loop_iter` is set to 2 for most validator-list rules and 6 for `validators_upper_bound_step` (one above the munged `MAX_VALIDATORS = 5`).
+- **Validator count reduction.** `storage.patch` reduces `MAX_VALIDATORS` from 50 to 5. Several inductive step rules further restrict to 1 validator for tractability.
+- **`setup_fresh` precondition.** Most inductive steps model a post-`refresh` state: no inactive stake, all validators have active stake with matching pool IDs and up-to-date exchange rates, `total_sui_supply` is correct, and `last_refresh_epoch == ctx.epoch()`. Each assumption is justified by a separately verified rule.
+- **Solvent exchange rates.** `summaries.move` assumes `sui_amount >= pool_token_amount` for all exchange rates, reflecting Sui system-level pool solvency.
+- **`redeem_fungible_staked_sui` summary.** The full proportional split between principal and rewards is simplified to `get_sui_amount(er, value)`. An internal `cvlm_assert` checks this is an underapproximation of the actual withdrawal.

certora/assumptions/Assumptions.conf

@@ -0,0 +1,13 @@
+{
+    "optimistic_loop": true,
+    "prover_args": [
+        "-maxConcurrentTransforms SIMPLIFIED:1,UNROLL:1,DSA:1",
+        "-disabledTransformations HOIST_LOOPS",
+        "-maxMergedBranchSize 1000000",
+        "-maxCommandCount 10000000",
+        "-maxBlockCount 1000000",
+        "-tacDumpsWithInternalFunctions true",
+        "-callTraceVecElemCount 0",
+        "-dumpCodeSizeAnalysis true",
+    ]
+}

certora/assumptions/Move.toml

@@ -0,0 +1,11 @@
+[package]
+name = "assumptions"
+edition = "2024.beta"
+
+[dependencies]
+liquid_staking = { local = "../../contracts" }
+cvlm = { git = "https://github.com/Certora/cvl-move-proto.git", subdir = "cvlm", rev = "main" }
+certora_sui_summaries = { git = "https://github.com/Certora/cvl-move-proto.git", subdir = "certora_sui_summaries",  rev = "main" }
+
+[addresses]
+assumptions = "0x0"

certora/assumptions/sources/assumptions.move

@@ -0,0 +1,32 @@
+module assumptions::assumptions;
+
+/*
+    Here we validate the assumptions we make in the main spec's summaries
+ */
+
+use cvlm::manifest::{rule, function_access};
+use cvlm::asserts::cvlm_assert;
+use sui_system::staking_pool::PoolTokenExchangeRate;
+
+public fun cvlm_manifest() {
+    rule(b"get_sui_amount_equivalence");
+
+    function_access(b"ls_get_sui_amount", @liquid_staking, b"storage", b"get_sui_amount");
+    function_access(b"ss_get_sui_amount", @sui_system, b"staking_pool", b"get_sui_amount");
+}
+
+// private function accessors
+native fun ls_get_sui_amount(exchange_rate: &PoolTokenExchangeRate, token_amount: u64): u64;
+native fun ss_get_sui_amount(exchange_rate: &PoolTokenExchangeRate, token_amount: u64): u64;
+
+// The main suilend spec's summaries assume that liquid_staking::storage::get_sui_amount is equivalent to
+// sui_system::staking_pool::get_sui_amount.  We validate that assumption here.
+public fun get_sui_amount_equivalence(
+    exchange_rate: &PoolTokenExchangeRate,
+    token_amount: u64
+) {
+    let ls_amount = ls_get_sui_amount(exchange_rate, token_amount);
+    let ss_amount = ss_get_sui_amount(exchange_rate, token_amount);
+    cvlm_assert(ls_amount == ss_amount);
+} 
+

certora/munges/fees.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/sources/fees.move b/contracts/sources/fees.move
+index 33df151..caa341c 100644
+--- a/contracts/sources/fees.move
++++ b/contracts/sources/fees.move
+@@ -133,7 +133,7 @@ module liquid_staking::fees {
+     // Note that while it's technically exploitable, we allow lsts to be created with 0 mint/redeem fees.
+     // This is because having a 0 fee LST is useful in certain cases where mint/redemption can only be done by
+     // a single party. It is up to the pool creator to ensure that the fees are set correctly.
+-    fun validate_fees(fees: &FeeConfig) {
++    public fun validate_fees(fees: &FeeConfig) {
+         assert!(fees.sui_mint_fee_bps <= MAX_BPS, EInvalidFeeConfig);
+         assert!(fees.staked_sui_mint_fee_bps <= MAX_BPS, EInvalidFeeConfig);
+         assert!(fees.redeem_fee_bps <= MAX_REDEEM_FEE_BPS, EInvalidFeeConfig);

certora/munges/munge.sh

@@ -0,0 +1,2 @@
+git apply -3 certora/munges/fees.patch 
+git apply -3 certora/munges/storage.patch 

certora/munges/record_patches.sh

@@ -0,0 +1,2 @@
+git diff HEAD:contracts/sources/fees.move  contracts/sources/fees.move  > certora/munges/fees.patch;
+git diff HEAD:contracts/sources/storage.move  contracts/sources/storage.move  > certora/munges/storage.patch;