CVE-2026-32732: Cross-Site Scripting (XSS) in @leanprover/unicode-input-component

The @leanprover/unicode-input-component package provides unicode abbreviation processing for the Lean 4 VS Code extension and related web applications. It allows users to type standard ASCII sequences, such as \alpha, and dynamically converts them into corresponding unicode characters. This functionality improves the developer experience when writing mathematical and formal logic proofs in Lean.

CVE-2026-32732 identifies a Cross-Site Scripting (XSS) vulnerability within this component's text rendering pipeline. The flaw occurs because the component improperly neutralizes script-related HTML tags when updating the input element's Document Object Model (DOM) representation. Specifically, user-supplied text strings are processed and inserted directly into the innerHTML property without adequate sanitization.

This vulnerability is classified as CWE-80, representing a basic XSS condition. Applications utilizing this component for user input, such as the Loogle search bar or the Lean 4 extension interface, inherit this exposure. The defect manifests in versions 0.1.9 and lower of the npm package.

The impact of this vulnerability depends on the context of the hosting application. If the component processes input within a web-based interface, an attacker can execute arbitrary JavaScript in the context of the user's session. The issue was resolved in version 0.2.0 by implementing proper HTML entity encoding before DOM insertion.

The root cause of CVE-2026-32732 lies in the direct concatenation of unescaped user input into HTML strings meant for DOM rendering. The component uses a custom function named replaceAt to manage the conversion of abbreviations and the application of visual highlights, such as underlining active abbreviation targets.

During this text transformation process, the component slices the original input string into segments. These segments are divided based on the location of identified abbreviations. The vulnerable implementation appends these raw, unescaped string slices directly into a new string variable designed to represent the updated HTML content.

Because the string slices bypass any sanitization routines, any HTML tags present in the original user input remain intact. When the application subsequently assigns this newly constructed string to the innerHTML property of the input field element, the browser parses and executes the embedded HTML and JavaScript.

The vulnerability is triggered under the condition that the component processes input containing structural HTML characters, specifically less-than and greater-than signs. The component's failure to distinguish between literal text intended for display and functional HTML markup creates the injection vector.

The vulnerable implementation resides in lean4-unicode-input-component/src/index.ts. The replaceAt function iterates over an array of identified abbreviation updates. Inside the loop, it slices the original string from the last untouched position to the start of the current abbreviation offset.

function replaceAt(str: string, updates: { range: Range; update: (old: string) => string }[]): string {
    // ...
    for (const u of updates) {
        newStr += str.slice(lastUntouchedPos, u.range.offset) // Vulnerable: unescaped slice
        newStr += u.update(str.slice(u.range.offset, u.range.offsetEnd + 1))
        lastUntouchedPos = u.range.offset + u.range.length
    }
    newStr += str.slice(lastUntouchedPos) // Vulnerable: unescaped slice
    return newStr
}

As shown in the vulnerable snippet, the result of str.slice(lastUntouchedPos, u.range.offset) is appended directly to newStr. If str contains a payload such as <img src=x onerror=alert()> before an abbreviation, the raw payload is written into newStr.

The patch introduced in commit 14b7a105c89d2819c5e78970fd258393f76453bb resolves this by adding an escapeHtml utility function. This function performs static string replacements for critical HTML control characters: &, <, >, `

Exploitation of CVE-2026-32732 requires the attacker to supply crafted input to an application utilizing the vulnerable @leanprover/unicode-input-component. The attacker must identify an input vector that feeds directly into the component's text processing and abbreviation resolution logic.

A standard proof-of-concept payload targets the lack of tag sanitization. An attacker can input a string such as <img src=x onerror=alert(document.domain)> \alpha. The inclusion of the \alpha triggers the abbreviation resolution mechanism, invoking the vulnerable replaceAt function.

When the component processes this input, it slices the string containing the img tag and appends it unescaped to the internal HTML representation. The browser then renders the img tag, fails to load the source x, and immediately executes the JavaScript payload defined in the onerror event handler.

This attack does not require authentication or specific network positioning, provided the target input field is publicly accessible. The execution occurs entirely on the client side, running within the security context of the user viewing or interacting with the malicious input.

The impact of CVE-2026-32732 is scoped to the client-side execution environment of the application integrating the vulnerable package. Because it is a Cross-Site Scripting vulnerability, an attacker gains the ability to execute arbitrary JavaScript within the browser session of a victim user.

Successful exploitation allows the attacker to perform actions on behalf of the user. This includes accessing sensitive session tokens, reading data displayed in the application interface, and issuing unauthorized requests to the backend server. The exact severity scales with the privileges and data access granted to the compromised user session.

The reported CVSS 4.0 score of 0.0 appears to be an anomaly or placeholder from the reserving CNA, as the vector CVSS:4.0/AV:N/AC:L/AT:N/PR:N/UI:A/VC:N/VI:N/VA:N/SC:N/SI:N/SA:N indicates no impact across all metrics. A more accurate assessment for unauthenticated, stored or reflected XSS typically yields a medium to high severity score, depending on the operational context.

Despite the low reported CVSS score, the Exploit Prediction Scoring System (EPSS) assigns a probability of 0.00045, placing it in the 13.35th percentile. The vulnerability is currently recognized at the proof-of-concept maturity level, with no active exploitation recorded in CISA's Known Exploited Vulnerabilities (KEV) catalog.

The primary remediation strategy for CVE-2026-32732 is to upgrade the @leanprover/unicode-input-component package to version 0.2.0 or higher. This version contains the official patch implemented in pull request #735, which securely encodes HTML entities during the text rendering process.

Development teams must update their package.json dependencies and regenerate lockfiles to ensure the patched version is pulled during build processes. Applications utilizing the component in production environments should be redeployed with the updated dependency to eliminate the XSS vector.

In environments where an immediate upgrade is impossible, developers can implement a temporary workaround. This involves manually sanitizing all user input before passing it to the unicode input component. A reliable HTML sanitization library, such as DOMPurify, should be used to strip script tags and event handlers from the input.

Alternatively, teams can temporarily replace the unicode input component with a standard HTML <input> or <textarea> element. While this degrades the user experience by removing dynamic abbreviation resolution, it entirely mitigates the vulnerability until the package can be safely updated.