fix: block adversarial exploit of non-aborting `assert!` - #8559

Merged

leodemoura merged 2 commits into

May 31, 2025

leodemoura commented May 30, 2025

Member

This PR fixes an adversarial soundness attack described in #8554. The attack exploits the fact that assert! no longer aborts execution, and that users can redirect error messages.
Another PR will implement the same fix for Expr.Data.

leodemoura added 2 commits

May 30, 2025 16:33


          chore: mkData in C

c80fca9


          chore: ensure internal panic is not redirected

00178bc

leodemoura added the changelog-compiler label

leodemoura added this pull request to the merge queue

github-actions Bot added the toolchain-available label

ghost commented May 31, 2025

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ed4252f8c93f591ae753cc963cfd69657ebd3e6a --onto 72141b05fd9a3328c1e5d99211dc4da4495cbd42. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-31 00:11:41)

Merged via the queue into master with commit 6940d2c

leodemoura added a commit that referenced this pull request


          fix: block potential adversarial exploit of non-aborting assert!

ef3b9b3

This PR is similar to #8559, but for `Expr.mkData`

leodemoura mentioned this pull request

fix: block potential adversarial exploit of non-aborting assert! #8560

Merged

github-merge-queue Bot pushed a commit that referenced this pull request


          fix: block potential adversarial exploit of non-aborting assert! (#…

837193b

…8560)

This PR is similar to #8559 but for `Expr.mkData`. This vulnerability
has not been exploited yet, but adversarial users may find a way.

digama0 reviewed

View reviewed changes

src/Lean/Level.lean

-                  let r : UInt64 := h.toUInt32.toUInt64 + hasMVar.toUInt64.shiftLeft 32 + hasParam.toUInt64.shiftLeft 33 + depth.toUInt64.shiftLeft 40
-                  r
+              @[extern "lean_level_mk_data"]
+              opaque Level.mkData (h : UInt64) (depth : Nat := 0) (hasMVar hasParam : Bool := false) : Level.Data

digama0 May 31, 2025

Collaborator

Note that it is still possible to prove that Level.Data is finite here, because it is not opaque type, and moreover Level.Data.depth returns a UInt32. If you are going to use this approach, please at least take the modification to lower the max bvar range to 2^20-2, so that it is at least possible to prove that there exists a sound implementation of the function which is indistinguishable from the real one without hitting a panic.

digama0 May 31, 2025

Collaborator

Or alternatively, make Level.depth and Expr.looseBVarRange opaque, so that it cannot be seen that they are implemented by projecting out of a finite type.

This was referenced Jun 16, 2025

fix: soundness bug in {Expr, Level}.data #8554

Closed

fix: opacify functions using {Expr,Level}.data #8821

Open

kim-em added a commit to kim-em/lean4lean that referenced this pull request


          address review: sharpen the mkData' docstring, share the bit proof

c1641a5

State the trust claim narrowly: `mkData_eq` is a chosen total specification
for the opaque constant, sound for runs that do not abort, not a claim
about what the implementation computes. Record that the `panic!` model was
a copy of the pre-`@[extern]` Lean definition, i.e. of the bug fixed by
leanprover/lean4#8559.

Merge `mkData_hasParam` and `mkData_hasMVar` into a single `mkData_flags`,
matching `Expr.mkData_flags`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y5K6isCtnCB86J8fRbVTKS

kim-em mentioned this pull request

feat: prove Level cached-flag correctness digama0/lean4lean#27

Open

kim-em added a commit to kim-em/lean4lean that referenced this pull request


          doc: correct the lean4 references in the mkData' docstring

ea355d1

leanprover/lean4#8554 is a closed PR, not an issue, and it proposed
saturating; the merged fixes are leanprover/lean4#8559 for `Level` and
leanprover/lean4#8560 for `Expr`, both of which abort. Rest the choice of
total extension on the abort semantics alone.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y5K6isCtnCB86J8fRbVTKS

kim-em added a commit to kim-em/lean4lean that referenced this pull request


          address review: sharpen the mkData' docstring, share the bit proof

2c31d72

State the trust claim narrowly: `mkData_eq` is a chosen total specification
for the opaque constant, sound for runs that do not abort, not a claim
about what the implementation computes. Record that the `panic!` model was
a copy of the pre-`@[extern]` Lean definition, i.e. of the bug fixed by
leanprover/lean4#8559.

Merge `mkData_hasParam` and `mkData_hasMVar` into a single `mkData_flags`,
matching `Expr.mkData_flags`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y5K6isCtnCB86J8fRbVTKS

kim-em added a commit to kim-em/lean4lean that referenced this pull request


          doc: correct the lean4 references in the mkData' docstring

e71fe16

leanprover/lean4#8554 is a closed PR, not an issue, and it proposed
saturating; the merged fixes are leanprover/lean4#8559 for `Level` and
leanprover/lean4#8560 for `Expr`, both of which abort. Rest the choice of
total extension on the abort semantics alone.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y5K6isCtnCB86J8fRbVTKS

kim-em added a commit to kim-em/lean4lean that referenced this pull request


          address review: sharpen the mkData' docstring, share the bit proof

d21392b

State the trust claim narrowly: `mkData_eq` is a chosen total specification
for the opaque constant, sound for runs that do not abort, not a claim
about what the implementation computes. Record that the `panic!` model was
a copy of the pre-`@[extern]` Lean definition, i.e. of the bug fixed by
leanprover/lean4#8559.

Merge `mkData_hasParam` and `mkData_hasMVar` into a single `mkData_flags`,
matching `Expr.mkData_flags`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y5K6isCtnCB86J8fRbVTKS

kim-em added a commit to kim-em/lean4lean that referenced this pull request


          doc: correct the lean4 references in the mkData' docstring

845d843

leanprover/lean4#8554 is a closed PR, not an issue, and it proposed
saturating; the merged fixes are leanprover/lean4#8559 for `Level` and
leanprover/lean4#8560 for `Expr`, both of which abort. Rest the choice of
total extension on the abort semantics alone.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y5K6isCtnCB86J8fRbVTKS

kim-em added a commit to kim-em/lean4lean that referenced this pull request


          address review: sharpen the mkData' docstring, share the bit proof

2cf8529

State the trust claim narrowly: `mkData_eq` is a chosen total specification
for the opaque constant, sound for runs that do not abort, not a claim
about what the implementation computes. Record that the `panic!` model was
a copy of the pre-`@[extern]` Lean definition, i.e. of the bug fixed by
leanprover/lean4#8559.

Merge `mkData_hasParam` and `mkData_hasMVar` into a single `mkData_flags`,
matching `Expr.mkData_flags`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y5K6isCtnCB86J8fRbVTKS

kim-em added a commit to kim-em/lean4lean that referenced this pull request


          doc: correct the lean4 references in the mkData' docstring

98511ad

leanprover/lean4#8554 is a closed PR, not an issue, and it proposed
saturating; the merged fixes are leanprover/lean4#8559 for `Level` and
leanprover/lean4#8560 for `Expr`, both of which abort. Rest the choice of
total extension on the abort semantics alone.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y5K6isCtnCB86J8fRbVTKS

kim-em added a commit to kim-em/lean4lean that referenced this pull request


          address review: sharpen the mkData' docstring, share the bit proof

ed915b1

State the trust claim narrowly: `mkData_eq` is a chosen total specification
for the opaque constant, sound for runs that do not abort, not a claim
about what the implementation computes. Record that the `panic!` model was
a copy of the pre-`@[extern]` Lean definition, i.e. of the bug fixed by
leanprover/lean4#8559.

Merge `mkData_hasParam` and `mkData_hasMVar` into a single `mkData_flags`,
matching `Expr.mkData_flags`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y5K6isCtnCB86J8fRbVTKS

kim-em added a commit to kim-em/lean4lean that referenced this pull request


          doc: correct the lean4 references in the mkData' docstring

ac98e05

leanprover/lean4#8554 is a closed PR, not an issue, and it proposed
saturating; the merged fixes are leanprover/lean4#8559 for `Level` and
leanprover/lean4#8560 for `Expr`, both of which abort. Rest the choice of
total extension on the abort semantics alone.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y5K6isCtnCB86J8fRbVTKS

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

Labels

changelog-compiler toolchain-available