More secure

doc/benchexec-in-container.md

@@ -19,21 +19,20 @@ Docker, but we strongly recommend to use [Podman](https://podman.io/)
 (compatible with Docker), as it provides "rootless" containers, i.e. its
 containers are started as a regular user without sudo (just like BenchExec
 containers). However, as the setup is largely the same, we provide it for
-either case.
+either case. In case you do want to use Docker, please also consider following
+the (easy to implement) [security recommendations](#securing-docker-execution).
 
-<!--
 If you only require a non-interactive setup, i.e. only run a single BenchExec
 process inside a container, you can avoid most of the complications. See
 [below](#non-interactive-setups) for more details.
--->
 
 ## Executing BenchExec in Docker and Podman
 
 Below follows a step-by-step guide to create a Docker / Podman image with
 BenchExec (assuming cgroups v2, the standard nowadays). Some further background
 and reasoning is provided later. Summarized, the main reason why BenchExec
 needs a "custom" setup for containers is due to how cgroups work in combination
-with containers; we need to "manually" set up a  separate cgroup for BenchExec.
+with containers; we need to "manually" set up a separate cgroup for BenchExec.
 
 While this setup should work on most recent system, we cannot guarantee this,
 since there simply are too many variables. In some cases, you may need to
@@ -57,10 +56,9 @@ for controller in $(cat /sys/fs/cgroup/cgroup.controllers); do
   echo "+$controller" > /sys/fs/cgroup/cgroup.subtree_control
   echo "+$controller" > /sys/fs/cgroup/benchexec/cgroup.subtree_control
 done
-# Give control to the non-root user
-chown -R user: /sys/fs/cgroup
-# ... and switch to that non-root user
-exec su -l -P user -c "$@"
+
+# ... or whatever your init process should be
+exec "$@"
 ```
 and set it executable (`chmod +x init.sh`).
 
@@ -75,31 +73,25 @@ RUN apt-get update && apt-get -y install \
     python3-minimal \
   && rm -rf /var/lib/apt/lists/*
 
-# Copy the created script
-COPY init.sh /init.sh
-
 # TODO Install BenchExec with any method (apt install, pip install, or just copy the .whl)
 # RUN pip install benchexec
 # RUN wget https://github.com/sosy-lab/benchexec/releases/download/<current release>.whl -O /opt/benchexec.whl
-COPY benchexec.whl /opt/benchexec.whl
 # ... or any other method
 
-# Create non-root user
-RUN useradd -ms /bin/bash user
-WORKDIR /home/user
+# Copy the created script
+COPY init.sh /init.sh
 
 # Set init.sh as the entrypoint -- It is important to use brackets here
 ENTRYPOINT [ "/init.sh" ]
 # Set the default process to run
 CMD [ "bash" ]
 ```
 If you already have a Dockerfile, you only need to install BenchExec into it
-and add the last few commands (i.e. copy `init.sh`, potentially create a user,
-and set the entrypoint).
+and add the last few commands (i.e. copy `init.sh` and set the entrypoint).
 
-With this finished, execute `docker build -t <tag> .` or
-`podman build -t <tag> .` in the directory where the Dockerfile is located to
-build the container.
+With this finished, execute `podman build -t <tag> .` (or
+`docker build -t <tag> .` when using Docker) in the directory where the
+Dockerfile is located to build the container.
 
 ### Executing BenchExec in the Container
 
@@ -119,11 +111,11 @@ but then mounting within the container still fails.
 
 > **IMPORTANT**: The `--privileged` argument, gives the Docker container *full
 > root access* to the host, so make sure to include the `--cap-drop=all` flag,
-> use this command toonly with trusted images, and configure your Docker
+> use this command only with trusted images, and configure your Docker
 > container such that everything in it is executed under a different user
-> account, not as root (as shown in the Dockerfile above). BenchExec is not
-> designed to run as root and does not provide any safety guarantees regarding
-> its container under these circumstances.
+> account, not as root (more details [below](#securing-docker-execution)).
+> BenchExec is not designed to run as root and does not provide any safety
+> guarantees regarding its container under these circumstances.
 
 With this, you should be able to execute, for example, `runexec echo`
 inside the Docker container. (In case you opted for the `.whl` install, you
@@ -134,7 +126,30 @@ instead.)
 In case you want to modify this setup, please consider the notes mentioned
 [below](#background-and-technical-details).
 
-<!--
+### Securing Docker Execution
+
+When running under Docker, the user which executes the commands by default has
+`UID` 0, i.e. has the permissions of `root` on the host system. For example, if
+you mount a folder into the container, the processes started in the container
+have *full write access* to these files, no matter what their permissions are.
+As such, a small mistake in, e.g., an evaluation script that deletes temporary
+files, could easily wreak havoc on your system. Using Podman directly mitigates
+this issue, as the Podman container runs with the permissions of the current
+user, not `root`, and thus cannot mess with system files (in particular, the
+"`root`" user in a Podman container is "mapped" to your current user).
+
+To significantly increase security of your Docker execution, add
+```docker
+# Create non-root user and set it as default
+RUN useradd -ms /bin/bash user
+WORKDIR /home/user
+USER user
+```
+at the end of your Dockerfile. Note: This is still worse than using Podman
+(e.g. privilege escalation within the container leads to obtaining root
+permissions on the host) but drastically reduces the chance for accidental
+problems.
+
 ### Non-interactive Setups
 
 In case you intend to only execute one BenchExec process inside the container,
@@ -148,7 +163,6 @@ you can simply execute
 This is mostly useful for executing a large benchmark suite with `benchexec`
 inside a container with the benchmarked tools installed, but processing the
 results separately.
--->
 
 ## Background and Technical Details