XSS in @leanprover/unicode-input-component
Key facts
- Attack vector
- Network
- Privileges required
- None
- User interaction
- Active
- Attack complexity
- Low
- Attack requirements
- None
- Impact type
- Cross-site scripting
- Confidentiality · integrity · availability
- None · None · None
- Fix status
- Fixed
Attack profile from CVSS 4.0 · CNA. Fix status from CNA and GitHub. Impact type from CWE-80.
Summary
Lean 4 VS Code Extension is a Visual Studio Code extension for the Lean 4 proof assistant. Projects that use @leanprover/unicode-input-component are vulnerable to an XSS exploit in 0.1.9 of the package and lower. The component re-inserted text in the input element back into the input element as unescaped HTML. The issue has been resolved in 0.2.0.
Why it matters now
SSVC decision points
CISA ADP · SSVC 2.0.3
- Exploitation
- None
- Automatable
- No
- Technical impact
- Partial
The decision (Track, Attend, Act) also depends on your mission and well-being impact; see CISA's SSVC guide.
Affected products
| Vendor | Product | Affected versions | Fixed in | Status | Source |
|---|---|---|---|---|---|
| leanprover | vscode-lean4 | before 0.2.0 | 0.2.0 | Patch available | CNA |
| — | @leanprover/unicode-input-component (npm) | before 0.2.0 | 0.2.0 | Patch available | GHSA-6ggm-pwr9-r5h2 |
- vscode-lean4 Vendorleanprover Affected before 0.2.0 Fixed in 0.2.0 Patch available CNA
- @leanprover/unicode-input-component (npm) Vendor— Affected before 0.2.0 Fixed in 0.2.0 Patch available GHSA-6ggm-pwr9-r5h2
Remediation
- Fix · CNA vscode-lean4 (leanprover) Fixed in 0.2.0
- Fix · GHSA-6ggm-pwr9-r5h2 @leanprover/unicode-input-component (npm) Fixed in 0.2.0 Advisory →
Timeline
- 2026-10-02 Threatist record created from CVE-2026-32732
- 2026-10-03 Alias added: GHSA-6ggm-pwr9-r5h2
References
Other 4
- https://github.com/leanprover/vscode-lean4/security/advisories/GHSA-6ggm-pwr9-r5h2
- https://github.com/leanprover/vscode-lean4/pull/735
- https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/weird.20behavior.20in.20loogle.20searchbar/near/578502003
- https://github.com/leanprover/vscode-lean4
More leanprover vulnerabilities
- TI-2026-51070 Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections CVSS 4.0MEDIUM 6.8
- TI-2026-50947 Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable CVSS 4.0MEDIUM 6.8
Sources
- CVE-2026-32732 · CVE Program
- CVE-2026-32732 · NVD
- FIRST EPSS
- GHSA-6ggm-pwr9-r5h2 · GitHub Advisory Database · CC BY 4.0
This product uses the NVD API but is not endorsed or certified by the NVD. Sources and licences