Aragon OSx Execute Authorization
A DAO can start executing a proposal only when the caller has its EXECUTE permission.
Aragon OSx provides contracts for creating and operating DAOs. Its DAO contract inherits a permission manager and protects execute with the EXECUTE permission. Permission-management mutations are protected by ROOT.
This case follows the authorization boundary at Aragon OSx commit daf4fbb06b89ab0a05516bccb70b625a1a38303b. It checks the ordered permission lookup, successful entry into the modeled action boundary, ROOT admission for direct mutations, and the source restrictions on wildcard ROOT and EXECUTE grants.
Why It Matters
DAO.execute is the point where a DAO turns authorization into external actions. If an unauthorized caller crosses that boundary, it may instruct the DAO to call other contracts or transfer assets. If permission mutation can bypass ROOT, an attacker can grant itself the right to reach that boundary later.
The value at risk is the DAO's authority over its treasury and connected contracts. DAO members, token holders, and integrations depend on the permission lookup respecting specific grants, wildcard fallbacks, and conditional denials in the source order. They also depend on wildcard restrictions preventing ROOT or EXECUTE from being granted to every caller or for every target.
How This Was Modeled and Proven
The Lean model follows the pinned DAO.execute permission gate and inherited PermissionManager logic. It checks caller-specific EXECUTE permission first, then the wildcard-caller and wildcard-target entries. On success, it records that the original caller reached the action boundary. Changing permissions means calling grant, grantWithCondition, and revoke. These calls require ROOT permission. The tested ROOT and EXECUTE grant paths also reject attempts to create universal access through a caller or target wildcard.
Lean checks 16 properties across the modeled inputs. One ties successful execute entry to EXECUTE authorization and the boundary record. Six tie successful direct permission changes to ROOT authorization. One shows that a specific conditional denial stops the permission lookup. Eight show that the checked ROOT and EXECUTE grant paths reject a broad caller or target wildcard under their stated conditions. All 16 reference proofs compile with no sorry, admit, or case-specific axioms.
Scope
Model boundary: The result applies to the modeled DAO permission state and original caller.
The execution theorem checks the fixed DAO's EXECUTE gate and records body entry by the original caller. The permission theorems check direct grant, grantWithCondition, and revoke calls for ROOT and EXECUTE, including the restricted wildcard paths.
Permission representation: Separate EXECUTE and ROOT mappings represent the source's Keccak-derived permission hashes. The fixed DAO and ANY_ADDR targets have explicit branches. Boolean boundary inputs carry condition-contract outcomes for the exact call context.
Wildcard checks: Eight theorems cover ROOT and EXECUTE, unconditional and conditional grants, and caller and target wildcard cases. Each begins from established ROOT authorization. A target-wildcard check uses a non-wildcard caller. A caller-wildcard check uses the fixed DAO target. Conditional checks use a non-special condition address supplied as a contract with the expected interface. Inputs that fail condition-address validation revert earlier and need their own result-specific proofs.
Execution boundary: DAO.execute runs its non-reentrancy bookkeeping before the authorization check. That modifier state requires a separate model. After authorization, this theorem records entry into the action boundary. The action-count limit, action loop, external calls, ETH values, allowed-failure map, gas checks, return data, and event each require an execution proof.
Other permission paths: The 16 checks cover direct fixed-DAO and wildcard paths. Bulk permission loops and writes for unrelated target contracts require separate proofs because they add loop ordering and storage effects beyond this slice.
Proof artifacts
- Contract.lean contains the source-shaped authorization and mutation model.
- Specs.lean defines the reader-facing helpers and all 16 properties.
- Proofs.lean contains all reference proofs.
- Case directory contains the compile target and generated-task wiring. The reviewed change is in pull request 153.
| Function | Theorem | Status |
|---|---|---|
| DAO.execute | execute_success_implies_authorized | Proven |
| permission lookup | specific_condition_denial_is_terminal | Proven |
| grant / grantWithCondition / revoke | 6 ROOT admission theorems | Proven |
| ROOT and EXECUTE grants | 8 wildcard rejection theorems | Proven |
Verify it yourself
git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark cd ethereum-verification-benchmark git checkout 3b5c09c9b94b730b7dc0a17fedfa1844d5d17452 lake build Benchmark.Cases.AragonOSx.ExecuteAuthorization.Compile
This target imports the contract model, specifications, and reference proofs at the pinned benchmark revision. A successful build means Lean checked the complete case under the boundaries listed here.
Model Boundaries
Model boundaries explain what the Lean model stands for in the DAO's real execution. Lean takes them as modeled inputs. We trust each boundary only after comparing it with the pinned source and the relevant external contract or interface; that review connects the proof to the deployed system.
condition-contract outcomethe supplied Boolean matches the condition contract's result for the exact call contextTrust basis: review the exact condition-contract call
The model uses the condition result for this exact call. A reviewer should compare it with the external contract's behavior: false and a caught revert both deny permission. This boundary is explicit because it decides whether a conditional permission opens the gate.
conditional-grant validationsuccessful conditional grants pass the address, contract, and interface checksTrust basis: compare the modeled guards with the pinned validation path
The model represents the address, contract, and interface outcomes as Boolean inputs. Reviewers can compare those guards with the DAO's validation path at the pinned revision. Invalid condition inputs revert before a grant can reach the wildcard restriction.
Hypotheses
A hypothesis is a fact a specific theorem starts with. Lean checks every later step from that fact to the conclusion. We trust the result as a precise, conditional promise: if the listed fact holds in the model, the conclusion follows. The exact signatures in Specs.lean and Proofs.lean make each premise reviewable rather than hidden.
successful authorization guardsthe modeled execute or direct permission call returns successLean premise: h : modeledCall.run s = ContractResult.success () s'
This is not an assumption that authorization passed. It is a precise modeled success result. From it, Lean proves that EXECUTE or ROOT authorization passed. An unauthorized call reverts, so it cannot satisfy this premise.
present denying conditionspecificStatus ≠ 0 and specificStatus ≠ 2Lean premises: hNonzero and hNotAllow
These facts identify one exact branch: a caller-specific entry exists but is not ALLOW. From that state, Lean proves that the denying condition stops permission lookup before either wildcard fallback. The narrow scope makes the claim easy to inspect.
exact wildcard-error pathROOT authorization holds; target-wildcard cases also require a non-wildcard callerLean premises in wildcardTargetGrantReverts_spec and wildcardCallerGrantReverts_spec
These facts select the path that reaches
PermissionsForAnyAddressDisallowed. They make the promise testable: without ROOT authorization or with an earlier validation failure, the source can revert for a different reason, which this theorem intentionally does not claim to cover.