[daniel-larraz]

Safe mode containers currently run as root with Docker's default capabilities and a writable file system, and can start any number of processes. This PR adds these docker run flags:

Flag	Effect
--user 65534:65534	Runs as an unprivileged user
--cap-drop ALL	Removes all Linux capabilities
--security-opt no-new-privileges	Blocks privilege gain, for example through setuid programs
--read-only and --tmpfs /tmp	Makes the file system read-only, except for an in-memory /tmp that counts toward --memory
--pids-limit 1024	Limits processes and threads

Breaking change

The Kind 2 executable and solvers must now be readable and executable by all users, for example mode 755. Anything stricter fails at run time. For example, an OpenSMT binary with mode 740 fails with EACCES in create_process.

Changes needed to keep the interpreter working

The new flags stop the container from reading mounted files that only their owner can read, which would break the interpreter in two ways:

• Interpreter input: this temp file is now readable by all users, inside a private (700) temp directory that keeps it from other users of the host.
• Lustre files passed to interpret(URI, ...): in safe mode, the API now reads the file and sends it over stdin, as interpret(String, ...) already does, instead of mounting it. Without this, a mode 600 file returned an empty trace with no error.

Choosing the process limit

The limit also counts threads. On a small test program, SMTInterpol peaked between 427 and 497 because each solver instance is a multi-threaded JVM, and it failed with java exited with code 1 at a limit of 256. The other solvers peaked at about 40. 1024 leaves about twice the observed peak, but larger programs or machines with more CPUs could need more. The limit is a constant for now, so changing it needs a release.

Testing

All of this ran on a local rootful Docker daemon with kind2-safe:latest built from this repo.

• Unit tests: ./gradlew test passes, including a new SafeModeTest.
• API, end to end: these gave the same results as the 0.12.0 release:
  • execute
  • interpret(String, ...)
  • interpret(URI, ...) with mode 644 and 600 files
  • Cancellation, which left no containers behind
• Solvers: with the same flags passed to docker run directly, results matched the unhardened runs for Z3, cvc5, Yices2, MathSAT and SMTInterpol. OpenSMT gave the expected results once its binary was world-readable. Bitwuzla failed the same way in both, because it only supports bit-vector logics and the test program uses integers.
• Options: --ivc, --enable MCS, --testgen, --dump_cex and --compositional gave the same results as unhardened runs on the same test program, with no errors. I didn't inspect the files those options may generate, so a feature that writes outside /tmp could still fail.

Not tested:

• Rootless Docker: the flags are expected to work there, but it's worth checking before release.
• Windows and macOS: Docker Desktop wasn't tested, including the permission handling of the interpreter input.
• Large programs: peak process counts come from a small program only.

Existing issue, not changed here

Interpreter input temp files are never deleted. They now also leave behind their private directory.

🤖 Generated with Claude Code