Skip to content

CASE_STUDY.md

Latest commit

 

History

History
168 lines (134 loc) · 8.42 KB

CASE_STUDY.md

File metadata and controls

168 lines (134 loc) · 8.42 KB
Raw

How ReqProof Would Have Prevented the $182M Beanstalk-Style Governance Failure

This demo models the Beanstalk-style governance failure as a specification problem: if the governor can execute treasury-changing calls immediately, a captured vote can drain funds in the same block. The fixed configuration routes execution through OpenZeppelin TimelockController with a non-zero delay.

The point is not that ReqProof replaces Slither, Foundry, OpenZeppelin, or a human smart-contract audit. The point is that a release gate can make the intended governance safety contract explicit, keep it linked to Solidity source and Foundry tests, and fail review when the implementation removes the timelock or same-block defenses.

The repository intentionally contains both sides of the story:

  • UnsafeGovernor demonstrates the failing configuration: the executor is the governor itself and executeImmediately performs a direct low-level call.
  • MyGovernor composes OpenZeppelin Governor extensions with GovernorTimelockControl.
  • MyTimelock pins a two-day delay and exposes role constants for review.
  • Treasury is the protected asset holder.

The requirement set captures the review contract:

  • STK-REQ-001 is the protocol-safety claim.
  • SYS-REQ-001 through SYS-REQ-034 cover proposal lifecycle, snapshot voting, timelock delay, predecessor ordering, role gates, cancelled-operation irreversibility, executor identity, delay floor, voting-window floor, zero-recipient rejection, treasury-drain reentrancy strategy, pinned governance parameters, timelock operation identity, treasury ownership, ETH accounting, token mint/delegation controls, snapshot immutability, and explicit unsafe-governor negative witnesses.
  • INT-REQ-001 covers the cross-contract path: protocol-state mutation must route through TimelockController execution.

The key Foundry tests are:

  • test/BeanstalkScenario.t.sol shows the unsafe governor can drain immediately and the timelock configuration rejects same-block execution.
  • test/Timelock.t.sol checks delay, predecessor, role, and cancellation behavior.
  • test/Governor.t.sol checks executor identity, voting delay, voting period, quorum, and proposal-threshold configuration.
  • test/AssuranceMatrix.t.sol checks the broader review matrix: pinned constants, role-gated scheduling, duplicate operation rejection, operation identity binding, owner-only treasury mutation, atomic drain failure, token mint/delegation behavior, immutable past votes, and unsafe-governor witnesses.

ReqProof uses the case study to dogfood Solidity support:

  • Solidity source and Foundry tests are traced from .sol files.
  • forge test --junit produces test evidence.
  • forge coverage --report lcov produces Solidity line/branch coverage evidence. This is not MC/DC.
  • Slither JSON is normalized into ReqProof code signals when configured.
  • Code-signal obligations force low-level call, address-zero, access-control, and reentrancy risks to be covered by requirements or explicitly suppressed.

Dogfood finding

The first version of this demo was intentionally small. When Slither signals were mapped into ReqProof obligations, the zero-address signal exposed a real gap in the demo Treasury: constructor(address initialOwner) and transferOwnership(address newOwner) accepted address(0). That could lock the Treasury by leaving no valid owner able to authorize future drains or ownership changes.

The fix is now part of the case study:

  • Treasury.InvalidOwner rejects zero-owner construction and transfer.
  • SYS-REQ-032 captures the owner-nonzero obligation.
  • test/AssuranceMatrix.t.sol::testTreasuryRejectsZeroOwner proves the negative path.

This is the intended workflow: scanner signal, requirement, implementation change, negative test, and clean audit gate.

Failure and fix path

The red-team half of BeanstalkScenario.t.sol deploys UnsafeGovernor and a funded Treasury, then calls executeImmediately(...) to drain the treasury in the same block. That test is intentionally present as a failing-design witness: it shows exactly what the requirements must forbid.

The fixed half deploys MyTimelock, schedules the same treasury-drain call, and asserts that same-block execution reverts. Only after the timelock delay elapses can the operation execute. ReqProof then ties the passing configuration to:

  • SYS-REQ-006, the timelock delay requirement;
  • SYS-REQ-010, the executor identity requirement;
  • INT-REQ-001, the Governor-to-Timelock mutation path;
  • STK-REQ-001, the protocol treasury safety claim.

In a production repository, the unsafe-only configuration would leave those requirements without the required implementation/evidence closure and would keep the release gate red until the design is fixed or the risk is explicitly accepted.

Z3-backed governance claims

The Solidity demo also models the Beanstalk-prevention invariants as concrete data-domain predicates, not only as prose:

  • voting_delay_elapsed proves the proposal cannot become active before current_block >= proposal_snapshot_block + voting_delay_blocks.
  • min_delay_elapsed proves timelock execution is gated by current_timestamp >= scheduled_timestamp + min_delay_seconds.
  • predecessor_requirement_satisfied proves execution only proceeds when no predecessor is required or the predecessor is done.
  • required_role_present proves privileged governance/timelock actions require the expected role bit.
  • cancelled_operation_stays_inactive proves a cancelled operation does not transition back to ready/done.
  • snapshot_vote_weight_matches_snapshot proves voting weight is bound to the proposal snapshot block.
  • voting_window_floor_satisfied proves same-block proposal/vote execution is rejected by the configured voting-delay and voting-period floors.

These predicates are intentionally separate from the Solidity compiler: they are the formal contract ReqProof requires the implementation and tests to satisfy. The current dogfood run proves:

  • data_constraint_z3_coverage: 7/7 data constraints checked.
  • data_constraints_complete: 14 data-domain coverage/exclusivity checks proved.
  • behavioral_implications_verified: 7 requirement implications proved.
  • z3_properties_verified: 21 Z3 proof results proved.

That is the difference between "Slither did not report a bug" and "the release gate contains explicit governance invariants that fail when the design removes the timelock or same-block defenses."

Signal-to-evidence matrix

The owned-code signal obligations are closed by specific requirements and tests, not by a blanket suppression:

Signal family Requirement(s) Evidence
address_zero_checked SYS-REQ-013, SYS-REQ-032 testTreasuryRejectsZeroDrainRecipient, testTreasuryRejectsZeroOwner
low_level_call_checked INT-REQ-001, SYS-REQ-028, SYS-REQ-034 BeanstalkScenario.t.sol, testDrainFailureRevertsAtomically, testUnsafeGovernorDirectCallBypassesTimelock
reentrancy_protected SYS-REQ-014 testTreasuryDrainDoesNotLeaveReentrancyGuardLocked
access_control_state_mutation SYS-REQ-008, SYS-REQ-019, SYS-REQ-024, SYS-REQ-025, SYS-REQ-029 Timelock role tests, owner-only Treasury tests, owner-only mint test
eth_value_handled SYS-REQ-026, SYS-REQ-027, SYS-REQ-028 passive receive, full drain, failed drain atomicity

The external OpenZeppelin scan remains documented separately in docs/REAL_CODEBASE_DOGFOOD.md; those findings are third-party review inputs, not owned-code requirements.

Current evidence snapshot

The current dogfood run has:

  • forge build: passing.
  • forge test: 28 tests across 5 Foundry suites passing.
  • proof audit --fail-level warn: 0 errors, 0 warnings.
  • Slither provider refresh: 10 normalized signals stored.
  • Documentation coverage: 36/36 requirements documented.