Harden workflow YAML and scanner file handling (#67473)

* Initial plan

* Harden maintenance YAML and scanner file handling

Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>

* Complete descriptor I/O and evidence hardening

Handle partial descriptor reads and writes with shared helpers, reject replaced TLC log artifacts, and bound ledger reads despite concurrent growth. Add focused regression coverage.

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
Co-authored-by: pelikhan <jhalleux@microsoft.com>
Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Peli de Halleux <pelikhan@users.noreply.github.com>

Author: 3 people

.github/scripts/work-queue-formal-check.cjs

@@ -15,6 +15,36 @@ function writeJSON(file, value) {
   fs.writeFileSync(file, `${JSON.stringify(value, null, 2)}\n`);
 }
 
+function readFileDescriptor(fd, expectedPath) {
+  const { size } = fs.fstatSync(fd);
+  const buffer = Buffer.alloc(size);
+  let offset = 0;
+  while (offset < size) {
+    const bytesRead = fs.readSync(fd, buffer, offset, size - offset, offset);
+    if (bytesRead === 0) break;
+    offset += bytesRead;
+  }
+  if (expectedPath !== undefined) {
+    const original = fs.fstatSync(fd);
+    const current = fs.lstatSync(expectedPath);
+    if (!current.isFile() || current.dev !== original.dev || current.ino !== original.ino) {
+      throw new Error("TLC log path no longer identifies the opened evidence file");
+    }
+  }
+  return buffer.subarray(0, offset).toString("utf8");
+}
+
+function writeJSONToFileDescriptor(fd, value) {
+  const buffer = Buffer.from(`${JSON.stringify(value, null, 2)}\n`);
+  fs.ftruncateSync(fd, 0);
+  let offset = 0;
+  while (offset < buffer.length) {
+    const bytesWritten = fs.writeSync(fd, buffer, offset, buffer.length - offset, offset);
+    if (bytesWritten === 0) throw new Error("Unable to make progress writing JSON evidence");
+    offset += bytesWritten;
+  }
+}
+
 function classify(exitCode, signal, timedOut, log) {
   if (timedOut) return "timed_out";
   if (exitCode === 0 && !signal && log.includes("Model checking completed. No error has been found.") && /(?:^|\n)\d+ states generated, \d+ distinct states found, 0 states left on queue\.(?:\r?\n|$)/.test(log)) return "passed";
@@ -162,8 +192,8 @@ async function runVerification(options) {
   fs.writeFileSync(path.join(bundleDir, "java-version.txt"), `${version.stdout || ""}${version.stderr || ""}`);
   const logPath = path.join(bundleDir, "tlc.log");
   const reservePath = path.join(outputDir, "result-space.reserve");
-  fs.writeFileSync(reservePath, Buffer.alloc(1024 * 1024));
-  const fd = fs.openSync(logPath, "w");
+  fs.writeFileSync(reservePath, Buffer.alloc(1024 * 1024), { flag: "wx", mode: 0o600 });
+  const fd = fs.openSync(logPath, "wx+", 0o600);
   let timedOut = false;
   let spawnError = null;
   /** @type {NodeJS.Timeout | undefined} */
@@ -191,14 +221,17 @@ async function runVerification(options) {
   });
   clearTimeout(timer);
   clearTimeout(killTimer);
-  fs.closeSync(fd);
   let log;
   let checkpoints;
   try {
-    log = fs.readFileSync(logPath, "utf8");
+    log = readFileDescriptor(fd, logPath);
     checkpoints = checkpointBundle(stateDir, bundleDir, options.checkpointMaxBytes ?? CHECKPOINT_MAX_BYTES, log.includes("Checkpointing completed"), env);
   } finally {
-    fs.unlinkSync(reservePath);
+    try {
+      fs.closeSync(fd);
+    } finally {
+      fs.unlinkSync(reservePath);
+    }
   }
   const finished = lastMatch(log, /(\d+) states generated, (\d+) distinct states found, (\d+) states left on queue\./g);
   const progress = lastMatch(log, /Progress\((\d+)\).*?: ([\d,]+) states generated.*?, ([\d,]+) distinct states found.*?, ([\d,]+) states left on queue\./g);
@@ -261,12 +294,30 @@ if (require.main === module) {
       console.error(`Formal verification collection failed: ${error.message}`);
       const outputDir = process.env.RESULTS_DIR || "";
       const resultPath = path.join(outputDir, "bundle", "result.json");
-      if (path.isAbsolute(outputDir) && path.resolve(outputDir) !== path.parse(outputDir).root && fs.existsSync(resultPath)) {
-        const result = JSON.parse(fs.readFileSync(resultPath, "utf8"));
-        writeJSON(resultPath, { ...result, status: "tool_error", exhausted: false, error: error.message, finished_at: new Date().toISOString() });
+      if (path.isAbsolute(outputDir) && path.resolve(outputDir) !== path.parse(outputDir).root) {
+        let resultFd;
+        try {
+          resultFd = fs.openSync(resultPath, "r+");
+        } catch (openError) {
+          if (!openError || openError.code !== "ENOENT") throw openError;
+        }
+        if (resultFd !== undefined) {
+          try {
+            const result = JSON.parse(readFileDescriptor(resultFd));
+            writeJSONToFileDescriptor(resultFd, {
+              ...result,
+              status: "tool_error",
+              exhausted: false,
+              error: error.message,
+              finished_at: new Date().toISOString(),
+            });
+          } finally {
+            fs.closeSync(resultFd);
+          }
+        }
       }
       process.exitCode = 1;
     });
 }
 
-module.exports = { TLC_SHA256, classify, inventory, checkpointBundle, runVerification };
+module.exports = { TLC_SHA256, classify, inventory, checkpointBundle, runVerification, readFileDescriptor, writeJSONToFileDescriptor };

.github/scripts/work-queue-formal-check.test.cjs

@@ -7,7 +7,7 @@ const path = require("node:path");
 const crypto = require("node:crypto");
 const { spawnSync } = require("node:child_process");
 const { test } = require("node:test");
-const { TLC_SHA256, classify, checkpointBundle, runVerification } = require("./work-queue-formal-check.cjs");
+const { TLC_SHA256, classify, checkpointBundle, runVerification, readFileDescriptor, writeJSONToFileDescriptor } = require("./work-queue-formal-check.cjs");
 
 const SUCCESS = "Model checking completed. No error has been found.\n42 states generated, 21 distinct states found, 0 states left on queue.\nThe depth of the complete state graph search is 7.\n";
 const INVARIANT_FALSE = "Error: The invariant of DAGValidity is equal to FALSE\n";
@@ -47,6 +47,12 @@ if (mode === "passed") {
 } else if (mode === "violation") {
   console.error("Error: Invariant Safety is violated.");
   process.exit(12);
+} else if (mode === "replace_log") {
+  const config = process.argv[process.argv.indexOf("-config") + 1];
+  const logPath = path.join(path.dirname(config), "tlc.log");
+  fs.unlinkSync(logPath);
+  fs.symlinkSync(process.env.FORMAL_TEST_REPLACEMENT_FILE, logPath);
+  process.stdout.write(${JSON.stringify(SUCCESS)});
 } else if (mode === "invariant_false") {
   process.stderr.write(${JSON.stringify(INVARIANT_FALSE)});
   process.exit(151);
@@ -107,6 +113,48 @@ test("only natural exit plus exhaustion is a pass", () => {
   assert.equal(classify(150, null, false, "Error: Parsing failed."), "tool_error");
 });
 
+test("log collection rejects replaced evidence without modifying the symlink target", async t => {
+  const options = fixture(t);
+  const replacement = path.join(path.dirname(options.javaBin), "replacement.log");
+  fs.writeFileSync(replacement, "replacement content");
+  options.env.FORMAL_TEST_MODE = "replace_log";
+  options.env.FORMAL_TEST_REPLACEMENT_FILE = replacement;
+
+  await assert.rejects(runVerification(options), /TLC log path no longer identifies/);
+
+  assert.equal(fs.readFileSync(replacement, "utf8"), "replacement content");
+  assert.equal(fs.existsSync(path.join(options.outputDir, "bundle", "summary.md")), false);
+  assert.equal(fs.existsSync(path.join(options.outputDir, "result-space.reserve")), false);
+});
+
+test("descriptor reads consume short reads until the snapshotted size or EOF", t => {
+  const options = fixture(t);
+  const fd = fs.openSync(options.jar, "r+");
+  t.after(() => fs.closeSync(fd));
+  const readSync = fs.readSync;
+  t.mock.method(fs, "readSync", (file, buffer, offset, length, position) => readSync(file, buffer, offset, Math.min(length, 3), position));
+  assert.equal(readFileDescriptor(fd), "fixture, not a real TLC jar");
+  let size = 100;
+  t.mock.method(fs, "fstatSync", () => ({ size }));
+  assert.equal(readFileDescriptor(fd), "fixture, not a real TLC jar");
+  size = 0;
+  assert.equal(readFileDescriptor(fd), "");
+});
+
+test("descriptor JSON writes consume short writes and overwrite from position zero", t => {
+  const options = fixture(t);
+  const fd = fs.openSync(options.jar, "r+");
+  t.after(() => fs.closeSync(fd));
+  const writeSync = fs.writeSync;
+  t.mock.method(fs, "writeSync", (file, buffer, offset, length, position) => writeSync(file, buffer, offset, Math.min(length, 3), position));
+  for (const value of [{ status: "running", message: "Unicode \u00e9" }, { status: "passed" }]) {
+    writeJSONToFileDescriptor(fd, value);
+    assert.equal(readFileDescriptor(fd), `${JSON.stringify(value, null, 2)}\n`);
+  }
+  fs.writeSync.mock.mockImplementation(() => 0);
+  assert.throws(() => writeJSONToFileDescriptor(fd, {}), /Unable to make progress/);
+});
+
 for (const { config, moduleName } of CONFIGS) {
   test(`${config}: successful run persists machine-readable evidence and exact sources`, async t => {
     const options = fixture(t, config);

pkg/workflow/maintenance_workflow_generation_fixes_test.go

@@ -56,6 +56,33 @@ func TestMaintenanceWorkflowJobMetadata(t *testing.T) {
 	}
 }
 
+func TestMaintenanceWorkflowQuotesCompileGitHubToken(t *testing.T) {
+	token := "${{ secrets.MAINTENANCE_TOKEN }}: 'quoted' # comment \\\n  injected: true"
+	generated, err := buildMaintenanceWorkflowYAML(context.Background(), buildMaintenanceWorkflowYAMLOptions{
+		cronSchedule: "37 0 * * *", scheduleDesc: "Daily", runsOnValue: "ubuntu-slim",
+		actionMode: ActionModeDev, version: "dev", defaultBranch: "main",
+		compileGitHubToken: token,
+	})
+	require.NoError(t, err)
+
+	var doc struct {
+		Jobs map[string]struct {
+			Steps []struct {
+				Env map[string]string `yaml:"env"`
+			} `yaml:"steps"`
+		} `yaml:"jobs"`
+	}
+	require.NoError(t, yamlv3.Unmarshal([]byte(generated), &doc))
+	var got string
+	for _, step := range doc.Jobs["compile-workflows"].Steps {
+		if value, ok := step.Env["GH_AW_MAINTENANCE_GITHUB_TOKEN"]; ok {
+			got = value
+			break
+		}
+	}
+	require.Equal(t, token, got)
+}
+
 func TestMaintenanceWorkflowDisabledManualJobsAcceptedByConfig(t *testing.T) {
 	for _, job := range []string{
 		"run_operation", "cleanup-cache-memory", "update_pull_request_branches",

pkg/workflow/maintenance_workflow_triggers_test.go

@@ -233,7 +233,7 @@ func TestGenerateMaintenanceWorkflow_PushTrigger(t *testing.T) {
 		if strings.Contains(jobSection, "contents: write") {
 			t.Errorf("compile-workflows should not request contents: write in PR mode, got:\n%s", jobSection)
 		}
-		if !strings.Contains(yaml, "GH_AW_MAINTENANCE_GITHUB_TOKEN: ${{ secrets.MAINTENANCE_TOKEN }}") {
+		if !strings.Contains(yaml, `GH_AW_MAINTENANCE_GITHUB_TOKEN: "${{ secrets.MAINTENANCE_TOKEN }}"`) {
 			t.Errorf("workflow should use configured maintenance github token secret, got:\n%s", yaml)
 		}
 		if !strings.Contains(yaml, "github-token: ${{ env.GH_AW_MAINTENANCE_GITHUB_TOKEN }}") {

pkg/workflow/maintenance_workflow_yaml_jobs.go

@@ -651,9 +651,8 @@ func writeMaintenanceCompileWorkflowsTokenStep(b *strings.Builder, opts buildMai
         uses: ` + getCachedActionPinFromResolver("actions/github-script", opts.resolver) + `
 `)
 	if opts.compileGitHubToken != "" {
-		b.WriteString(`        env:
-          GH_AW_MAINTENANCE_GITHUB_TOKEN: ` + opts.compileGitHubToken + `
-`)
+		b.WriteString("        env:\n")
+		writeYAMLEnv(b, "          ", "GH_AW_MAINTENANCE_GITHUB_TOKEN", opts.compileGitHubToken)
 	}
 	b.WriteString(`        with:
 `)

specs/eslint-factory/trace.mjs

@@ -193,9 +193,14 @@ export function validateTrace(trace, entry) {
 
 export function readableTrace(trace, entry) {
   const lines = [`# ${entry.name}`, "", `Expected TLC diagnostic: \`${entry.expected}\`.`, "", "| State | Transition | Original | Phase | Proposed / applied | Readback | Scan / flag | Quality |", "|---|---|---|---|---|---|---|---|"];
-  for (const { number, action, state: s } of trace)
-    lines.push(
-      `| ${number} | ${action.replace(/\|/g, "\\|")} | ${s.original.join(",") || "none"} | ${s.phase.join(", ")} | ${s.proposed.join(",")} / ${s.applied.join(",")} | ${s.verified.join(",")} | ${s.scan} / ${s.lintClean} | ${s.quality} |`
-    );
+  const escapeCell = value =>
+    String(value)
+      .replaceAll("\\", "\\\\")
+      .replaceAll("|", "\\|")
+      .replace(/\r\n|\n|\r/g, "<br>");
+  for (const { number, action, state: s } of trace) {
+    const cells = [number, action, s.original.join(",") || "none", s.phase.join(", "), `${s.proposed.join(",")} / ${s.applied.join(",")}`, s.verified.join(","), `${s.scan} / ${s.lintClean}`, s.quality];
+    lines.push(`| ${cells.map(escapeCell).join(" | ")} |`);
+  }
   return lines.join("\n") + "\n";
 }

specs/eslint-factory/trace.test.mjs

@@ -0,0 +1,29 @@
+import assert from "node:assert/strict";
+import { test } from "node:test";
+import { readableTrace } from "./trace.mjs";
+
+test("readable traces escape every cell delimiter and line break", () => {
+  const trace = [
+    {
+      number: 1,
+      action: "Transition | one\nsecond line",
+      state: {
+        original: ["item|one"],
+        phase: ["scan"],
+        proposed: ["candidate"],
+        applied: ["candidate"],
+        verified: ["readback"],
+        scan: "clean",
+        lintClean: ["clean"],
+        quality: "good\\value",
+      },
+    },
+  ];
+
+  const output = readableTrace(trace, { name: "fixture", expected: "NeverWitness" });
+
+  assert.match(output, /Transition \\| one<br>second line/);
+  assert.match(output, /item\\\|one/);
+  assert.match(output, /good\\\\value/);
+  assert.equal(output.split("\n").filter(line => line.startsWith("| 1 |")).length, 1);
+});

specs/work-queue/compare-evaluation.mjs

@@ -5,7 +5,7 @@ import fs from "node:fs";
 import path from "node:path";
 import { spawnSync } from "node:child_process";
 import { fileURLToPath } from "node:url";
-import { TLC_SHA256, classify } from "../../.github/scripts/work-queue-formal-check.cjs";
+import { TLC_SHA256, classify, readFileDescriptor, writeJSONToFileDescriptor } from "../../.github/scripts/work-queue-formal-check.cjs";
 
 const root = path.dirname(fileURLToPath(import.meta.url));
 const args = process.argv.slice(2);
@@ -19,7 +19,7 @@ const hash = value => crypto.createHash("sha256").update(value).digest("hex");
 assert.equal(hash(fs.readFileSync(jar)), TLC_SHA256, "unexpected TLC jar checksum");
 assert.notEqual(output, path.parse(output).root, "results must not be the filesystem root");
 fs.mkdirSync(output, { recursive: true });
-assert(!fs.existsSync(path.join(output, "comparison.json")), "do not overwrite previous comparison evidence");
+const comparisonFd = fs.openSync(path.join(output, "comparison.json"), "wx", 0o600);
 const cases = [
   ["WorkQueue", "Recovery"],
   ["FairWorkQueue", "FairBatch"],
@@ -118,10 +118,14 @@ WorkResubmissionNoOp == Original!WorkResubmissionNoOp /\\ Revised!WorkResubmissi
   const command = ["-XX:+UseParallelGC", "-Xmx1g", "-cp", jar, "tlc2.TLC", "-workers", "2", "-seed", "1", "-fp", "0", "-config", "Comparison.cfg", "-metadir", "state", "Comparison.tla"];
   const started = Date.now();
   const logPath = path.join(directory, "tlc.log");
-  const fd = fs.openSync(logPath, "w");
+  const fd = fs.openSync(logPath, "wx+", 0o600);
   const checked = spawnSync(java, command, { cwd: directory, timeout: 900_000, killSignal: "SIGINT", stdio: ["ignore", fd, fd] });
-  fs.closeSync(fd);
-  const log = fs.readFileSync(logPath, "utf8");
+  let log;
+  try {
+    log = readFileDescriptor(fd, logPath);
+  } finally {
+    fs.closeSync(fd);
+  }
   const diagnostic = mutation === "missing-transition" ? "Action property NextEquivalence is violated" : mutation === "changed-normalization" ? "Invariant ReplayEquivalence is violated" : null;
   const expectedExit = mutation === "missing-transition" ? 13 : mutation ? 12 : 0;
   const status = classify(checked.status, checked.signal, checked.error?.code === "ETIMEDOUT", log);
@@ -148,10 +152,8 @@ WorkResubmissionNoOp == Original!WorkResubmissionNoOp /\\ Revised!WorkResubmissi
   };
   comparisons.push(result);
   const complete = comparisons.length === cases.length;
-  fs.writeFileSync(
-    path.join(output, "comparison.json"),
-    `${JSON.stringify({ complete, passed: complete && comparisons.every(c => c.passed), java_version: javaVersion.stderr, runner_sha256: hash(fs.readFileSync(fileURLToPath(import.meta.url))), comparisons }, null, 2)}\n`
-  );
+  writeJSONToFileDescriptor(comparisonFd, { complete, passed: complete && comparisons.every(c => c.passed), java_version: javaVersion.stderr, runner_sha256: hash(fs.readFileSync(fileURLToPath(import.meta.url))), comparisons });
   console.log(`${name}: ${result.passed ? "expected result" : "FAILED"} (${result.elapsed_seconds}s)`);
   assert(result.passed, `comparison failed; inspect ${logPath}`);
 }
+fs.closeSync(comparisonFd);

specs/work-queue/native_probe.cjs

@@ -11,6 +11,27 @@ const scheduler = require("../../actions/setup/js/work_queue_scheduler.cjs");
 const policy = require("../../actions/setup/js/work_queue_policy.cjs");
 const limits = require("../../actions/setup/js/work_queue_limits.cjs");
 
+function readLedgerFile(file) {
+  const maxBytes = 80 * 1024 * 1024;
+  const fd = fs.openSync(file, "r");
+  try {
+    if (fs.fstatSync(fd).size > maxBytes) throw new Error("resource_limit: adapter input exceeds 80 MiB");
+    const chunks = [];
+    let total = 0;
+    while (total <= maxBytes) {
+      const buffer = Buffer.alloc(Math.min(64 * 1024, maxBytes + 1 - total));
+      const bytesRead = fs.readSync(fd, buffer, 0, buffer.length, total);
+      if (bytesRead === 0) break;
+      total += bytesRead;
+      if (total > maxBytes) throw new Error("resource_limit: adapter input exceeds 80 MiB");
+      chunks.push(buffer.subarray(0, bytesRead));
+    }
+    return Buffer.concat(chunks, total).toString("utf8");
+  } finally {
+    fs.closeSync(fd);
+  }
+}
+
 function execute(input) {
   if (input.action === "typed_number_literal") {
     if (typeof input.literal !== "string" || !/^(?:NaN|[+-]Infinity|-?(?:0|[1-9][0-9]*)(?:\.[0-9]+)?(?:[eE][+-]?[0-9]+)?)$/.test(input.literal)) {
@@ -63,8 +84,7 @@ function execute(input) {
   }
   let data = input.data;
   if (input.ledger_file) {
-    if (fs.statSync(input.ledger_file).size > 80 * 1024 * 1024) throw new Error("resource_limit: adapter input exceeds 80 MiB");
-    data = fs.readFileSync(input.ledger_file, "utf8");
+    data = readLedgerFile(input.ledger_file);
   }
   let start = performance.now();
   const commits = queue.parseTransactionLog(data);
@@ -104,11 +124,15 @@ function execute(input) {
   return result;
 }
 
-const lines = readline.createInterface({ input: process.stdin, crlfDelay: Infinity });
-lines.on("line", line => {
-  try {
-    process.stdout.write(`${JSON.stringify(execute(JSON.parse(line)))}\n`);
-  } catch (error) {
-    process.stdout.write(`${JSON.stringify({ error: error.message })}\n`);
-  }
-});
+if (require.main === module) {
+  const lines = readline.createInterface({ input: process.stdin, crlfDelay: Infinity });
+  lines.on("line", line => {
+    try {
+      process.stdout.write(`${JSON.stringify(execute(JSON.parse(line)))}\n`);
+    } catch (error) {
+      process.stdout.write(`${JSON.stringify({ error: error.message })}\n`);
+    }
+  });
+}
+
+module.exports = { readLedgerFile };