Security: defend against unsafeCast and elaboration-time attacks#19
Merged
GasStationManager merged 4 commits intomainfrom Mar 6, 2026
Merged
Security: defend against unsafeCast and elaboration-time attacks#19GasStationManager merged 4 commits intomainfrom
GasStationManager merged 4 commits intomainfrom
Conversation
added 4 commits
March 6, 2026 19:08
For submission definitions not present in the target, add a Nat literal sanity check: if a stored natVal renders as a negative numeral, reject. This catches unsafeCast/run_elab corruption patterns (e.g. badNat exploit) while still allowing normal helper definitions.
Scan all sub-expressions (not just top-level values) of new declarations for corrupted Nat literals. Catches unsafeCast corruption hidden inside lists, structures, pairs, or any compound type.
Add rebuildLevel to deep-copy Level nodes (zero, succ, max, imax, param, mvar). Update rebuildExpr to rebuild levels in .sort and .const expressions. This catches attacks that use unsafeCast on Level objects to create definitions with undeclared universe parameters (e.g., the magic/isProp attack that proves False via universe-polymorphism inconsistency). The kernel rejects the rebuilt expressions because free level params become visible after breaking compacted-region references.
…recursors Scan types of inductInfo, ctorInfo, and recInfo for corrupted Nat literals, not just defnInfo/thmInfo/opaqueInfo.
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.
Follow-up security hardening after #18 (merged).
Attacks defended against
1. Import superset check (commit bea2fbd)
Submissions must import at least everything the target imports. Prevents redefining types by omitting imports (e.g.
def FermatLastTheorem := True).2. Nat literal validation (commits 73196d3, f06ecb5)
Recursively scans all sub-expressions of new declarations for corrupted Nat literals (stored natVal renders as negative). Catches
unsafeCast+run_elabpatterns that launder corrupted values through compile-time evaluation.3. Level object rebuild (commit 5cafc55)
Deep-copies all
Levelnodes (.sort,.constlevel lists) before kernel replay. CatchesunsafeCastonLevelobjects that create definitions with undeclared universe parameters (e.g. themagic/isPropattack provingFalsevia universe inconsistency).Test results (11 cases)