Restrict safe mode containers

src/main/java/edu/uiowa/cs/clc/kind2/api/ApiUtil.java

@@ -14,6 +14,7 @@
 import java.io.IOException;
 import java.io.InputStream;
 import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
 import java.util.List;
 
 import edu.uiowa.cs.clc.kind2.Kind2Exception;
@@ -38,12 +39,28 @@ public static File writeLustreFile(String program) {
 
   /**
    * Writes an interpreter input to a temporary file for Kind 2 to read.
+   * <p>
+   * In safe mode, this file is mounted into a container that runs as another user, so all users
+   * can read the file. Its directory, which only the current user can enter, keeps the file from
+   * other users of the host.
    *
    * @param program the interpreter input text
    * @return the file the input was written to
    */
   public static File writeInterpreterFile(String program) {
-    return writeTempFile("kind2-api-", ".json", program);
+    File file = null;
+    try {
+      File directory = Files.createTempDirectory("kind2-api-").toFile();
+      file = new File(directory, "interpreter-input.json");
+      file.createNewFile();
+      if (program != null) {
+        Util.writeToFile(program, file);
+      }
+      file.setReadable(true, false);
+      return file;
+    } catch (IOException e) {
+      throw new Kind2Exception("Cannot write to file: " + file, e);
+    }
   }
 
   /**

src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java

@@ -13,6 +13,7 @@
 import java.io.InputStreamReader;
 import java.net.URI;
 import java.net.URISyntaxException;
+import java.nio.file.Files;
 import java.nio.file.InvalidPathException;
 import java.nio.file.Path;
 import java.nio.file.Paths;
@@ -46,6 +47,11 @@ public class Kind2Api {
   private static final String DEFAULT_SAFE_MODE_MEMORY_USAGE = "2g";
   private static final String DEFAULT_SAFE_MODE_SWAP_USAGE = DEFAULT_SAFE_MODE_MEMORY_USAGE;
   private static final int DEFAULT_SAFE_MODE_MAX_RUNS = 2;
+  // Counts threads as well as processes. SMTInterpol starts a multi-threaded JVM per solver
+  // instance, and reached about 500 on a small program, while the other solvers stay near 40.
+  private static final int SAFE_MODE_PIDS_LIMIT = 1024;
+  // An unprivileged user that exists in the image's base system.
+  private static final String SAFE_MODE_USER = "65534:65534";
   private static final long DOCKER_COMMAND_TIMEOUT_SECONDS = 10;
   private static final long DOCKER_EXIT_GRACE_MILLIS = 2000;
   // Calls that cannot be cancelled (the interpreter, and execute without a monitor) give up
@@ -343,6 +349,15 @@ public String interpret(String program, String main, String json) {
    */
   private String runInterpreter(File interpreterFile, Path lustreFile, String program, String main) {
     String containerName = newContainerName();
+    if (containerName != null && lustreFile != null) {
+      // The container's user may not be able to read the file, but this process can.
+      try {
+        program = new String(Files.readAllBytes(lustreFile), java.nio.charset.StandardCharsets.UTF_8);
+        lustreFile = null;
+      } catch (IOException e) {
+        throw new Kind2Exception("Cannot read Lustre file: " + lustreFile, e);
+      }
+    }
     List<String> options = getInterpreterCommand(interpreterFile, lustreFile, containerName);
 
     options.add("--lus_main");
@@ -541,7 +556,6 @@ private void callKind2(String program, Result result, IProgressMonitor monitor,
   private static final String DOCKER_YICES2_BIN = "/usr/local/bin/yices-smt2";
   private static final String DOCKER_Z3_BIN = "/usr/local/bin/z3";
   private static final String DOCKER_INTERPRETER_INPUT = "/tmp/interpreter-input.json";
-  private static final String DOCKER_LUSTRE_FILE = "/tmp/program.lus";
 
   public void setDockerImage(String dockerImage) {
     this.dockerImage = dockerImage;
@@ -785,9 +799,9 @@ private void dockerCommand(String... args) {
 
   /**
    * Returns the docker run command, up to but not including the image name, with the resource
-   * limits and the Kind 2 and solver mounts that every safe mode execution uses.
+   * limits, the restrictions and the Kind 2 and solver mounts that every safe mode execution uses.
    */
-  private List<String> getDockerRunCommand(String containerName) {
+  List<String> getDockerRunCommand(String containerName) {
     List<String> options = new ArrayList<>();
     options.add("docker");
     options.add("run");
@@ -815,6 +829,23 @@ private List<String> getDockerRunCommand(String containerName) {
     options.add("--network");
     options.add("none");
 
+    options.add("--pids-limit");
+    options.add(String.valueOf(SAFE_MODE_PIDS_LIMIT));
+
+    options.add("--cap-drop");
+    options.add("ALL");
+
+    options.add("--security-opt");
+    options.add("no-new-privileges");
+
+    options.add("--user");
+    options.add(SAFE_MODE_USER);
+
+    // Kind 2 and the solvers can only write to /tmp, which is in memory and counts toward --memory.
+    options.add("--read-only");
+    options.add("--tmpfs");
+    options.add("/tmp");
+
     mountIfPresent(options, "KIND2", KIND2, DOCKER_KIND2);
     mountSolversToDocker(options);
     return options;
@@ -854,10 +885,6 @@ private List<String> getInterpreterCommand(File interpreterFile, Path lustreFile
     if (inDocker) {
       mounts.add("--mount");
       mounts.add(bindMountSpec(interpreterFile.toPath(), DOCKER_INTERPRETER_INPUT));
-      if (lustreFile != null) {
-        mounts.add("--mount");
-        mounts.add(bindMountSpec(lustreFile.toAbsolutePath(), DOCKER_LUSTRE_FILE));
-      }
     }
 
     List<String> options = getKind2Command(containerName, mounts);
@@ -867,7 +894,7 @@ private List<String> getInterpreterCommand(File interpreterFile, Path lustreFile
     options.add(inDocker ? DOCKER_INTERPRETER_INPUT : interpreterFile.getAbsolutePath());
 
     if (lustreFile != null) {
-      options.add(inDocker ? DOCKER_LUSTRE_FILE : lustreFile.toString());
+      options.add(lustreFile.toString());
     }
 
     return options;
@@ -1351,6 +1378,10 @@ synchronized void setLimit(int newLimit) {
    * In safe mode, the location of the Kind 2 executable and solvers will not be searched 
    * for on the PATH variable: they must be set via the API
    * <p>
+   * Containers run as an unprivileged user with no capabilities and a read-only file system, so
+   * the Kind 2 executable and the solvers must be readable by all users, and executables must be
+   * executable by all users.
+   * <p>
    * Default: false
    * @param safeMode whether or not to enable safe mode.
    */

src/test/java/edu/uiowa/cs/clc/kind2/api/SafeModeTest.java

@@ -0,0 +1,70 @@
+/*
+ * Copyright (c) 2026, Board of Trustees of the University of Iowa
+ * All rights reserved.
+ *
+ * Licensed under the BSD 3-Clause License. See LICENSE in the project root for license information.
+ */
+
+package edu.uiowa.cs.clc.kind2.api;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+import static org.junit.jupiter.api.Assumptions.assumeTrue;
+
+import java.io.File;
+import java.io.IOException;
+import java.nio.file.FileSystems;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.attribute.PosixFilePermission;
+import java.nio.file.attribute.PosixFilePermissions;
+import java.util.Collections;
+import java.util.List;
+
+import org.junit.jupiter.api.Test;
+
+class SafeModeTest {
+  private static void assertHasOption(List<String> command, String option, String value) {
+    int index = command.indexOf(option);
+    assertTrue(index >= 0, option + " is missing from " + command);
+    assertEquals(value, command.get(index + 1));
+  }
+
+  @Test
+  void dockerRunCommandRestrictsContainer() throws IOException {
+    Path kind2 = Files.createTempFile("kind2", null);
+    String originalKind2 = Kind2Api.KIND2;
+    try {
+      Kind2Api.KIND2 = kind2.toAbsolutePath().toString();
+      List<String> command = new Kind2Api().getDockerRunCommand("name");
+
+      assertHasOption(command, "--network", "none");
+      assertHasOption(command, "--pids-limit", "1024");
+      assertHasOption(command, "--cap-drop", "ALL");
+      assertHasOption(command, "--security-opt", "no-new-privileges");
+      assertHasOption(command, "--user", "65534:65534");
+      assertHasOption(command, "--tmpfs", "/tmp");
+      assertTrue(command.contains("--read-only"));
+    } finally {
+      Kind2Api.KIND2 = originalKind2;
+      Files.delete(kind2);
+    }
+  }
+
+  @Test
+  void interpreterFileIsReadableOnlyThroughAMount() throws IOException {
+    assumeTrue(FileSystems.getDefault().supportedFileAttributeViews().contains("posix"));
+
+    File file = ApiUtil.writeInterpreterFile("[]");
+    try {
+      assertEquals(Collections.singletonList("[]"), Files.readAllLines(file.toPath()));
+      assertTrue(Files.getPosixFilePermissions(file.toPath())
+          .contains(PosixFilePermission.OTHERS_READ));
+      assertEquals("rwx------", PosixFilePermissions
+          .toString(Files.getPosixFilePermissions(file.getParentFile().toPath())));
+    } finally {
+      Files.delete(file.toPath());
+      Files.delete(file.getParentFile().toPath());
+    }
+  }
+}