Read the docs
TI-2026-25224 Aliases CVE-2026-32732GHSA-6ggm-pwr9-r5h2

XSS in @leanprover/unicode-input-component

Priority LOW 3CWE-80Published · Updated

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

Exploitation None reported CISA SSVC · not in CISA KEV
EPSS 0.00318 24th percentileScored 2026-11-07
Fix Fixed vscode-lean4 (leanprover): 0.2.0@leanprover/unicode-input-component (npm): 0.2.0

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

VendorProductAffected versionsFixed inStatusSource
leanprovervscode-lean4before 0.2.00.2.0Patch availableCNA
—@leanprover/unicode-input-component (npm)before 0.2.00.2.0Patch availableGHSA-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

  1. 2026-10-02 Threatist record created from CVE-2026-32732
  2. 2026-10-03 Alias added: GHSA-6ggm-pwr9-r5h2

References

  • 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