From a617bdf02d8e23972c97e1ba221cb3bb2141a2f2 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Fri, 6 Nov 2026 11:43:21 -0600 Subject: [PATCH] Restrict safe mode containers Safe mode containers ran as root with Docker's default capabilities and a writable file system, and could start any number of processes. Run them as an unprivileged user with no capabilities, no way to gain privileges, a read-only file system with an in-memory /tmp, and a limit on processes and threads. The container's user cannot read files that only their owner can read, so make the interpreter input readable by all users and keep it from other users of the host with a private directory. In safe mode, read a Lustre file in this process and send it over stdin instead of mounting it, so that its permissions still don't matter. Co-Authored-By: Claude Opus 5.5 --- .../edu/uiowa/cs/clc/kind2/api/ApiUtil.java | 19 ++++- .../edu/uiowa/cs/clc/kind2/api/Kind2Api.java | 47 ++++++++++--- .../uiowa/cs/clc/kind2/api/SafeModeTest.java | 70 +++++++++++++++++++ 3 files changed, 127 insertions(+), 9 deletions(-) create mode 100644 src/test/java/edu/uiowa/cs/clc/kind2/api/SafeModeTest.java diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/ApiUtil.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/ApiUtil.java index e074184..fc31f63 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/ApiUtil.java +++ b/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. + *

+ * 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); + } } /** diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 2b52f39..5c2e456 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/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 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 getDockerRunCommand(String containerName) { + List getDockerRunCommand(String containerName) { List options = new ArrayList<>(); options.add("docker"); options.add("run"); @@ -815,6 +829,23 @@ private List 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 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 options = getKind2Command(containerName, mounts); @@ -867,7 +894,7 @@ private List 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 *

+ * 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. + *

* Default: false * @param safeMode whether or not to enable safe mode. */ diff --git a/src/test/java/edu/uiowa/cs/clc/kind2/api/SafeModeTest.java b/src/test/java/edu/uiowa/cs/clc/kind2/api/SafeModeTest.java new file mode 100644 index 0000000..27faa9e --- /dev/null +++ b/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 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 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()); + } + } +}