fix: (critical) prevent xss in unicode input component (#735)

This PR fixes a prompt injection in the unicode input component, which is also used on several web pages (e.g. Loogle). The issue was originally reported [here](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/weird.20behavior.20in.20loogle.20searchbar/with/578558458).

The technical cause of the issue is as follows:
- The text of the unicode input HTML element is set (e.g. from a query parameter) and escaped properly
- Any of the handlers in the unicode input component triggers, reading the `innerText` of the component, which yields the text of the HTML element (without escapes)
- The unicode input component sets the `innerHtml` of the HTML element (potentially including tags to mark active abbreviations using underlines), thus injecting the non-escaped tags

The fix for this issue is to escape all text before setting it in the `innerHtml` except for the underline tags that are created by the unicode input component itself.

**If you are using the unicode input component on a website, it is strongly recommended to update the unicode input component to 0.2.0 after this PR!**

Author: mhuisi

lean4-unicode-input-component/src/index.ts

@@ -122,16 +122,25 @@ function setTextCursorSelection(searchNode: Node, offset: number) {
     sel.addRange(range)
 }
 
+function escapeHtml(s: string): string {
+    return s
+        .replaceAll('&', '&')
+        .replaceAll('<', '&lt;')
+        .replaceAll('>', '&gt;')
+        .replaceAll('"', '&quot;')
+        .replaceAll("'", '&#039;')
+}
+
 function replaceAt(str: string, updates: { range: Range; update: (old: string) => string }[]): string {
     updates.sort((u1, u2) => u1.range.offset - u2.range.offset)
     let newStr = ''
     let lastUntouchedPos = 0
     for (const u of updates) {
-        newStr += str.slice(lastUntouchedPos, u.range.offset)
+        newStr += escapeHtml(str.slice(lastUntouchedPos, u.range.offset))
         newStr += u.update(str.slice(u.range.offset, u.range.offsetEnd + 1))
         lastUntouchedPos = u.range.offset + u.range.length
     }
-    newStr += str.slice(lastUntouchedPos)
+    newStr += escapeHtml(str.slice(lastUntouchedPos))
     return newStr
 }
 
@@ -220,7 +229,7 @@ export class InputAbbreviationRewriter implements AbbreviationTextSource {
         const queryHtml = this.textInput.innerHTML
         const updates = Array.from(this.rewriter.getTrackedAbbreviations()).map(a => ({
             range: a.range,
-            update: (old: string) => `<u>${old}</u>`,
+            update: (old: string) => `<u>${escapeHtml(old)}</u>`,
         }))
         const newQueryHtml = replaceAt(query, updates)
         if (queryHtml === newQueryHtml) {
@@ -236,7 +245,7 @@ export class InputAbbreviationRewriter implements AbbreviationTextSource {
     async replaceAbbreviations(changes: Change[]): Promise<boolean> {
         const updates: { range: Range; update: (old: string) => string }[] = changes.map(c => ({
             range: c.range,
-            update: _ => c.newText,
+            update: _ => escapeHtml(c.newText),
         }))
         this.setInputHTML(replaceAt(this.getInput(), updates))
         // Unlike in VS Code, directly setting innerHTML does not fire any document-change events,