Skip to content

S011.md

Latest commit

 

History

History
80 lines (58 loc) · 2.87 KB

S011.md

File metadata and controls

80 lines (58 loc) · 2.87 KB
Raw

S011 — SMT Invariant Violation

  • Category: formal_verification
  • Severity: High
  • Rule name: smt_invariant_violation

What it detects

S011 is produced by Sanctifier's formal-verification backend. It parses #[invariant = "..."] attributes on contract functions and feeds each invariant to the Z3 SMT solver under a configurable timeout. A finding is emitted for every invariant that the solver cannot prove safe — either it found a concrete counterexample (the invariant can be violated) or it timed out. Invariants proved safe produce no finding.

Why it matters

Unit tests check the cases you thought of; an SMT solver checks all of them within the modeled domain. When Z3 disproves an invariant — say, "total supply always equals the sum of balances" — it has produced a mathematical counterexample showing your contract can reach a state you believed impossible. These are exactly the deep accounting and conservation bugs that hand-review and fuzzing miss, so the severity is High and the counterexample trace is your direct path to the fix.

Vulnerable example

#![no_std]
use soroban_sdk::{contract, contractimpl, Env};

#[contract]
pub struct Bank;

#[contractimpl]
impl Bank {
    // S011: Z3 disproves this — withdraw can drive `balance` below zero,
    // violating the stated invariant.
    #[invariant = "balance >= 0"]
    pub fn withdraw(env: Env, balance: i64, amount: i64) -> i64 {
        balance - amount
    }
}

Safe example

#![no_std]
use soroban_sdk::{contract, contractimpl, Env};

#[contract]
pub struct Bank;

#[contractimpl]
impl Bank {
    // The guard makes the invariant provable: the result is never negative.
    #[invariant = "balance >= 0"]
    pub fn withdraw(env: Env, balance: i64, amount: i64) -> i64 {
        if amount > balance {
            return balance;
        }
        balance - amount
    }
}

CVSS-style risk rating

  • Vector: CVSS:3.1/AV:N/AC:H/PR:N/UI:N/S:U/C:N/I:H/A:H
  • Base score: 7.1
  • Rating: High

A disproved invariant means a reachable state breaks a guarantee the contract relies on; reaching it may need specific inputs (higher complexity), but the impact on integrity and availability of the accounting logic is high.

How to fix

  1. Read the counterexample trace: it shows the exact inputs that violate the invariant.
  2. Add the missing guard or bound (range check, saturating math, precondition) so the violating state is unreachable.
  3. Re-run verification; the finding clears only when Z3 proves the invariant holds.
  4. Strengthen or correct the invariant itself if it was mis-stated.

Related rules

Related rules: S003, S012

References