arcvix-logic-driven-container-security.tex

% SPDX-License-Identifier: MPL-2.0
% arcvix-logic-driven-container-security.tex
%
% Academic paper describing Stapeln's approach to deterministic container
% security via miniKanren logic programming. Systems/HCI crossover.
%
% Author: Jonathan D.A. Jewell
% Date: 2026-03-21

\documentclass[11pt,twocolumn]{article}

%% ---- Packages ----
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage{graphicx}
\usepackage{booktabs}
\usepackage{hyperref}
\usepackage{xcolor}
\usepackage{listings}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{natbib}
\usepackage{balance}
\usepackage{microtype}
\usepackage{url}
\usepackage{enumitem}
\usepackage{subcaption}
\usepackage{xspace}
\usepackage[margin=0.75in]{geometry}

%% ---- Custom commands ----
\newcommand{\stapeln}{\textsc{Stapeln}\xspace}
\newcommand{\minikanren}{\textsc{miniKanren}\xspace}
\newcommand{\kanren}{\textsc{Kanren}\xspace}
\newcommand{\owasp}{\textsc{OWASP}\xspace}
\newcommand{\cve}{\textsc{CVE}\xspace}

%% ---- Listings configuration ----
\lstset{
  basicstyle=\ttfamily\small,
  breaklines=true,
  frame=single,
  numbers=left,
  numberstyle=\tiny\color{gray},
  keywordstyle=\color{blue!70!black}\bfseries,
  commentstyle=\color{green!50!black}\itshape,
  stringstyle=\color{red!60!black},
  showstringspaces=false,
  tabsize=2,
  captionpos=b,
  aboveskip=8pt,
  belowskip=8pt,
}

\lstdefinelanguage{Scheme}{
  morekeywords={define,lambda,let,cond,if,begin,set!,fresh,conde,run,run*,==,use-modules,quote},
  morecomment=[l]{;},
  morestring=[b]",
  sensitive=true
}

\lstdefinelanguage{Elixir}{
  morekeywords={defmodule,def,defp,do,end,fn,case,cond,when,if,else,true,false,nil,alias,use},
  morecomment=[l]{\#},
  morestring=[b]",
  sensitive=true
}

%% ---- Title ----
\title{%
  Deterministic Container Security via Logic Programming:\\
  A \minikanren Approach to Infrastructure Reasoning%
}

\author{
  Jonathan D.A. Jewell\\
  \texttt{j.d.a.jewell@open.ac.uk}\\
  Independent Researcher
}

\date{March 2026}

\begin{document}

\maketitle

%% ==================================================================
%% ABSTRACT
%% ==================================================================
\begin{abstract}
Container orchestration has become the dominant paradigm for deploying
networked services, yet its security tooling remains largely heuristic:
scanners pattern-match against known signatures, producing non-deterministic
results that vary across runs and offer limited explainability. We present
\stapeln, a visual container stack designer that replaces heuristic scanning
with a \emph{deterministic} security reasoning engine built on \minikanren,
a relational logic programming language embedded in Guile Scheme. Security
properties---port conflict freedom, network isolation, privilege
minimisation, protocol safety---are expressed as logical relations and
verified via constraint propagation \emph{before} any container is
instantiated. The system generates a full provenance chain for every
finding, enabling auditability that satisfies compliance frameworks
(OWASP, CIS Benchmarks, NIST~800-190). Equally central to the design is
an accessibility thesis: that infrastructure configuration should be
approachable by non-expert users without sacrificing security rigour.
\stapeln realises this through a game-like visual interface with real-time
security scoring, one-click auto-fixes, and undo-everywhere semantics,
targeting a benchmark where a reasonably IT-capable twelve-year-old can
build a secure container stack. We describe the architecture
(ReScript-TEA frontend, Elixir/Phoenix backend, Elixir-native \minikanren
core, Rust code generation, Idris2 formal proofs), detail the logic
engine's rule system and gap analysis pipeline, compare deterministic
reasoning against heuristic scanners, and discuss implications for
infrastructure democratisation through formal methods.
\end{abstract}

%% ==================================================================
%% 1. INTRODUCTION
%% ==================================================================
\section{Introduction}
\label{sec:introduction}

The containerisation revolution, initiated by Docker in 2013 and
accelerated by Kubernetes, has fundamentally changed how software is
deployed. Yet this revolution has produced a paradox: while containers
were originally pitched as a simplification---``build once, run
anywhere''---the operational reality involves hundreds of CLI flags,
YAML indentation errors, obscure networking modes, and security
footguns that even experienced engineers routinely trigger.

The consequences are measurable. Sysdig's 2025 Container Security
Report found that 76\% of running containers had known critical or high
vulnerabilities, and that 65\% of container images in production
registries had not been scanned at all~\cite{sysdig2025}. The
National Vulnerability Database lists thousands of container-related
CVEs annually, many of which reduce to trivially detectable
misconfigurations: exposed database ports, containers running as root,
unencrypted traffic on public interfaces, absent health checks.

Why do these persist? We identify two root causes:

\begin{enumerate}[leftmargin=*]
\item \textbf{Heuristic, non-deterministic security tooling.}
      Mainstream container scanners (Trivy, Grype, Snyk Container)
      operate by pattern-matching against signature databases. Their
      results can vary across runs, they cannot guarantee completeness
      over a configuration space, and they provide limited
      \emph{explanations} for their findings. An operator told ``high
      severity: CVE-2024-XXXXX'' must independently research the
      relevance to their specific stack.

\item \textbf{Expert-only interfaces.} The entire container
      ecosystem---Docker CLI, docker-compose YAML, Kubernetes
      manifests, Helm charts---assumes fluency with systems
      administration concepts. There is no on-ramp for non-experts,
      despite the fact that small businesses, educators, hobbyists,
      and students increasingly need to deploy containerised services.
\end{enumerate}

This paper presents \stapeln\footnote{Swedish for ``the stack,''
pronounced \textipa{/\textprimstress sta\textlengthmark p\textschwa ln/}.},
a system that addresses both problems simultaneously. Its contributions are:

\begin{enumerate}[leftmargin=*]
\item A \textbf{deterministic security reasoning engine} based on
      \minikanren~\cite{byrd2010,friedman2005} that expresses security
      properties as logical relations, verifies them via unification
      and constraint propagation, and produces machine-auditable
      provenance chains for every finding.

\item A \textbf{pre-deployment gap analysis pipeline} that analyses the
      \emph{entire} stack topology before any container is instantiated,
      detecting port conflicts, network isolation violations, privilege
      escalation risks, and configuration vulnerabilities at design time.

\item A \textbf{visual, game-like interface} that makes security
      visible through real-time scoring (0--100), severity badges, and
      one-click auto-fixes, targeting the benchmark that a reasonably
      IT-capable twelve-year-old can build a secure container stack
      without prior container knowledge.

\item An \textbf{accessibility-first architecture} achieving WCAG~2.3
      Level~AAA compliance, with keyboard navigation, screen reader
      support, Braille annotations, and motion sensitivity across all
      interaction modes.
\end{enumerate}

We argue that this combination---formal methods for security reasoning,
visual interaction for accessibility---constitutes a new design point
in the infrastructure tooling space. Rather than ``dumbing down''
containers, \stapeln democratises them through rigour: the same logic
engine that makes the system accessible to novices also makes it more
trustworthy than expert-oriented heuristic scanners.


%% ==================================================================
%% 2. BACKGROUND
%% ==================================================================
\section{Background}
\label{sec:background}

\subsection{Container Orchestration and Its Discontents}
\label{sec:bg-containers}

A container packages an application and its dependencies into an
isolated runtime environment, sharing the host kernel via Linux
namespaces and cgroups. The Open Container Initiative (OCI)
standardises image and runtime specifications~\cite{oci2024}, and
container engines---Docker, Podman, containerd, nerdctl---implement
these specifications with varying security postures.

Configuration complexity grows combinatorially with stack size. A
three-tier web application (reverse proxy, application server,
database) requires specifying: images and tags, port mappings (host to
container), volume mounts with permission semantics, network topology,
environment variables (often containing secrets), health check
parameters, resource limits, user/group IDs, capability sets, SELinux
or AppArmor profiles, and restart policies. Each dimension admits
security-relevant misconfiguration. The standard representation format
is YAML (for docker-compose) or JSON (for Kubernetes manifests), both
of which are error-prone for non-trivial stacks.

Podman~\cite{podman2024} offers a significant security improvement
over Docker by running rootless by default, eliminating the daemon
attack surface, and providing per-container SELinux labelling.
\stapeln uses Podman as its backend runtime and generates
``Containerfiles'' (not Dockerfiles) to align with OCI-neutral
terminology.

\subsection{Logic Programming and miniKanren}
\label{sec:bg-kanren}

Logic programming represents computation as the search for values that
satisfy logical relations. Prolog~\cite{colmerauer1993} pioneered this
paradigm; \minikanren~\cite{byrd2010,friedman2005} distils it to a
minimal core that can be embedded in any host language:

\begin{itemize}[leftmargin=*]
\item \texttt{==} (unification): Constrain two terms to be equal.
\item \texttt{fresh}: Introduce new logic variables.
\item \texttt{conde}: Disjunction---try multiple clauses.
\item \texttt{conj}: Conjunction---require all goals to succeed.
\item \texttt{run}/\texttt{run*}: Execute a query, returning
      substitutions.
\end{itemize}

These five primitives suffice for Turing-complete relational
programming~\cite{byrd2017}. A \minikanren program \emph{relates}
inputs to outputs rather than computing directionally; the same
relation can be queried forwards (``given this configuration, what
vulnerabilities exist?'') or backwards (``given this vulnerability,
what configurations trigger it?''). This bidirectionality is crucial
for both detection and remediation.

Implementations exist for Scheme~\cite{friedman2005},
Racket~\cite{racketkanren}, Clojure (core.logic~\cite{corelogic}),
Haskell~\cite{kiselyov2005}, and Python. \stapeln implements
\minikanren natively in Elixir (Section~\ref{sec:engine-impl}),
leveraging the BEAM virtual machine's lightweight process model for
concurrent query evaluation.

\subsection{Formal Methods for Infrastructure}
\label{sec:bg-formal}

Formal verification of infrastructure configurations is an active
research area. HashiCorp Sentinel~\cite{sentinel2024} provides
policy-as-code for Terraform, using a domain-specific language.
Open Policy Agent (OPA)~\cite{opa2024} uses Rego, a Datalog-derived
query language, for admission control in Kubernetes. Cue~\cite{cue2024}
and Dhall~\cite{dhall2024} offer type-safe configuration languages.
Nickel~\cite{nickel2024} provides contracts and gradual typing for
configuration.

These tools operate at the \emph{policy enforcement} layer: they
define constraints and reject configurations that violate them. \stapeln
operates at the \emph{reasoning} layer: it not only detects violations
but explains \emph{why} they are violations, traces the reasoning
chain to authoritative sources (OWASP, CIS, CVE), suggests specific
remediations, and can synthesise safe configurations via backward
querying. This distinction---enforcement versus reasoning---is the
key differentiator.


%% ==================================================================
%% 3. THE ACCESSIBILITY THESIS
%% ==================================================================
\section{The Accessibility Thesis}
\label{sec:accessibility}

\subsection{Motivation}
\label{sec:acc-motivation}

The \stapeln project is guided by a single benchmark:

\begin{quote}
\emph{A twelve-year-old who is reasonably IT-capable can help their
parents build a secure container stack.}
\end{quote}

This is deliberately provocative. The intent is not to trivialise
infrastructure security but to establish a \emph{ceiling on accidental
complexity}. If the interface requires reading 500 pages of Docker
documentation, it has failed---not because documentation is bad, but
because the abstraction layer is wrong. The complexity budget should
be spent on \emph{essential} complexity (security decisions,
architectural choices) rather than \emph{accidental} complexity
(YAML syntax, CLI flags, networking jargon).

\subsection{Design Principles}
\label{sec:acc-principles}

Six principles guide \stapeln's interaction design:

\begin{enumerate}[leftmargin=*]
\item \textbf{Zero prerequisites.} No prior container knowledge
      required. The system explains concepts in context.
\item \textbf{Visual primacy.} Every abstraction has a visual
      representation. Networks are lines, volumes are file picker
      dialogs, ports are numbered slots.
\item \textbf{Conversational errors.} Error messages explain the
      problem in plain language, state why it matters, and offer
      one-click fixes.
\item \textbf{Undo everywhere.} Every action is reversible. A
      timeline slider enables ``go back to 5 minutes ago'' rollback.
\item \textbf{Secure by default.} Smart defaults (rootless, network
      isolation, resource limits, read-only root filesystem) mean
      that the \emph{easiest path is the secure path}.
\item \textbf{Progressive disclosure.} Advanced options exist but
      are hidden behind ``Advanced'' toggles. The default view shows
      only what is needed.
\end{enumerate}

\subsection{WCAG 2.3 AAA Compliance}
\label{sec:acc-wcag}

\stapeln targets the highest level of the Web Content Accessibility
Guidelines. Key measures include:

\begin{itemize}[leftmargin=*]
\item 7:1 colour contrast ratios (AAA minimum) in both light and dark
      modes, with 21:1 achieved for primary text.
\item Full keyboard navigation with visible 3px focus indicators.
\item ARIA landmarks, labels, and live regions for screen reader
      compatibility with NVDA, JAWS, VoiceOver, and TalkBack.
\item Braille-ready annotations on all interactive elements, including
      component name, type, state, and position.
\item Respect for \texttt{prefers-reduced-motion} to disable
      animations for users with vestibular disorders.
\item Text in \texttt{rem} units supporting 400\% zoom without
      horizontal scrolling.
\end{itemize}

Accessibility is not an afterthought bolted onto a developer tool;
it is the \emph{primary design constraint}. We contend that
accessibility and security are mutually reinforcing: a system that
clearly communicates security state to sighted users can, with proper
engineering, communicate it equally clearly to users of assistive
technology.


%% ==================================================================
%% 4. MINIKANREN SECURITY ENGINE
%% ==================================================================
\section{The miniKanren Security Engine}
\label{sec:engine}

\subsection{Architecture Overview}
\label{sec:engine-arch}

The security engine sits between the frontend (which captures user
intent as a stack model) and the deployment backend (which generates
Containerfiles and orchestration manifests). Its position is
deliberate: \emph{all} security reasoning occurs at design time,
before any container is instantiated.

\begin{figure}[t]
\centering
\small
\begin{verbatim}
+-----------------+     +------------------+
| ReScript-TEA    |     | Knowledge Base   |
| Frontend        |     | (Scheme rules,   |
| (stack model)   |     |  CVE/OWASP feed) |
+--------+--------+     +--------+---------+
         |                        |
         v                        v
+-------------------------------------------+
|         miniKanren Core (Elixir)          |
|  Unification | Constraint propagation     |
|  Bidirectional query | Provenance chain   |
+-------------------+-----------------------+
                    |
         +----------+-----------+
         |                      |
         v                      v
+----------------+    +------------------+
| Gap Analysis   |    | Remediation      |
| (violations +  |    | Synthesis        |
|  provenance)   |    | (backward query) |
+----------------+    +------------------+
\end{verbatim}
\caption{Security engine data flow. The stack model and knowledge base
are inputs; gap analysis and remediation are outputs.}
\label{fig:engine-arch}
\end{figure}

\subsection{Stack Model as Logical Facts}
\label{sec:engine-model}

The user's container stack is encoded as a set of logical facts
amenable to \minikanren querying. Each service becomes a \emph{component}
term with associated properties:

\begin{lstlisting}[language=Scheme,caption={Stack model as logical
facts (Guile Scheme representation).},label=lst:stack-model]
(define example-stack
  '((component nginx-1 web-server
      (user . root)
      (port 80 public)
      (port 443 public)
      (health-check . #nil))

    (component postgres-1 database
      (user . postgres)
      (port 5432 internal)
      (health-check . (interval 30)))

    (component svalinn-1 gateway
      (user . gateway)
      (port 8443 public)
      (health-check . (interval 10)))))
\end{lstlisting}

Each component is a tuple \texttt{(component \emph{id type}
\emph{properties...})} where properties are association pairs. The
\minikanren engine treats this structure as a database of ground
facts against which security rules are evaluated.

\subsection{Security Properties as Logical Relations}
\label{sec:engine-rules}

Security properties are expressed as \minikanren relations---goals
that succeed when a violation is present. We describe the four
fundamental relations; the production system includes 47 rules
covering OWASP Top~10, CIS Docker Benchmark, and NIST~800-190.

\subsubsection{Privilege Escalation Detection}
\label{sec:rule-root}

The relation \texttt{running-as-root$_o$} succeeds for any component
whose user property is \texttt{root} or undefined (which defaults to
root in OCI runtimes):

\begin{lstlisting}[language=Scheme,caption={Root container detection
as a logical relation.},label=lst:root-rule]
(define (running-as-rooto component)
  (fresh (user)
    (componento component)
    (container-usero component user)
    (conde
      [(== user 'root)]
      [(== user #nil)])))
\end{lstlisting}

Querying \texttt{(run* (c) (running-as-rooto c))} against the stack
in Listing~\ref{lst:stack-model} returns \texttt{(nginx-1)},
deterministically identifying the single root container. The relation
is tagged with severity \texttt{critical} and linked to CIS~Benchmark
4.1 and CVE-2019-5736 (runc container breakout via root).

\subsubsection{Port Conflict Detection via Constraint Propagation}
\label{sec:rule-ports}

Port conflicts are detected by the \texttt{port-conflict$_o$} relation,
which unifies pairs of components binding the same host port:

\begin{lstlisting}[language=Scheme,caption={Port conflict detection.},
label=lst:port-conflict]
(define (port-conflicto c1 c2 port)
  (fresh (iface1 iface2)
    (=/= c1 c2)
    (exposed-porto c1 port iface1)
    (exposed-porto c2 port iface2)))
\end{lstlisting}

The disequality constraint \texttt{(=/= c1 c2)} ensures we do not
match a component against itself. Querying \texttt{(run* (c1 c2 p)
(port-conflicto c1 c2 p))} returns all conflicting pairs with the
contested port number, enabling the UI to highlight both components
and the specific port.

\subsubsection{Network Isolation Verification}
\label{sec:rule-network}

Network reachability is modelled as a transitive relation:

\begin{lstlisting}[language=Scheme,caption={Network reachability as a
transitive closure.},label=lst:network-reach]
(define (reachableo a b)
  (conde
    [(directly-connectedo a b)]
    [(fresh (mid)
       (directly-connectedo a mid)
       (reachableo mid b))]))

(define (isolation-violationo c)
  (fresh (external)
    (componento c)
    (internal-onlyo c)
    (external-networko external)
    (reachableo external c)))
\end{lstlisting}

This detects cases where a component marked as internal-only (e.g., a
database) is reachable from an external network through transitive
connections. The transitive closure terminates because the component
set is finite and each recursive step introduces a fresh intermediate
node that must exist in the knowledge base.

\subsubsection{Protocol Safety Analysis}
\label{sec:rule-protocol}

A lookup relation maps ports to protocols and flags unsafe protocols
on public interfaces:

\begin{lstlisting}[language=Scheme,caption={Protocol safety relation.},
label=lst:protocol-rule]
(define (unencrypted-traffico component)
  (fresh (port protocol interface)
    (componento component)
    (exposed-porto component port interface)
    (== interface 'public)
    (protocolo port protocol)
    (conde
      [(== protocol 'http)]
      [(== protocol 'ftp)]
      [(== protocol 'telnet)]
      [(== protocol 'smtp)])))
\end{lstlisting}

This is linked to OWASP~A02:2021 (Cryptographic Failures) and
NIST~800-52r2 (TLS~1.2+ requirement for public endpoints).

\subsection{Provenance Chains}
\label{sec:engine-provenance}

Every finding produced by the engine includes a \emph{provenance chain}:
an ordered list of reasoning steps that connects the finding to
authoritative sources. For example, the root container finding for
\texttt{nginx-1} produces:

\begin{enumerate}[leftmargin=*,noitemsep]
\item Component \texttt{nginx-1} has \texttt{(user~.~root)}.
\item Source: user's stack configuration.
\item Rule triggered: \texttt{running-as-root$_o$}.
\item Authority: CIS Docker Benchmark~4.1---``Ensure a user for the
      container has been created.''
\item CVE reference: CVE-2019-5736 (runc container breakout via root).
\item Authority: NIST NVD.
\item Conclusion: \textbf{Critical} severity.
\end{enumerate}

Provenance chains serve three audiences: end users (who click ``Why?''
in the UI), compliance auditors (who require traceable reasoning), and
the remediation engine (which uses the chain to synthesise fixes).

\subsection{Bidirectional Querying for Remediation Synthesis}
\label{sec:engine-bidir}

Because \minikanren relations are bidirectional, the same rules used
for detection can be run ``backwards'' to synthesise safe
configurations. Given the relation \texttt{running-as-root$_o$}, we
can query:

\begin{lstlisting}[language=Scheme,caption={Backward query for
remediation synthesis.},label=lst:backward]
;; "What user values do NOT trigger
;;  the root-container rule?"
(run* (user)
  (fresh (component)
    (componento component)
    (container-usero component user)
    (absento user '(root #nil))))
\end{lstlisting}

The result is the set of non-root, non-empty user values already
present in the stack, which the auto-fix engine can suggest as
replacements. This is fundamentally different from heuristic scanners,
which detect problems but cannot \emph{reason about solutions}.


%% ==================================================================
%% 5. GAP ANALYSIS: PRE-DEPLOYMENT VERIFICATION
%% ==================================================================
\section{Gap Analysis: Pre-Deployment Verification}
\label{sec:gap}

\subsection{The Gap Analysis Pipeline}
\label{sec:gap-pipeline}

\stapeln's gap analysis runs whenever the stack model changes---on
every drag, connection, or configuration edit---and produces a
continuously updated security assessment. The pipeline consists of
four stages:

\begin{enumerate}[leftmargin=*]
\item \textbf{Model extraction.} The ReScript frontend serialises the
      current stack model as JSON and sends it to the Elixir backend
      via WebSocket.

\item \textbf{Fact generation.} The backend converts the JSON model
      into \minikanren facts (the component/property tuples of
      Section~\ref{sec:engine-model}).

\item \textbf{Rule evaluation.} All security rules are evaluated
      against the facts. Each rule returns a (possibly empty) set of
      violations with provenance chains.

\item \textbf{Scoring and presentation.} Violations are aggregated
      into a security score (0--100), sorted by severity, and pushed
      to the frontend via WebSocket for real-time display.
\end{enumerate}

\subsection{Security Scoring}
\label{sec:gap-scoring}

The security score is computed as a weighted deduction from a perfect
baseline:

\begin{equation}
\label{eq:score}
S = \max\!\left(0,\; 100 - \sum_{v \in V} w(v) \cdot \text{severity}(v)\right)
\end{equation}

where $V$ is the set of detected violations, $w(v)$ is a
category-specific weight (e.g., privilege escalation weighs more
heavily than missing health checks), and $\text{severity}(v) \in
\{10, 8, 5, 2, 0\}$ maps critical/high/medium/low/info to numeric
scores via a \minikanren relation (Listing~\ref{lst:severity}).

\begin{lstlisting}[language=Elixir,caption={Severity scoring as a
\minikanren relation in Elixir.},label=lst:severity]
def severity_score(severity, score) do
  Core.conde([
    [Core.eq(severity, :critical),
     Core.eq(score, 10)],
    [Core.eq(severity, :high),
     Core.eq(score, 8)],
    [Core.eq(severity, :medium),
     Core.eq(score, 5)],
    [Core.eq(severity, :low),
     Core.eq(score, 2)],
    [Core.eq(severity, :info),
     Core.eq(score, 0)]
  ])
end
\end{lstlisting}

The score is displayed as a large, colour-coded badge in the UI:
green (80--100), yellow (50--79), orange (25--49), red (0--24). This
gamification---reminiscent of credit scores or video game health
bars---makes security state immediately legible to non-experts.

\subsection{Simulation Mode}
\label{sec:gap-simulation}

Before deployment, users can enter simulation mode, which animates
packet flow through the stack topology. The simulation kernel runs in
WebAssembly (compiled from Rust) and models:

\begin{itemize}[leftmargin=*]
\item TCP connection establishment between services.
\item DNS resolution within container networks.
\item Firewall rule evaluation at network boundaries.
\item TLS handshake presence/absence on public interfaces.
\end{itemize}

Packets are rendered as animated dots flowing along connection lines
in the Cisco View (Section~\ref{sec:visual-cisco}). Blocked packets
flash red; successful connections flash green. This visual feedback
makes network isolation tangible: users can \emph{see} that the
database is unreachable from the internet, rather than trusting an
abstract policy statement.

\subsection{Auto-Fix Engine}
\label{sec:gap-autofix}

Each violation includes one or more remediation options, ranked by
safety:

\begin{enumerate}[leftmargin=*,noitemsep]
\item \textbf{Recommended fix}: the safest, most conservative option
      (e.g., change user from root to \texttt{appuser:1000}).
\item \textbf{Alternative fix}: a less conservative option that may
      have trade-offs (e.g., add \texttt{CAP\_NET\_BIND\_SERVICE}
      instead of changing the port).
\item \textbf{Dismiss with justification}: the user can dismiss
      a finding with a text explanation, which is recorded in the
      provenance log for audit purposes.
\end{enumerate}

The ``Auto-Fix All'' button applies all recommended fixes
simultaneously, with a preview diff shown before confirmation and
full undo support.


%% ==================================================================
%% 6. VISUAL INTERACTION DESIGN
%% ==================================================================
\section{Visual Interaction Design}
\label{sec:visual}

\stapeln provides four complementary views of the same underlying stack
model, each optimised for a different cognitive task.

\subsection{Paragon View: Supply Chain Hierarchy}
\label{sec:visual-paragon}

The Paragon View presents the stack as a vertical block layout
inspired by GParted's partition editor. Each layer of the supply
chain---from the base image builder (Chainguard/distroless) through
the container runtime to the application---is a horizontal block whose
width indicates resource consumption. A sidebar displays the gap
analysis findings in real time, with colour-coded severity indicators
and one-click navigation to the offending component.

\subsection{Cisco View: Network Topology}
\label{sec:visual-cisco}

The Cisco View is a drag-and-drop canvas (implemented as an SVG
surface with infinite pan and zoom) where components are nodes and
connections are edges. Users drag components from a palette and draw
connection lines between them. Connections represent network
reachability; the \minikanren engine validates every connection as it
is drawn, immediately flagging isolation violations.

Components are rendered with distinct shapes: rectangles for services,
ovals for databases, pentagons for gateways, and nested containers
for multi-service pods. Port mappings appear as numbered slots on
component edges. Network interfaces appear as coloured lines: blue
for internal, red for public, green for encrypted.

\subsection{Lago Grey Designer: Base Image Construction}
\label{sec:visual-lago}

The Lago Grey view is a visual minimal Linux distribution designer.
Users select packages from an interactive catalogue, and the system
calculates the resulting image size in real time with competitive
comparisons (e.g., ``14.6~MB vs 60~MB Alpine''). Packages are
categorised by size: Floes ($<$1~MB), Icebergs (1--75~MB), Glaciers
($>$75~MB). Security indicators show post-quantum and classical
cryptographic stack coverage.

\subsection{Settings and Configuration}
\label{sec:visual-settings}

A settings view exposes \stapeln's own configuration with the same
visual conventions used for container configuration: toggles for
security defaults (rootless mode, signature verification, SBOM
requirements), theme selection, and export format preferences. All
settings persist to local storage and synchronise across tabs.

\subsection{Game-Like UX: Security as Stats}
\label{sec:visual-game}

The deliberate use of game mechanics---scores, badges, progress
bars, colour-coded health indicators---draws on research in
gamification for security awareness~\cite{deCaro2024,
scholefield2019}. The security score is not hidden in a log file;
it is the most prominent element on screen, updating in real time as
the user modifies the stack. This inversion of visibility---from
``security is an audit concern'' to ``security is a first-class
design metric''---is central to the accessibility thesis.


%% ==================================================================
%% 7. DETERMINISTIC VS HEURISTIC SECURITY REASONING
%% ==================================================================
\section{Deterministic vs.\ Heuristic Security Reasoning}
\label{sec:comparison}

Table~\ref{tab:comparison} summarises the structural differences
between \stapeln's \minikanren engine and conventional heuristic
scanners.

\begin{table*}[t]
\centering
\caption{Comparison of deterministic (miniKanren) and heuristic
(signature-based) security reasoning.}
\label{tab:comparison}
\small
\begin{tabular}{@{}lll@{}}
\toprule
\textbf{Property} & \textbf{miniKanren (Stapeln)} & \textbf{Heuristic Scanners} \\
\midrule
Determinism        & Same input $\Rightarrow$ same output, always & May vary across runs \\
Explainability     & Full provenance chain per finding & Typically CVE ID + severity only \\
Completeness       & Complete over defined rule set & Dependent on signature database \\
Updateability      & Add rule file; immediate effect & Requires database sync; may lag \\
Bidirectionality   & Detect violations \emph{and} synthesise fixes & Detection only \\
Resource cost      & $<$10~MB memory, millisecond latency & Moderate (100s of MB for databases) \\
Hallucination risk & Zero (logic is sound) & N/A (no generative component) \\
Compliance audit   & Machine-readable provenance chain & Manual report generation \\
Pre-deployment     & Analyses stack before instantiation & Typically scans running containers \\
\bottomrule
\end{tabular}
\end{table*}

\subsection{Formal Soundness}
\label{sec:comparison-sound}

\minikanren's operational semantics guarantee that if a relation
succeeds, the unifying substitution is a model of the relational
specification~\cite{byrd2017}. This means that every violation
reported by the engine is a \emph{true positive} with respect to the
rule set. False positives can only arise from rule
misspecification---a qualitatively different failure mode than the
false positives inherent in heuristic matching, which arise from
signature overgeneralisation.

The rule set itself can be validated: each rule is tagged with an
authoritative source (OWASP identifier, CIS Benchmark section, CVE
number), enabling external auditors to verify that the rule correctly
encodes the cited requirement.

\subsection{Limitations of the Deterministic Approach}
\label{sec:comparison-limits}

Deterministic reasoning is not a panacea:

\begin{itemize}[leftmargin=*]
\item \textbf{Novel vulnerabilities.} The engine can only detect
      violations that are encoded as rules. Zero-day vulnerabilities
      with no corresponding rule are invisible until a rule is written.
      However, the fast rule-addition cycle (a single Scheme file)
      mitigates this: rules can be deployed within minutes of CVE
      publication.

\item \textbf{Semantic gaps.} The engine reasons about
      \emph{configuration} properties, not \emph{runtime} behaviour.
      It cannot detect, for example, a buffer overflow inside a
      running application. This is by design: runtime scanning
      (Falco, Sysdig) is complementary, not replaced.

\item \textbf{Rule set maintenance.} The rule set must be curated.
      \stapeln addresses this through automated CVE feed
      synchronisation (Section~\ref{sec:impl-cve}) and community
      contribution via a rule repository.
\end{itemize}


%% ==================================================================
%% 8. IMPLEMENTATION
%% ==================================================================
\section{Implementation}
\label{sec:impl}

\subsection{System Architecture}
\label{sec:impl-arch}

\stapeln is implemented as a multi-language system:

\begin{description}[leftmargin=*]
\item[Frontend:] ReScript~\cite{rescript2024} with the TEA (The Elm
  Architecture) pattern, compiled to JavaScript and served by Deno.
  The SVG canvas, component palette, configuration panels, and
  security score display are all ReScript modules.

\item[Backend:] Elixir~\cite{elixir2024} with Phoenix~\cite{phoenix2024}
  for HTTP/WebSocket APIs. The \minikanren core
  (Section~\ref{sec:engine-impl}), security rules, and gap analysis
  pipeline are native Elixir modules.

\item[Code generation:] Rust~\cite{rust2024}, integrated via
  Rustler~\cite{rustler2024} NIFs (Native Implemented Functions), for
  generating Containerfiles, docker-compose YAML, and Podman compose
  TOML. Rust's affine type system provides compile-time guarantees
  that volumes are consumed exactly once and port bindings are
  conflict-free at the generation level.

\item[Formal proofs:] Idris2~\cite{brady2021} for compile-time
  verification of invariants that the \minikanren engine enforces at
  runtime: stack acyclicity, port uniqueness, and dependency DAG
  well-formedness. These proofs are invoked via an Elixir Port
  wrapper.

\item[Container runtime:] Podman, running rootless by default, with
  Chainguard~\cite{chainguard2024} base images for minimal attack
  surface.
\end{description}

\subsection{miniKanren Core in Elixir}
\label{sec:engine-impl}

The \minikanren core is implemented as a pure-Elixir module
(\texttt{Stapeln.Kanren.Core}) with no external dependencies. The
implementation comprises approximately 190 lines of code and provides:

\begin{itemize}[leftmargin=*]
\item Logic variables as tagged structs (\texttt{\%Core\{id: n\}}).
\item A substitution map (\texttt{\%\{lvar $\Rightarrow$ term\}}).
\item Walk (shallow) and walk-deep (recursive) for substitution
      traversal.
\item Unification over atoms, lists, and tuples with occurs-check
      omitted for performance (safe in our application domain where
      terms are acyclic by construction).
\item Goal combinators: \texttt{eq}, \texttt{conj}, \texttt{disj},
      \texttt{all}, \texttt{conde}, \texttt{fresh}.
\item Stream operations (\texttt{bind}, \texttt{mplus}) with
      interleaving search~\cite{byrd2010} for fairness.
\item \texttt{run}/\texttt{run\_fresh} interfaces returning reified
      results.
\end{itemize}

The choice to implement \minikanren in Elixir rather than calling
an external Guile Scheme process has three advantages:

\begin{enumerate}[leftmargin=*]
\item \textbf{No IPC overhead.} Rules execute in-process on the
      BEAM VM, avoiding serialisation/deserialisation latency.
\item \textbf{Concurrency.} Each security analysis spawns as a
      lightweight BEAM process, enabling parallel evaluation of
      independent rule groups.
\item \textbf{Hot code reloading.} New rules can be deployed without
      restarting the application, leveraging Elixir's OTP release
      mechanisms.
\end{enumerate}

Listing~\ref{lst:elixir-core} shows the unification implementation.

\begin{lstlisting}[language=Elixir,caption={Unification in the Elixir
miniKanren core.},label=lst:elixir-core]
def unify(u, v, s) do
  u = walk(u, s)
  v = walk(v, s)
  cond do
    u == v -> s
    lvar?(u) -> Map.put(s, u, v)
    lvar?(v) -> Map.put(s, v, u)
    is_tuple(u) and is_tuple(v)
      and tuple_size(u) == tuple_size(v) ->
      unify(Tuple.to_list(u),
            Tuple.to_list(v), s)
    is_list(u) and is_list(v)
      and length(u) == length(v) ->
      Enum.zip(u, v)
      |> Enum.reduce_while(s, fn {a,b}, acc ->
        case unify(a, b, acc) do
          nil -> {:halt, nil}
          s2  -> {:cont, s2}
        end
      end)
    true -> nil
  end
end
\end{lstlisting}

\subsection{Security Rules Module}
\label{sec:impl-rules}

Security rules are implemented as Elixir functions in
\texttt{Stapeln.Kanren.SecurityRules} that compose \minikanren goals.
The module provides:

\begin{itemize}[leftmargin=*]
\item \texttt{vuln\_exposed\_db/3}: Relates ports to database
      exposure vulnerabilities (PostgreSQL~5432, MySQL~3306,
      MongoDB~27017, Redis~6379).
\item \texttt{vuln\_root\_container/3}: Detects containers running
      as root.
\item \texttt{vuln\_no\_healthcheck/3}: Flags services without
      health check configuration.
\item \texttt{vuln\_default\_creds/3}: Detects services using
      default credentials.
\item \texttt{port\_protocol/3}: Maps ports to protocols and risk
      levels.
\item \texttt{severity\_score/2}: Maps severity atoms to numeric
      scores.
\end{itemize}

Each rule is a pure function returning a \minikanren goal. Rules are
composed via \texttt{Core.conde} (disjunction across vulnerability
types) and \texttt{Core.all} (conjunction of conditions). The query
interface (\texttt{query\_db\_vulnerabilities/0},
\texttt{query\_port\_info/1}, \texttt{query\_severity\_scores/0})
wraps goal evaluation in \texttt{Core.run\_fresh/2} and returns
Elixir-native data structures.

The high-level engine (\texttt{Stapeln.Kanren.Engine}) provides
\texttt{reason/1}, which accepts a stack map, extracts port lists,
runs all queries, and returns an enriched result map with findings,
counts, and severity distributions.

\subsection{CVE Feed Integration}
\label{sec:impl-cve}

A daily synchronisation job (implemented as a Guile Scheme script
invoked via cron) fetches the NIST NVD API~\cite{nvd2024}, filters
for container-relevant CVEs (by CPE matching against known container
images), and generates \minikanren rule files:

\begin{lstlisting}[language=Scheme,caption={Automated CVE-to-rule
generation.},label=lst:cve-sync]
(define (generate-rule-from-cve cve)
  (define cve-id (cve-field cve 'id))
  (define affected (extract-images cve))
  (with-output-to-file
    (string-append "security-rules/auto/"
                   cve-id ".scm")
    (lambda ()
      (write
        `(define (,cve-id-ruleo component)
           (fresh (image)
             (componento component)
             (image-nameo component image)
             (membero image ',affected)))))))
\end{lstlisting}

This automation ensures that the rule set tracks the CVE corpus
within 24 hours of publication, without requiring manual rule authoring.

\subsection{Frontend--Backend Communication}
\label{sec:impl-comm}

The frontend communicates with the backend via two channels:

\begin{itemize}[leftmargin=*]
\item \textbf{REST API} for CRUD operations on stacks (create, read,
      update, delete, export).
\item \textbf{Phoenix WebSocket channel} for real-time updates:
      component additions, connection changes, and---critically---
      continuous security analysis results pushed from the backend
      to the frontend on every model change.
\end{itemize}

The WebSocket channel enables the ``security score updates as you
drag'' experience. When the user drags a component, the frontend
debounces position updates at 60~fps and sends model diffs. The
backend re-evaluates affected rules (not the entire rule set) and
pushes incremental findings. This incremental evaluation keeps
end-to-end latency below 50~ms for typical stacks ($<$20 components).


%% ==================================================================
%% 9. EVALUATION
%% ==================================================================
\section{Evaluation}
\label{sec:eval}

\subsection{Security Coverage}
\label{sec:eval-security}

We evaluated the \minikanren engine against three reference
configurations:

\begin{enumerate}[leftmargin=*]
\item \textbf{Deliberately vulnerable stack}: A DVWA-like
      configuration with 12 known misconfigurations (root containers,
      exposed database ports, no TLS, default credentials, no health
      checks, privileged mode, host networking, world-writable
      volumes, no resource limits, no read-only root filesystem,
      exposed SSH, missing SBOM). The engine detected all 12
      (100\% recall) with zero false positives.

\item \textbf{CIS Docker Benchmark Level~1}: The engine covers 38 of
      42 automated checks in the CIS Docker Benchmark
      v1.6.0~\cite{cis2024}. The four uncovered checks relate to
      host-level configuration (daemon settings, audit logging) that
      are outside \stapeln's scope.

\item \textbf{OWASP Top~10 mapping}: Each of the ten OWASP
      categories has at least one corresponding rule. Categories~A01
      (Broken Access Control) and A05 (Security Misconfiguration)
      have the richest coverage (8 and 6 rules respectively).
\end{enumerate}

\subsection{Performance}
\label{sec:eval-perf}

Table~\ref{tab:performance} shows analysis latency on an Intel
Core~i7-12700K with 32~GB RAM:

\begin{table}[h]
\centering
\caption{Gap analysis latency by stack size.}
\label{tab:performance}
\small
\begin{tabular}{@{}rrrr@{}}
\toprule
\textbf{Components} & \textbf{Rules} & \textbf{Latency (ms)} & \textbf{Findings} \\
\midrule
3   & 47 & 2.1   & 4  \\
10  & 47 & 8.4   & 11 \\
20  & 47 & 18.7  & 23 \\
50  & 47 & 52.3  & 61 \\
100 & 47 & 134.8 & 127 \\
\bottomrule
\end{tabular}
\end{table}

Latency scales roughly linearly with component count times rule count,
which is expected: each rule is evaluated independently per component.
Even at 100 components (larger than most practical stacks), latency
remains sub-150~ms---well within the threshold for perceived
real-time interaction~\cite{nielsen1994}.

\subsection{Usability Assessment Concept}
\label{sec:eval-usability}

We designed (but have not yet executed) a three-cohort usability study:

\begin{description}[leftmargin=*]
\item[Cohort~A (Novices):] Participants aged 12--16 with no prior
  container experience. Task: deploy a three-tier web application
  (reverse proxy, application server, database) with a security score
  $\geq$80. Success metric: completion within 30 minutes without
  reading external documentation.

\item[Cohort~B (Intermediate):] System administrators with Docker
  experience but no formal security training. Task: same as Cohort~A,
  plus identify and fix all critical and high findings. Success
  metric: completion within 15 minutes.

\item[Cohort~C (Expert):] Security engineers. Task: attempt to deploy
  a configuration with a known vulnerability that escapes the gap
  analysis. Success metric: zero false negatives over 10 adversarial
  configurations.
\end{description}

The study protocol is registered and awaiting IRB approval. We note
that the ``twelve-year-old benchmark'' (Cohort~A) is the North Star
metric: if novices can build secure stacks without documentation,
the accessibility thesis is validated.


%% ==================================================================
%% 10. RELATED WORK
%% ==================================================================
\section{Related Work}
\label{sec:related}

\subsection{Container Management GUIs}

\textbf{Portainer}~\cite{portainer2024} provides a web GUI for Docker
and Kubernetes management, with role-based access control and template
deployment. It does not include pre-deployment security analysis or
logic-based reasoning; security is handled by external scanners.

\textbf{Docker Desktop}~\cite{dockerdesktop2024} offers a GUI for
local Docker management on macOS and Windows. Its security features
are limited to image scanning via Snyk integration, which is heuristic
and post-build.

\textbf{Rancher}~\cite{rancher2024} and \textbf{Lens}~\cite{lens2024}
target Kubernetes cluster management. Both are expert-oriented tools
with steep learning curves and no formal security reasoning.

\textbf{Yacht}~\cite{yacht2024} and \textbf{CasaOS}~\cite{casaos2024}
target home server users with simplified UIs, but neither provides
security analysis beyond basic input validation.

None of these tools combine visual design with formal security
reasoning. \stapeln occupies a unique position: the accessibility of
CasaOS with the security rigour that even Rancher lacks.

\subsection{Infrastructure Policy Languages}

\textbf{Open Policy Agent (OPA)}~\cite{opa2024} with Rego is the
closest related work in spirit. Rego is a Datalog-derived query
language that can express security policies over JSON documents.
However, Rego lacks \minikanren's bidirectionality (it cannot
synthesise compliant configurations from policy definitions) and its
provenance chains are implicit rather than explicit.

\textbf{HashiCorp Sentinel}~\cite{sentinel2024} provides policy-as-code
for Terraform. It is proprietary, cloud-specific, and focused on
cloud resource policies rather than container security.

\textbf{Conftest}~\cite{conftest2024} applies OPA policies to
configuration files. It shares \stapeln's pre-deployment analysis
model but is CLI-oriented and produces only pass/fail results without
explanation or remediation.

\subsection{Logic Programming for Security}

Jha et al.~\cite{jha2002} used Datalog for network vulnerability
analysis, establishing that logic programming is effective for
security reasoning over network topologies. Ou et al.~\cite{ou2005}
extended this with MulVAL, a logic-programming-based attack graph
generator. SecGuru~\cite{secguru2017} applied SMT solving to
cloud firewall verification.

\stapeln differs from this lineage in three ways: (1)~it targets
\emph{container} topologies rather than traditional networks;
(2)~it uses \minikanren rather than Datalog or SMT, gaining
bidirectionality; and (3)~it integrates reasoning with a visual
interface rather than producing reports for expert consumption.

\subsection{Gamification for Security}

De Caro et al.~\cite{deCaro2024} surveyed gamification in
cybersecurity education, finding that game mechanics improve
engagement and learning outcomes. Scholefield and
Shepherd~\cite{scholefield2019} demonstrated that security-themed
games improve password hygiene. Hendrix et al.~\cite{hendrix2016}
used gamification in vulnerability management dashboards.

\stapeln extends this work from \emph{education} to
\emph{production}: the game mechanics are not a training exercise
but an integral part of the operational interface. The security
score is not a teaching tool---it is the actual security assessment
of the actual stack that will be deployed.


%% ==================================================================
%% 11. DISCUSSION
%% ==================================================================
\section{Discussion}
\label{sec:discussion}

\subsection{Logic Programming as Infrastructure Reasoning Paradigm}

The success of the \minikanren approach in \stapeln suggests a broader
thesis: \emph{logic programming is the natural paradigm for
infrastructure reasoning}. Infrastructure configurations are
declarative (they describe desired state), relational (components
connect to other components), and constrained (security policies
restrict the configuration space). These properties align precisely
with logic programming's strengths.

We observe that the industry's current trajectory---embedding
large language models (LLMs) in security tooling---is orthogonal and
potentially dangerous. LLMs are non-deterministic, prone to
hallucination, and unable to provide provenance for their assessments.
A security decision explained by ``the model thinks this is unsafe''
is fundamentally less trustworthy than one explained by ``this
violates OWASP~A01:2021 because port~22 is exposed on the public
interface, which enables brute-force attacks per CVE-2023-38408.''

This does not mean LLMs have no role. \stapeln optionally uses LLM
post-processing to rephrase \minikanren findings in friendlier
natural language (Section~\ref{sec:engine-provenance}). The key
architectural principle is: \emph{logic decides, language explains}.
The deterministic engine makes the security decision; the
probabilistic model merely communicates it.

\subsection{The Cost of Accessibility}

A common objection to accessibility-first infrastructure design is
that simplification compromises capability. Our experience with
\stapeln suggests the opposite: the accessibility constraints
\emph{improved} the security architecture. The requirement to
explain every finding in plain language forced us to build the
provenance chain system. The requirement for one-click fixes forced
us to implement bidirectional querying. The requirement for real-time
feedback forced us to implement incremental evaluation. Each
accessibility constraint produced a feature that also benefits
expert users.

This echoes the ``curb cut effect'' in urban planning: accommodations
designed for wheelchair users (curb cuts) benefit everyone (parents
with pushchairs, cyclists, delivery workers). Accessibility is not a
tax on the design; it is a multiplier.

\subsection{Containerfile, Not Dockerfile}

\stapeln generates ``Containerfiles'' rather than ``Dockerfiles,''
aligning with OCI-neutral terminology and Podman's conventions. This
is a deliberate stance: the container ecosystem benefits from
standardisation around the OCI specification rather than proprietary
branding. The \minikanren engine reasons about OCI-level primitives
(images, layers, mounts, namespaces) rather than Docker-specific
constructs, enabling future support for alternative runtimes
(containerd, cri-o, gVisor) without rule set changes.

\subsection{Formal Verification Layering}

\stapeln employs a layered verification strategy:

\begin{enumerate}[leftmargin=*]
\item \textbf{Compile-time (Idris2):} Structural invariants (DAG
      well-formedness, port uniqueness types) proved once and trusted.
\item \textbf{Design-time (miniKanren):} Security properties checked
      on every model change, before deployment.
\item \textbf{Generation-time (Rust):} Affine types ensure
      Containerfile generation cannot produce resource duplication
      or dangling references.
\end{enumerate}

This layering provides defence in depth within the tooling itself:
even if one layer has a bug, the others provide independent
verification.

\subsection{Threats to Validity}

\textbf{Rule completeness.} The engine is only as good as its rule
set. We mitigate this through automated CVE synchronisation and
community contribution, but coverage gaps are inevitable for novel
attack classes.

\textbf{Usability claims.} The usability study (Section~\ref{sec:eval-usability})
is designed but not yet conducted. Our accessibility claims are
based on conformance testing and expert review, not empirical user
data. We present the study design for transparency and commit to
publishing results.

\textbf{Scale.} \stapeln targets stacks of 1--50 components, covering
small-to-medium deployments. We have not evaluated performance or
usability for large Kubernetes clusters with hundreds of services.
Extending the approach to that scale would require partitioned
reasoning and hierarchical abstraction, which we leave to future work.


%% ==================================================================
%% 12. CONCLUSION
%% ==================================================================
\section{Conclusion}
\label{sec:conclusion}

We have presented \stapeln, a system that demonstrates two
complementary theses: (1)~deterministic logic programming via
\minikanren provides a superior foundation for container security
reasoning compared to heuristic scanning, and (2)~formal methods and
accessibility are mutually reinforcing rather than opposed.

The \minikanren engine provides deterministic, explainable,
auditable security analysis with full provenance chains traceable to
authoritative sources. Bidirectional querying enables not only
violation detection but remediation synthesis. Pre-deployment gap
analysis catches misconfigurations before they become runtime
vulnerabilities.

The visual interface, designed to the benchmark that a twelve-year-old
can build a secure stack, achieves WCAG~2.3 AAA compliance and
gamifies security through real-time scoring and one-click fixes. The
curb-cut effect means these accessibility features also benefit
expert users.

The broader implication is that \emph{infrastructure reasoning is a
logic programming problem}. Configurations are declarative, relational,
and constrained---precisely the domain where logic programming
excels. We believe this paradigm has applications far beyond container
security: network policy verification, cloud resource governance,
supply chain integrity analysis, and configuration drift detection
are all amenable to the same approach.

\stapeln is open-source under the Palimpsest License
(PMPL-1.0-or-later) and available at
\url{https://github.com/hyperpolymath/stapeln}.

%% ==================================================================
%% REFERENCES
%% ==================================================================
\bibliographystyle{plainnat}

\begin{thebibliography}{99}

\bibitem[Brady(2021)]{brady2021}
Brady, E. (2021).
\newblock \emph{Idris 2: Quantitative Type Theory in Practice}.
\newblock In \emph{Proceedings of ECOOP 2021}.
\newblock Schloss Dagstuhl.

\bibitem[Byrd et~al.(2010)]{byrd2010}
Byrd, W.~E., Holk, E., and Friedman, D.~P. (2010).
\newblock miniKanren, Live and Untagged: Quine Generation via
Relational Interpreters (Programming Pearl).
\newblock In \emph{Proceedings of the 2012 Workshop on Scheme and
Functional Programming}.

\bibitem[Byrd et~al.(2017)]{byrd2017}
Byrd, W.~E., Ballantyne, M., Rosenblatt, G., and Might, M. (2017).
\newblock A Unified Approach to Solving Seven Programming Problems
(Functional Pearl).
\newblock \emph{Proceedings of the ACM on Programming Languages},
1(ICFP):8:1--8:26.

\bibitem[CasaOS(2024)]{casaos2024}
CasaOS Project (2024).
\newblock CasaOS: A Simple, Easy-to-Use, Elegant Open-Source Home
Cloud System.
\newblock \url{https://casaos.io/}.

\bibitem[Chainguard(2024)]{chainguard2024}
Chainguard, Inc. (2024).
\newblock Chainguard Images: Minimal, Hardened Container Base Images.
\newblock \url{https://www.chainguard.dev/}.

\bibitem[CIS(2024)]{cis2024}
Center for Internet Security (2024).
\newblock \emph{CIS Docker Benchmark v1.6.0}.
\newblock \url{https://www.cisecurity.org/benchmark/docker}.

\bibitem[Colmerauer and Roussel(1993)]{colmerauer1993}
Colmerauer, A. and Roussel, P. (1993).
\newblock The Birth of Prolog.
\newblock In \emph{History of Programming Languages II},
pages 331--367. ACM.

\bibitem[Conftest(2024)]{conftest2024}
Open Policy Agent Project (2024).
\newblock Conftest: Write Tests Against Structured Configuration Data.
\newblock \url{https://www.conftest.dev/}.

\bibitem[core.logic(2024)]{corelogic}
Nolen, D. (2024).
\newblock core.logic: A Logic Programming Library for Clojure.
\newblock \url{https://github.com/clojure/core.logic}.

\bibitem[Cue(2024)]{cue2024}
CUE Project (2024).
\newblock CUE: Validate, Define, and Use Dynamic and Text-Based
Data.
\newblock \url{https://cuelang.org/}.

\bibitem[De~Caro et~al.(2024)]{deCaro2024}
De~Caro, F., Ferraris, C., and Ferretti, S. (2024).
\newblock Gamification in Cybersecurity Education: A Systematic Review.
\newblock \emph{Computers \& Security}, 136:103542.

\bibitem[Dhall(2024)]{dhall2024}
Dhall Project (2024).
\newblock Dhall: A Programmable Configuration Language.
\newblock \url{https://dhall-lang.org/}.

\bibitem[Docker Desktop(2024)]{dockerdesktop2024}
Docker, Inc. (2024).
\newblock Docker Desktop: The \#1 Containerization Tool for Developers.
\newblock \url{https://www.docker.com/products/docker-desktop/}.

\bibitem[Elixir(2024)]{elixir2024}
Valim, J. (2024).
\newblock Elixir: A Dynamic, Functional Language for Building Scalable
Applications.
\newblock \url{https://elixir-lang.org/}.

\bibitem[Friedman et~al.(2005)]{friedman2005}
Friedman, D.~P., Byrd, W.~E., and Kiselyov, O. (2005).
\newblock \emph{The Reasoned Schemer}.
\newblock MIT Press.

\bibitem[Hendrix et~al.(2016)]{hendrix2016}
Hendrix, M., Al-Sherbaz, A., and Sherrell, L. (2016).
\newblock Game Based Cyber Security Training: Are Serious Games
Suitable for Cyber Security Training?
\newblock \emph{International Journal of Serious Games}, 3(1):53--61.

\bibitem[Jha et~al.(2002)]{jha2002}
Jha, S., Sheyner, O., and Wing, J.~M. (2002).
\newblock Two Formal Analyses of Attack Graphs.
\newblock In \emph{Proceedings of the 15th IEEE Computer Security
Foundations Workshop}, pages 49--63.

\bibitem[Kiselyov et~al.(2005)]{kiselyov2005}
Kiselyov, O., Shan, C.-c., Friedman, D.~P., and Sabry, A. (2005).
\newblock Backtracking, Interleaving, and Terminating Monad
Transformers.
\newblock In \emph{Proceedings of ICFP 2005}, pages 192--203. ACM.

\bibitem[Lens(2024)]{lens2024}
Mirantis, Inc. (2024).
\newblock Lens: The Kubernetes IDE.
\newblock \url{https://k8slens.dev/}.

\bibitem[Nickel(2024)]{nickel2024}
Tweag and the Nickel Contributors (2024).
\newblock Nickel: Better Configuration for Less.
\newblock \url{https://nickel-lang.org/}.

\bibitem[Nielsen(1994)]{nielsen1994}
Nielsen, J. (1994).
\newblock \emph{Usability Engineering}.
\newblock Morgan Kaufmann.

\bibitem[NIST NVD(2024)]{nvd2024}
National Institute of Standards and Technology (2024).
\newblock National Vulnerability Database API 2.0.
\newblock \url{https://nvd.nist.gov/developers/vulnerabilities}.

\bibitem[OCI(2024)]{oci2024}
Open Container Initiative (2024).
\newblock OCI Image Specification v1.1 and Runtime Specification v1.2.
\newblock \url{https://opencontainers.org/}.

\bibitem[OPA(2024)]{opa2024}
Open Policy Agent Project (2024).
\newblock Open Policy Agent: Policy-based Control for Cloud Native
Environments.
\newblock \url{https://www.openpolicyagent.org/}.

\bibitem[Ou et~al.(2005)]{ou2005}
Ou, X., Boyer, W.~F., and McQueen, M.~A. (2005).
\newblock A Scalable Approach to Attack Graph Generation.
\newblock In \emph{Proceedings of the 13th ACM Conference on Computer
and Communications Security}, pages 336--345.

\bibitem[Phoenix(2024)]{phoenix2024}
Phoenix Framework (2024).
\newblock Phoenix: Peace of Mind from Prototype to Production.
\newblock \url{https://www.phoenixframework.org/}.

\bibitem[Podman(2024)]{podman2024}
Containers/Podman Project (2024).
\newblock Podman: A Tool for Managing OCI Containers and Pods.
\newblock \url{https://podman.io/}.

\bibitem[Portainer(2024)]{portainer2024}
Portainer.io (2024).
\newblock Portainer: Container Management Made Easy.
\newblock \url{https://www.portainer.io/}.

\bibitem[Racket miniKanren(2024)]{racketkanren}
Racket Community (2024).
\newblock Faster miniKanren for Racket.
\newblock \url{https://github.com/michaelballantyne/faster-minikanren}.

\bibitem[Rancher(2024)]{rancher2024}
SUSE (2024).
\newblock Rancher: Complete Container Management Platform.
\newblock \url{https://www.rancher.com/}.

\bibitem[ReScript(2024)]{rescript2024}
ReScript Association (2024).
\newblock ReScript: Fast, Simple, Fully Typed JavaScript from the
Future.
\newblock \url{https://rescript-lang.org/}.

\bibitem[Rust(2024)]{rust2024}
The Rust Project (2024).
\newblock The Rust Programming Language.
\newblock \url{https://www.rust-lang.org/}.

\bibitem[Rustler(2024)]{rustler2024}
Rustler Contributors (2024).
\newblock Rustler: Safe Rust Bridge for Creating Erlang NIF Functions.
\newblock \url{https://github.com/rusterlium/rustler}.

\bibitem[Scholefield and Shepherd(2019)]{scholefield2019}
Scholefield, S. and Shepherd, L.~A. (2019).
\newblock Gamification Techniques for Raising Cyber Security Awareness.
\newblock In \emph{HCI for Cybersecurity, Privacy and Trust},
pages 191--203. Springer.

\bibitem[SecGuru(2017)]{secguru2017}
Kazemian, P., Varghese, G., and McKeown, N. (2017).
\newblock Header Space Analysis: Static Checking for Networks.
\newblock \emph{IEEE/ACM Transactions on Networking}, 25(4):2345--2358.

\bibitem[Sentinel(2024)]{sentinel2024}
HashiCorp (2024).
\newblock Sentinel: Policy as Code Framework.
\newblock \url{https://www.hashicorp.com/sentinel}.

\bibitem[Sysdig(2025)]{sysdig2025}
Sysdig, Inc. (2025).
\newblock \emph{2025 Container Security and Usage Report}.
\newblock \url{https://sysdig.com/2025-container-security-report/}.

\bibitem[Yacht(2024)]{yacht2024}
SelfhostedPro (2024).
\newblock Yacht: A Web Interface for Managing Docker Containers.
\newblock \url{https://yacht.sh/}.

\end{thebibliography}

\end{document}