lean-0015: Kernel did not bound the size of Nat numerals it computes
The kernel computed Nat numerals of unbounded size. Hardening added after an exploit in the FRO's bug hunt built a multi-gigabyte numeral using the GMP 6.1.2 bug (lean-0010).
| Status | fixed |
|---|---|
| Fixed in | v4.33.1 |
| Subsystem | kernel |
| Guarantee broken | — |
| Mechanism | — |
| Symptom | — |
| Severity | hardening |
| Fools | — |
| Discovery | |
| Features | — |
| References |