Skip to content

fix(security): formalize upgrade scope invariants and anti-redirection verification - #389

Draft
s6pa1rta3n-lab wants to merge 1 commit into
Stellar-Analysis:mainfrom
s6pa1rta3n-lab:fix-issue-381
Draft

fix(security): formalize upgrade scope invariants and anti-redirection verification#389
s6pa1rta3n-lab wants to merge 1 commit into
Stellar-Analysis:mainfrom
s6pa1rta3n-lab:fix-issue-381

Conversation

@s6pa1rta3n-lab

Copy link
Copy Markdown

Summary

Resolves #381 by formalizing the mathematical invariants for upgrade target scope validation, auditing all contracts across the privilege graph for capability-granting hooks, and replacing placebo file-existence checks with an executable Soroban host exploit-attempt test harness.

Payout Stipulations & Acceptance Criteria Checklist

  • Formal Invariant Specification: contracts/upgrade/src/scope.rs and docs/contract-privilege-graph.md specify formal invariants governing target scope validation (Governance Root Isolation, Upgrade Orchestrator Non-Self-Modification, Transitive Authority Non-Redirection, Non-Delegation of Governance Authority).
  • Executable Exploit-Attempt Proof: Test deploys a real governed target (StellarInsights), executes a governed upgrade through UpgradeManager, and proves that the upgraded code cannot redirect upgrade authority (UpgradeManagerAlreadySet invariant) or perform unauthorized governance/migration actions.
  • Exhaustive Privilege Graph Audit: Audited all contracts in the system (UpgradeManager, MultisigContract, StellarInsights/V2, TimeLockedTransactions, EscrowContract, TokenSwap, Analytics) for capability-granting hooks and documented hardening/accepted risks.
  • Removal of Placebo Tests: Replaced disk existence assertions in contracts/tests/privilege_escalation_test.rs and contracts/upgrade/tests/privilege_escalation_test.rs with genuine behavioral and invariant verification tests.
  • All Tests Green: All workspace tests and upgrade testutils pass cleanly.

Key Changes

  1. contracts/upgrade/src/scope.rs: Formally specified mathematical invariants covering identity boundaries, transitive authorization immutability, and authority non-delegation.
  2. contracts/upgrade/tests/privilege_escalation_test.rs: Implemented genuine Soroban tests verifying blocked self-upgrades, blocked governance upgrades, threshold enforcement, and exploit-attempt rejections on upgraded targets (anti-redirection verification).
  3. contracts/upgrade/tests/test_support/mod.rs: Added governance_upgrade method to V2Target trait for direct unauthorized upgrade invocation testing.
  4. docs/contract-privilege-graph.md: Updated privilege graph documentation with comprehensive entry point inventory, formal invariant definitions, Mermaid diagram, and exhaustive privilege audit for all system contracts.
  5. contracts/tests/privilege_escalation_test.rs & tests/privilege_escalation_test.rs: Replaced placebo checks with invariant specification assertions.

Payout Routing

  • EVM (Base/Arbitrum/Polygon/ETH): 0xF46C9F6d70C50BF81ef3588AB523a90a594a2F89
  • Stellar: GCL6OXAMLD75BMTINA6EMRUDWK5THQUSHMYNLSNBCJAPZJHNYJTUNIBC

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Upgrade governance scope check only blocks two hardcoded addresses, not transitive privilege escalation

1 participant