Add fail-closed reentrancy rely-guarantee gate#2032
Merged
Conversation
Single-function CEI checks (cei_safe, allow_post_interaction_writes) do not prevent cross-function reentrancy: a CEI-clean function that makes an external call leaves transiently-exploitable state live during its callback, exploitable by a reentrant sibling function. This is the Midnight take()/liquidate() callback bug, which previously passed verification. Add a dedicated fail-closed pass, validateReentrancyDisposition, that runs after call well-formedness and separate from the CEI check. Any function that opens a reentrancy window (external call or raw low-level call opcode) and is not view/pure is rejected unless it carries a sound disposition: nonreentrant(<lock>) (runtime guard) or reentrancy_trusted (audited author assertion). CEISafety is demoted: its tags no longer satisfy the gate. reentrancy_trusted is metadata-only (no codegen, no proof obligation), so retrofitted contracts' runtime Yul is byte-identical. Existing smoke contracts that open windows are retrofitted with the appropriate tag. AUDIT.md and TRUST_ASSUMPTIONS.md updated to record the new trust boundary per the synchronization non-negotiable.
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Contributor
| \n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
…ompiler-main-test passes (#2032)
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
…antee gate (#2032) Annotate the unsafeYul raw-call AST fixture (reentrancyTrusted) and the macro-DSL external-call smoke specs (CallWithValueSmoke.execute/executeBytes, MacroExternal.storeEcho) with reentrancy_trusted so CompilationModelFeatureTest compiles under the fail-closed gate. Codegen-preserving: reentrancy_trusted asserts trust without injecting a runtime guard, so emitted Yul and trust reports are unchanged.
…nerators The macro property-test generator (generate_macro_property_tests.py) and the selector verifier (check_selectors.py) matched `function <name> (...)` but not the optional mutability modifiers that sit between `function` and the name (Verity/Macro/Syntax.lean). A function annotated with one of these modifiers — e.g. `function reentrancy_trusted hashLeaves (...)` introduced by this PR — captured the modifier keyword as the name, failed at `(`, and was silently dropped: the externally-dispatchable function got no property test and no selector check, while CI stayed green (an empty test file still compiles). Both regexes now consume any number of leading modifiers (payable/view/pure/no_external_calls/allow_post_interaction_writes/cei_safe/ reentrancy_trusted/nonreentrant(<lock>)) before capturing the identifier. `internal` is deliberately omitted: internal helpers carry no external selector, so leaving them unmatched keeps them correctly excluded. Regenerated artifacts/macro_property_tests via the CI wrapper; 27 suites restored their previously-dropped functions (e.g. the 5 reentrancy_trusted entrypoints of LinkedExternalDynamicArgSmoke). InternalHelperSmoke stays unchanged. Fixes the Bugbot MEDIUM finding.
# Conflicts: # PrintAxioms.lean
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 2bf5b52. Configure here.
…#2032) The nonreentrant(<lock>) transient guard is synthesised only at the external dispatch boundary (attachNonReentrantGuard), so it is absent on the lock-free internal-helper shadow the macro emits for direct intra-contract calls. The shadow's reentrancyTrusted flag is synthesised from the lock (not an author assertion), so a public entry that internalCalls such a function would run the guarded body without the lock, silently bypassing the only reentrancy protection (Bugbot HIGH on this PR). Split ensureSupportsInternalHelperSpec (type-support only) from new ensureCallableAsInternalHelper, which additionally fail-closes any internal call to a function with nonReentrantLock set and reentrancy_trusted unset. reentrancy_trusted remains the sound exemption (caller-agnostic author assertion). Declaration-site rejection of `internal nonreentrant(<lock>)` (#1971) is preserved by leaving the declaration-validation path on the type-only check. Tests: NonreentrantCalledAsInternalHelperRejected (public nonreentrant entry called as helper -> rejected) and NonreentrantTrustedInternalHelperAccepted (same call accepted once callee adds reentrancy_trusted). AUDIT.md and TRUST_ASSUMPTIONS.md document the internal-helper closure.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Single-function CEI checks (
cei_safe,allow_post_interaction_writes) do not prevent cross-function reentrancy. A CEI-clean function that makes an external call leaves transiently-exploitable state live during its callback, which a reentrant sibling function can exploit — this is the Midnighttake()/liquidate()callback bug, and it previously passed verification.This PR adds a dedicated fail-closed pass,
validateReentrancyDisposition(Compiler/CompilationModel/Validation.lean), that runs after call well-formedness and separate from the single-function CEI check:callopcode) and that is notview/pure.nonreentrant(<lock>)(runtime guard) orreentrancy_trusted(audited, author-asserted). CEI tags no longer satisfy the gate —CEISafetyis demoted.reentrancy_trustedis metadata-only (no codegen, no proof obligation), so retrofitted contracts' runtime Yul is byte-identical. Existing smoke contracts that open windows are retrofitted with the appropriate tag.AUDIT.mdandTRUST_ASSUMPTIONS.mdare updated to record the new trust boundary, per the synchronization non-negotiable.Validation
lake build— green (full, incl. proofs)make check— green ("All checks passed")LowLevelTryCatchSmoke, was a genuine catch by the new gate of a contract that only compiles via the CLI--moduleFFI path and slipped the build-time retrofit; fixed by tagging its 3 functions → 3/3)Test plan
lake buildpassesmake checkpassesPropertyReentrancyDispositionDeclared)Note
High Risk
Changes compiler acceptance for every mutating function with external or low-level call windows and introduces an unverified
reentrancy_trustedtrust boundary; mistakes would silently weaken reentrancy policy across the contract corpus.Overview
This PR closes the cross-function reentrancy gap where a CEI-clean function with an external call could still leave mid-update state exploitable by a sibling entrypoint (Midnight
take/liquidateshape). Compilation now runsvalidateReentrancyDispositionafter call well-formedness checks: any non-view/purefunction whose bodystmtOpensReentrancyWindowmust declarenonreentrant(<lock>)or the new metadata-onlyreentrancy_trustedauthor assertion.cei_safe/allow_post_interaction_writesno longer satisfy this gate;CEISafetyis documented as single-function ordering only. Window detection treatsstaticcall-summarised ECMs as non-opening; mutating calls, raw Yul calls, and other external forms still trigger the gate.reentrancy_trustedthreads through the macro intoFunctionSpec.reentrancyTrusted(no codegen). Existing smoke and test specs that open windows are retrofitted with the tag so builds stay green while runtime Yul stays unchanged for those contracts.Macro lowering adds
ensureCallableAsInternalHelper: a lock-onlynonreentrantentry cannot be called as an internal helper (the shadow path drops the transient guard);reentrancy_trustedon the callee is the accepted exemption.SecurityCombos.leanpins rejection/acceptance pairs with#guard_msgs.Additively,
Verity.Core.Invariant/Verity.Core.Reentrancy,Env.reenter, andContracts/ReentrancyRelyGuaranteemachine-check the buggy vs lockedtakestory (+8 proven theorems, proof-only in CI). Audit/trust docs, verification counters, property manifests, and selector/property-test generators are updated for the new modifier and contracts.Reviewed by Cursor Bugbot for commit 3945e77. Bugbot is set up for automated code reviews on this repo. Configure here.