Quote argv for the Autogenerated header with an allow-list (scrutineer #2511)

[JasonGross]

Fixes scrutineer finding #2511 (CWE-116, severity Low).

The bug

Every generated file starts with an Autogenerated: <command line> header line so that the exact synthesis command can be copied into a shell and re-run. ForExtraction.quote in src/CLI.v decided whether to single-quote each argv element with a deny-list of shell metacharacters, and that list omitted newline, tab, carriage return and every other control character. An argument such as p256<newline>touch<tab>pwned was therefore emitted bare, and pasting the line ran touch pwned as a second command. In the js_of_ocaml web build, argv comes from a crafted ?argv= URL (the README publishes links of exactly that shape), so the header of a generated file could carry an attacker-chosen command.

Reproduced with the currently installed binary:

$ fiat_crypto word-by-word-montgomery $'p256\ntouch\tpwned' 64 '2^256 - 2^224 + 2^192 + 2^96 - 1' add | head -2 | cat -A
/* Autogenerated: '/data/jason/.opam/rocq-dev/bin/fiat_crypto' word-by-word-montgomery p256$
touch^Ipwned 64 '2^256 - 2^224 + 2^192 + 2^96 - 1' add */$
$ sh ./old_invocation.sh; ls pwned
[... usage error from fiat_crypto ...]
pwned

The fix

quote now uses an allow-list, in the style of Python's shlex.quote: a word is left bare only if it is non-empty and every character is an ASCII letter, digit, or one of _-.,:@%+; everything else is wrapped in single quotes with '"'"' for embedded single quotes (the existing, correct escaping). As before, and unlike shlex.quote, / and = are still quoted, so the output for every argument the old quoter handled correctly is unchanged.

Control characters and comment syntax. Single quotes neutralise newline/tab/CR for the shell (a literal newline inside '...' is preserved as data). But a raw newline in the header line is itself a problem: the Go and Zig backends wrap each header line in a // line comment (and PipelineLines passes the header to comment_file_header_block without preprocess_comment_block), so a raw newline inside the single-quoted argument would end the comment and turn the remainder of the argument into source code. I considered three options:

1. Reject argv elements containing control characters. Rejected because it is a user-visible behaviour change for a CLI whose string-valued options (--doc-prepend-header, ...) have no documented restriction, and the point of this finding is the header line, not argument validation.
2. Leave the raw newline inside single quotes, exactly like shlex.quote. Shell-safe, but leaves the comment-breakage in //-comment backends.
3. Escape the control characters in the invocation string. Chosen.

Arguments that contain a control character (byte < 0x20, or 0x7f) are emitted with ANSI-C quoting $'...', escaping newline/tab/CR as \n/\t/\r, backslash as \\, single quote as \047, and any other control character as a three-digit octal escape. The header line therefore never contains a raw control character. $'...' is understood by bash, zsh, ksh and any POSIX.1-2024 shell. In shells that do not understand it (e.g. dash, which is /bin/sh on Debian), the word is still an ordinary single-quoted string preceded by a literal $: the argument value is wrong, but nothing can execute, because no single quote is ever emitted inside that form (\047 is used instead of \', which dash would treat as the end of the quoted string). Such arguments never occur in legitimate use and this form does not appear in any checked-in generated file. The full rationale is in the doc comment above quote.

There is no other copy of the quoting logic: the Haskell and js_of_ocaml builds extract the same Coq PipelineMain, and fiat-html/*.js never touches the invocation.

Verification

• Coq compile (overlay against the installed library): coqc -q -R src Crypto ... src/CLI.v (5.6 s), then src/StandaloneMonadicUtils.v, src/StandaloneOCamlMain.v, src/StandaloneHaskellMain.v, src/StandaloneJsOfOCamlMain.v, src/Bedrock/Standalone/StandaloneOCamlMain.v, src/StandaloneDebuggingExamples.v: all succeed.
• Unit evaluation inside Coq (Eval vm_compute in ForExtraction.quote ...): "p256" → p256; "" → ''; "32,64" → 32,64; "src/ExtractionOCaml/word_by_word_montgomery" → quoted; "2^255 - 19" → quoted; "it's" → 'it'"'"'s'; "a=b" → 'a=b'; "p256\ntouch\tpwned" → $'p256\ntouch\tpwned'; "a'\n; touch pwned; '\\b\r\001\177" → $'a\047\n; touch pwned; \047\\b\r\001\177'.
• No output regression, all 172 checked-in generated files (fiat-c, fiat-rust, fiat-go, fiat-zig, fiat-java, fiat-bedrock2; fiat-json has no header): a Python port of both the old and the new quote (shlex.split each Autogenerated: line into its 4857 argv tokens, re-quote, compare) reproduces every line byte for byte with both implementations. Characters occurring in bare tokens: ,-0123456789A-Za-z_; the 27 distinct quoted tokens are the binary paths, the primes, the empty string, (auto), and the Go doc header.
• Rebuilt binaries via the overlay path: extracted and compiled src/ExtractionOCaml/word_by_word_montgomery and src/ExtractionOCaml/unsaturated_solinas from the new .vo files (coqc extraction ≈ 1 min, ocamlfind ocamlopt ≈ 35 s each).
• Regenerated 14 checked-in files with the rebuilt binaries via make -f Makefile.examples ... WORD_BY_WORD_MONTGOMERY=... UNSATURATED_SOLINAS=...: fiat-c/src/{p256_64,curve25519_64,poly1305_32}.c, fiat-rust/src/{p256_64,curve25519_64}.rs, fiat-go/64/{p256,curve25519}/*.go, fiat-zig/src/{p256_64,curve25519_64,poly1305_32}.zig, fiat-java/src/{FiatP256,FiatCurve25519}.java, fiat-json/src/{p256_64,curve25519_64}.json. git status is clean afterwards: all byte-identical.
• End-to-end injection test with the rebuilt binary. Running it with the curve description p256\ntouch\tpwned yields a single header line

  /* Autogenerated: 'src/ExtractionOCaml/word_by_word_montgomery' $'p256\ntouch\tpwned' 64 '2^256 - 2^224 + 2^192 + 2^96 - 1' add */
  

  sh -n (dash) and bash -n accept it. Executing it in bash, zsh and dash against a stub binary that dumps its argv: bash and zsh pass exactly the original bytes (p 2 5 6 \n t o u c h \t p w n e d), dash passes the inert literal $p256\ntouch\tpwned; no pwned file is created in any shell. Same result for the second payload above (single quotes, ;, backslash, CR, \x01, DEL): bash round-trips every byte, nothing executes.

Not verified / out of scope

• I did not run the full make or the Haskell/js_of_ocaml builds; they extract the same Coq code and no .ml/.hs/.js file contains its own copy of the quoter.
• Only 14 of the 172 generated files were regenerated with the rebuilt binaries; the Python check covers the header line of all 172. CI's regeneration check should confirm the rest.
• Related, not fixed here: the curve description: ... header line (and --doc-prepend-header) still carries the raw curve description, so with a newline in it the Zig/Go comment is still broken on that next line. That is the separate header-assembly sink (S14/S15) and belongs with the src/Stringification comment handling (e.g. running the header through ToString.preprocess_comment_block); I left it out to keep this PR to the shell-quoting finding.

🤖 Generated with Claude Code

https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD