Author: Abdulwahed Mansour
The Sunna Protocol's security model is built on defense-in-depth. Multiple independent layers of protection ensure that no single vulnerability can compromise the protocol.
Threat: A malicious contract re-enters a Sunna function during execution to manipulate state before the original call completes.
Mitigation:
- All state-changing functions use OpenZeppelin's
ReentrancyGuard. - Checks-Effects-Interactions (CEI) pattern enforced across all contracts.
- External calls are made only after all state updates are finalized.
Threat: An attacker manipulates oracle price feeds to inflate asset valuations, triggering phantom yield extraction.
Mitigation:
OracleValidatorrejects price data older than a configurable staleness threshold.- Round completeness check:
answeredInRound >= roundIdprevents stale round data. - Multi-oracle aggregation where available (Chainlink, Pyth, TWAP).
- Price deviation checks reject updates that exceed reasonable bounds.
- SolvencyGuard re-validates after every oracle update.
Threat: Fees are extracted based on unrealized gains while the protocol carries unrealized losses. This is the Asymmetric Deficit Socialization (ADS) vulnerability discovered by Abdulwahed Mansour across major DeFi protocols ($98.6M+ exposure).
Mitigation:
FeeControllerenforces PY-1:ΔTreasury ≡ 0 IF ΔLoss > 0.TakafulBufferholds fees in escrow until solvency is confirmed.SolvencyGuardblocks any withdrawal that would violate SE-1.reportLoss()function physically cannot mint fees — by construction.
Threat: A malicious governance proposal attempts to disable safety invariants.
Mitigation:
ConstitutionalGuardmakes invariants SE-1 through DFB-1 immutable.- No governance proposal can modify or bypass constitutional checks.
- Time-lock on all proposals allows community review.
- $HELAL governance is bounded: can adjust parameters, cannot touch invariants.
Threat: An attacker uses flash loans to temporarily inflate balances and extract value within a single transaction.
Mitigation:
- Share price calculations use time-weighted averages, not spot values.
- Deposit and withdrawal in the same block are restricted.
- SolvencyGuard validates state before AND after every operation.
Threat: Exploiting integer division rounding to steal fractional amounts over many transactions (dust attacks, off-by-one exploits).
Mitigation:
- All financial calculations use multiply-before-divide ordering.
- Boundary comparisons use
>=(not>) to prevent off-by-one rejections. SunnaMathlibrary provides safe arithmetic operations with explicit rounding.- Fuzz testing with edge-case values (0, 1, type(uint256).max).
Threat: Using outdated oracle prices to execute trades or settlements at advantageous but incorrect prices. Discovered in Moonwell audit by Abdulwahed Mansour.
Mitigation:
OracleValidatorchecksansweredInRound,updatedAt, and price positivity.- Configurable staleness threshold (default: 1 hour).
- Zero and negative prices are rejected immediately.
| Item | Status | Notes |
|---|---|---|
| Six invariants formally specified | Complete | See INVARIANTS.md |
| Unit test suite | Complete | Per-contract coverage |
| Fuzz testing suite (Foundry) | Complete | 256+ runs per function |
| Invariant-based fuzz testing | Complete | SE-1 and PY-1 property tests |
| Static analysis (Slither) | Planned | Pre-audit phase |
| Symbolic execution (Halmos/Certora) | Planned | Pre-audit phase |
| External security audit | Planned | Trail of Bits / Spearbit |
| Bug bounty program | Planned | Post-mainnet via Immunefi |
| Incident response plan | Documented | See below |
- Each invariant has dedicated test cases for normal, edge, and failure scenarios.
- Tests verify that violating transactions revert with the correct custom error.
- Boundary conditions tested: zero values, maximum uint256, exact-equality cases.
- Foundry fuzz tests with randomized inputs for all public functions.
- Invariant-based fuzzing that checks SE-1 through DFB-1 after every action sequence.
- Minimum 256 runs per fuzz test (10,000+ for critical financial paths).
- Special attention to precision loss scenarios (odd numbers, small amounts).
- Multi-contract scenarios simulating real user flows.
- Adversarial scenarios testing all attack vectors listed in the threat model.
- End-to-end Mudaraba lifecycle tests (creation → effort recording → settlement/burn).
- Oracle failure scenarios (stale data, zero price, negative price, round mismatch).
- Symbolic execution of SolvencyGuard and FeeController critical paths.
- Proof that SE-1 and PY-1 hold under all reachable states.
- Property:
reportLoss()can never result in fee share minting. - Property: JHD balance is monotonically non-decreasing per manager.
- Detection: On-chain monitoring for invariant violations via event listeners.
- Assessment: Severity classification (Critical / High / Medium / Low).
- Containment: Emergency pause via ConstitutionalGuard (if applicable).
- Communication: Immediate disclosure to $HELAL governance and affected users.
- Resolution: Deploy fix through Sunna Shield adapter or governance proposal.
- Post-mortem: Public report with root cause analysis and prevention measures.
Last updated: 2026-02-22