fix(security): panic-attack P10 — MEDIUM fixes (HTTPS, mktemp, JSON 400, safe array)

- Upgrade HTTP→HTTPS in LeanTool.res, Page.res, Components.res,
  extract_nusmv.jl, extract_spin.jl, provision_corpora.sh
- balance_smtlib_optimized.sh: replace hardcoded /tmp path with mktemp+trap
- server.jl: wrap JSON3.read in try/catch; return 400 on malformed body
- Daemon.res: Array.getUnsafe(i) → Array.get(i) with option handling

Co-Authored-By: Claude Haiku 4.5 <noreply@anthropic.com>

Author: hyperpolymath

balance_smtlib_optimized.sh

@@ -17,10 +17,12 @@ REPLICA_DIR="$SMTLIB_DIR/replica"
 mkdir -p "$REPLICA_DIR"
 
 # Get a list of all .smt2 files and store in a temporary file
-find "$SMTLIB_DIR" -name "*.smt2" > /tmp/smtlib_files.txt
+SMTLIB_TMPFILE=$(mktemp)
+trap 'rm -f "$SMTLIB_TMPFILE"' EXIT
+find "$SMTLIB_DIR" -name "*.smt2" > "$SMTLIB_TMPFILE"
 
 # Read the list into an array
-mapfile -t FILES < /tmp/smtlib_files.txt
+mapfile -t FILES < "$SMTLIB_TMPFILE"
 
 # Replicate files in batches to avoid timeout
 echo "Starting replication of $FILES_TO_ADD files..."

echidna-playground/src/Components.res

@@ -121,7 +121,7 @@ module TeamSection = {
       url: "",
       affiliations: [
         ("CRI", "https://www.cri.ensmp.fr/"),
-        ("MINES ParisTech", "http://www.mines-paristech.eu"),
+        ("MINES ParisTech", "https://www.minesparis.psl.eu"),
       ],
     },
   ]

echidna-playground/src/Page.res

@@ -61,7 +61,7 @@ let primeExampleSection = (): string => {
       `We don't provide a Coq tutorial (yet), but as a showcase, we `,
       `display a proof of the infinitude of primes in Coq. The proof relies `,
       `in the Mathematical Components library by the `,
-      Html.a(~href="http://ssr.msr-inria.inria.fr/", "MSR/Inria"),
+      Html.a(~href="https://ssr.msr-inria.inria.fr/", "MSR/Inria"),
       ` team led by Georges Gonthier, so our first step will be to load it and `,
       `set a few Coq options:`,
     ]),

scripts/extract_nusmv.jl

@@ -1,7 +1,7 @@
 #!/usr/bin/env julia
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Extract NuSMV / nuXmv model-checker CTL/LTL properties.
-# Vendor: http://nusmv.fbk.eu/distrib/ (examples ship with distribution).
+# Vendor: https://nusmv.fbk.eu/distrib/ (examples ship with distribution).
 using JSON3, Dates
 include("extractor_save_common.jl")
 const DIR = "external_corpora/nusmv"; const OUT = "training_data"; const START_ID = 2_600_000

scripts/extract_spin.jl

@@ -1,7 +1,7 @@
 #!/usr/bin/env julia
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Extract SPIN model-checker LTL properties from Promela models.
-# Vendor: http://spinroot.com/spin/Examples or nimble-code/Spin
+# Vendor: https://spinroot.com/spin/Examples or nimble-code/Spin
 using JSON3, Dates
 include("extractor_save_common.jl")
 const DIR = "external_corpora/spin"; const OUT = "training_data"; const START_ID = 2_000_000

scripts/provision_corpora.sh

@@ -90,7 +90,7 @@ CATALOGUE=(
     "seahorn|git|https://github.com/seahorn/seahorn"
     "spin|git|https://github.com/nimble-code/Spin"
     "prism|git|https://github.com/prismmodelchecker/prism-examples"
-    "nusmv|skip|http://nusmv.fbk.eu/distrib/" # distro ships examples
+    "nusmv|skip|https://nusmv.fbk.eu/distrib/" # distro ships examples
     "uppaal|skip|https://uppaal.org/documentation/" # commercial; examples gated
     "tlaplus_examples|git|https://github.com/tlaplus/Examples"
 

src/julia/api/server.jl

@@ -145,7 +145,11 @@ function handle_predict(req::HTTP.Request)
     state = get_state()
     state.request_count += 1
 
-    body = JSON3.read(String(req.body))
+    body = try
+        JSON3.read(String(req.body))
+    catch e
+        return HTTP.Response(400, JSON3.write(Dict("error" => "Invalid JSON: $(e)")))
+    end
 
     prover = parse_prover(get(body, :prover, "lean"))
     goal_text = get(body, :goal, "")
@@ -212,7 +216,11 @@ function handle_suggest(req::HTTP.Request)
     state = get_state()
     state.request_count += 1
 
-    body = JSON3.read(String(req.body))
+    body = try
+        JSON3.read(String(req.body))
+    catch e
+        return HTTP.Response(400, JSON3.write(Dict("error" => "Invalid JSON: $(e)")))
+    end
     goal_text = get(body, :goal, "")
     prover_str = get(body, :prover, "lean")
     top_k = get(body, :top_k, 5)

src/provers/clients/LeanTool.res

@@ -5,11 +5,11 @@
  * ECHIDNA LeanTool Client
  * Lean 4 theorem proving via OpenAI-compatible API.
  * Uses the LeanTool OpenAI-compatible API server.
- * Demo: http://www.codeproofarena.com:8800/v1
+ * Demo: https://www.codeproofarena.com:8800/v1
  */
 
 /** Default LeanTool API endpoint */
-let leantoolDefaultEndpoint = "http://www.codeproofarena.com:8800/v1"
+let leantoolDefaultEndpoint = "https://www.codeproofarena.com:8800/v1"
 
 /** Lean Playground endpoint for fallback */
 let leanPlaygroundUrl = "https://live.lean-lang.org"

src/provers/runners/Daemon.res

@@ -162,7 +162,10 @@ let emit = async (daemon: t, event: daemonEvent): unit => {
   let handlers = daemon.eventHandlers
   for i in 0 to Array.length(handlers) - 1 {
     try {
-      await (handlers->Array.getUnsafe(i))(event)
+      switch handlers->Array.get(i) {
+      | Some(handler) => await handler(event)
+      | None => ()
+      }
     } catch {
     | exn => consoleError("[Daemon] Event handler error:", exn)
     }