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.
Attack Parameters
Attack Vector
Network
Can be exploited remotely
Attack Complexity
Low
Easy to exploit
Attack Requirements
None
No additional conditions
Privileges Required
None
No privileges needed
User Interaction
Active
User action required
Impact Assessment
Confidentiality
None
No data leak
Integrity
None
No data modification
Availability
None
No disruption
CVSS Vector v4.0
Weakness Type (CWE)
References 3
https://github.com/leanprover/vscode-lean4/pull/735
security-advisories@github.com
https://github.com/leanprover/vscode-lean4/security/advisories/GHSA-6ggm-pwr9-r…
security-advisories@github.com
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/weird.20b…
security-advisories@github.com