lean-0010: Linux release builds linked GMP 6.1.2, which has an exploitable bug
Lean's Linux CI built against GMP 6.1.2, which has an exploitable bug; the fix requires GMP 6.3.0. Not a bug in Lean's own source. Listed among the runtime soundness bugs in the FRO's bug hunt; see also lean-0015.
| Status | fixed |
|---|---|
| Fixed in | v4.33.1 |
| Subsystem | build |
| Guarantee broken | |
| Mechanism | |
| Symptom | — |
| Severity | unsoundness |
| Fools | — |
| Discovery | |
| Features | — |
| References |