Make IOUtils exec operators opt-in

[NoneSilva]

What

IOUtils provides documented operators IOExec, IOEnvExec, IOExecTemplate, and
IOEnvExecTemplate that run OS commands during model checking. The Java override
tlc2.overrides.IOUtils loads by default, so a specification that EXTENDS IOUtils
runs arbitrary OS commands when TLC checks it, on the machine of whoever runs
the check. TLC gives no notice: inheritIO is off, so the subprocess output is
captured into a record, not shown.

That is fine when you check your own spec. It is a problem when you check a spec
written by someone else, which is the normal way specs are shared: papers,
courses, examples, PR review, CI. Checking such a spec runs its commands
locally. This does not dispute that exec is intended; it is about the default.
The operators stay available, behind a one-line opt-in.

Change

• modules/tlc2/overrides/IOUtils.java: gate the single runProcess(ProcessBuilder)
  that all four exec operators reach on the system property
  tlc2.overrides.IOUtils.enableExec. When it is not "true", throw a TLC error
  before the process starts. The default is off.
• build.xml and tests/IOUtilsUnixTests.tla: opt the test suite in, so ant test
  still exercises the exec operators, including the nested child TLC.
• modules/IOUtils.tla: document the flag.

Verification

ant test stays green, because the suite opts in. To see the gate, build the
branch and model-check any spec that calls IOExec: without the flag TLC stops
with the gate error; with -Dtlc2.overrides.IOUtils.enableExec=true it runs.

A reproducible before and after harness in Docker is at
https://github.com/nonesilva-contributions/communitymodules-ioutils-exec-measurements.

Relates to #137

[lemmy]

Thanks for the PR. We don't plan to merge this change.

TLC's longstanding, albeit unwritten, threat model assumes that it runs in a suitably secured environment and that specs and their dependencies have been vetted by a human. TLA+ specs are typically small, consisting of just one or a few modules, which makes such review practical. This is also why the absence of a package manager has not been a significant limitation.

TLC is not designed to safely execute untrusted specs. For example, Java operator overrides provide another means of executing arbitrary code. Disabling the IOUtils exec operators by default would therefore address only one execution mechanism, without establishing a meaningful security boundary.

The proposed change would break existing specs while providing an incomplete mitigation that risks creating a false sense of security. Users who need to check untrusted specs should run TLC in a sandboxed environment with appropriately restricted privileges.

Closing as wontfix.

[lemmy]

related: tlaplus/tlaplus#1474 (comment)