Merge pull request #3 from freedomofpress/hpc

build: add container, scripts, and documentation for verifying and constructing proofs on an HPC cluster

Author: felixlinker

Makefile

@@ -10,11 +10,14 @@ well-formed:
 interactive:
 	@$(TAMARIN_RELEASE) +RTS -N$(N_THREADS) -RTS interactive --image-format=SVG --derivcheck-timeout=0 --port=$(PORT) "./"
 
+# Keep make from deleting a freshly constructed proof as an intermediate file.
+.SECONDARY:
+
 proof/%.spthy: securedrop.spthy oracle.py parts/*.spthy
 	mkdir -p proof
 	@$(TAMARIN_RELEASE) +RTS -N$(N_THREADS) -RTS --derivcheck-timeout=0 --prove="$**" --output="$@" "securedrop.spthy"
 
-proof/%.log: proof/*.spthy
+proof/%.log: proof/%.spthy
 	@$(TAMARIN_RELEASE) +RTS -N$(N_THREADS) -RTS --derivcheck-timeout=0 "proof/$*.spthy" > "proof/$*.log" 2>&1
 
 debug/%.spthy: securedrop.spthy oracle.py parts/*.spthy

README.md

@@ -16,6 +16,13 @@ Add `tamarin-prover` to your `PATH`, or provide its path to `make` using the `TA
 
 If you want to explore the model in interactive mode or construct proofs, you must also install [python 3](https://www.python.org/downloads/).
 
+A containerized environment is also available, for example via Docker:
+
+```bash
+docker build --tag tamarin hpc
+docker run --rm --volume "$PWD:/workspace" tamarin --version
+```
+
 ## Repository Structure
 
 | File | Description |
@@ -56,3 +63,29 @@ Tamarin traverses proofs using depth-first search and thus typically only needs
 | B | `proof/Easy_.spthy` | 03:37:03 | 01:46:27 | 04:39:35 | 30 GB |
 | B | `proof/Executability.spthy` | 01:55:26 | 00:37:20 | 01:27:26 | 30 GB |
 | B | `proof/Secrecy_.spthy` | 01:49:26 | 00:28:22 | 01:06:19 | 30 GB |
+
+### Running on HPC
+
+If you have access to an HPC cluster, you can construct and verify proofs inside
+an Apptainer container.  For example, from the root of this repository, via
+Slurm:
+
+1. Build the container:
+    ```bash
+    apptainer build --fakeroot tamarin.sif hpc/tamarin.def
+    ```
+
+2. Run the well-formedness checks:
+    ```bash
+    salloc --nodes 1 --ntasks 1 --mem=10G --time=1:00:00 apptainer exec tamarin.sif bash -c 'ulimit -Sn $(ulimit -Hn); make well-formed'
+    ```
+
+3. Verify a proof:
+    ```bash
+    salloc --nodes=1 --ntasks=1 --cpus-per-task=10 --mem=192G --time=12:00:00 apptainer exec tamarin.sif bash -c 'ulimit -Sn $(ulimit -Hn); make proof/Auto_.log'
+    ```
+
+You can also run batch jobs to:
+
+- Verify all proofs: `sbatch hpc/verify.sbatch`
+- Reconstruct all proofs: `sbatch hpc/prove.sbatch`

hpc/Dockerfile

@@ -0,0 +1,16 @@
+FROM --platform=linux/amd64 debian:trixie-slim
+ARG MAUDE_VERSION
+ARG TAMARIN_VERSION
+
+COPY setup.sh /tmp/setup.sh
+RUN sh /tmp/setup.sh && rm -f /tmp/setup.sh
+
+ENV MAUDE_LIB=/opt/maude \
+    LC_ALL=C.UTF-8 \
+    LANG=C.UTF-8
+
+RUN tamarin-prover test
+
+WORKDIR /workspace
+ENTRYPOINT ["tamarin-prover"]
+CMD ["--help"]

hpc/prove.sbatch

@@ -0,0 +1,27 @@
+#!/bin/bash
+#SBATCH --job-name=prove-securedrop-protocol-models
+#SBATCH --array=0-4
+#SBATCH --nodes=1
+#SBATCH --ntasks=1
+#SBATCH --cpus-per-task=10
+#SBATCH --mem=512G
+#SBATCH --time=24:00:00
+#SBATCH --requeue
+#SBATCH --output=slurm-%x-%A_%a.out
+
+set -euo pipefail
+
+# Path to the Apptainer image (override with: sbatch --export=SIF=$HOME/tamarin.sif ...)
+SIF="${SIF:-tamarin.sif}"
+
+PREFIXES=(Agreement_ Auto_ Easy_ Executability Secrecy_)
+PREFIX="${PREFIXES[$SLURM_ARRAY_TASK_ID]}"
+
+cd "$SLURM_SUBMIT_DIR"
+
+echo "Constructing proof/${PREFIX}.spthy on $(hostname) with ${SLURM_CPUS_PER_TASK} threads"
+
+apptainer exec "$SIF" bash -c \
+    "ulimit -Sn \$(ulimit -Hn); make N_THREADS=${SLURM_CPUS_PER_TASK} \
+    -B \
+    proof/${PREFIX}.spthy"

hpc/setup.sh

@@ -0,0 +1,42 @@
+#!/bin/sh
+set -eux
+
+MAUDE_VERSION="${MAUDE_VERSION:-3.5}"
+TAMARIN_VERSION="${TAMARIN_VERSION:-1.12.0}"
+
+export DEBIAN_FRONTEND=noninteractive
+
+# Runtime dependencies:
+apt-get update
+apt-get install --no-install-recommends --yes \
+    ca-certificates \
+    curl \
+    graphviz \
+    make \
+    libffi8 \
+    libgmp10 \
+    libstdc++6 \
+    libtinfo6 \
+    python3 \
+    unzip \
+    zlib1g
+rm -rf /var/lib/apt/lists/*
+
+# Maude:
+curl -fsSL -o /tmp/maude.zip \
+    "https://github.com/maude-lang/Maude/releases/download/Maude${MAUDE_VERSION}/Maude-${MAUDE_VERSION}-linux-x86_64.zip"
+mkdir -p /opt/maude
+unzip -j -o /tmp/maude.zip -d /opt/maude
+rm -f /tmp/maude.zip
+chmod 0755 /opt/maude/maude
+ln -sf /opt/maude/maude /usr/local/bin/maude
+
+# Tamarin:
+curl -fsSL -o /tmp/tamarin.tar.gz \
+    "https://github.com/tamarin-prover/tamarin-prover/releases/download/${TAMARIN_VERSION}/tamarin-prover-${TAMARIN_VERSION}-linux64-ubuntu.tar.gz"
+mkdir -p /tmp/tamarin
+tar -xzf /tmp/tamarin.tar.gz -C /tmp/tamarin
+install -m 0755 \
+    "$(find /tmp/tamarin -type f -name tamarin-prover | head -n1)" \
+    /usr/local/bin/tamarin-prover
+rm -rf /tmp/tamarin /tmp/tamarin.tar.gz

hpc/tamarin.def

@@ -0,0 +1,25 @@
+Bootstrap: docker
+From: debian:trixie-slim
+
+%files
+    hpc/setup.sh /tmp/setup.sh
+
+%post
+    sh /tmp/setup.sh
+    rm -f /tmp/setup.sh
+
+%environment
+    export MAUDE_LIB=/opt/maude
+    export LC_ALL=C.UTF-8
+    export LANG=C.UTF-8
+
+%test
+    tamarin-prover test
+
+%runscript
+    exec tamarin-prover "$@"
+
+%help
+    Run Tamarin directly: apptainer run tamarin.sif --help
+
+    Open a shell: apptainer shell tamarin.sif

hpc/verify.sbatch

@@ -0,0 +1,27 @@
+#!/bin/bash
+#SBATCH --job-name=verify-securedrop-protocol-models
+#SBATCH --array=0-4
+#SBATCH --nodes=1
+#SBATCH --ntasks=1
+#SBATCH --cpus-per-task=10
+#SBATCH --mem=192G
+#SBATCH --time=12:00:00
+#SBATCH --requeue
+#SBATCH --output=slurm-%x-%A_%a.out
+
+set -euo pipefail
+
+# Path to the Apptainer image (override with: sbatch --export=SIF=$HOME/tamarin.sif ...)
+SIF="${SIF:-tamarin.sif}"
+
+PREFIXES=(Agreement_ Auto_ Easy_ Executability Secrecy_)
+PREFIX="${PREFIXES[$SLURM_ARRAY_TASK_ID]}"
+
+cd "$SLURM_SUBMIT_DIR"
+
+echo "Verifying proof/${PREFIX}.log on $(hostname) with ${SLURM_CPUS_PER_TASK} threads"
+
+apptainer exec "$SIF" bash -c \
+    "ulimit -Sn \$(ulimit -Hn); make N_THREADS=${SLURM_CPUS_PER_TASK} \
+    -W proof/${PREFIX}.spthy \
+    proof/${PREFIX}.log"