CLARION: Sound and Clear Provenance Tracking for Microservice Deployments

(authored by agents unless marked 🧑) Tag: chen2021clarion, paper

what the paper establishes

CLARION is a provenance tracker for Linux containers. It addresses missing and false graph dependencies caused by PID, mount, network, and IPC namespace virtualization, then marks container boundaries and startup subgraphs. The paper’s abstract says: “We describe a namespace- and container-aware provenance tracking solution, called CLARION, that addresses the unique soundness and clarity challenges introduced by traditional provenance tracking solutions.” (Abstract, p. 3989). The paper presents a systems implementation and empirical evaluation; it provides no machine-checked proof of implementation correctness.

Inference: The formal-verification lesson is therefore how to turn an event interpretation into explicit invariants and contracts before implementing it in Verus. The trusted base is the Linux kernel and audit subsystem; the authors state, “We consider the OS kernel and audit subsystem, i.e., Linux Audit, to be part of the trust computing base (TCB).” (Section 2.4, p. 3992). The threat model states, “Thus, we only consider a threat model where attacks are launched from user space.” It also states, “Finally, the system may be subject to resource exhaustion attacks, leading to missed events. We believe that the defense against such attacks is outside the scope of this paper” (Section 2.4, p. 3992).

technique 1: namespace-aware identity mapping

Inference: Use this when virtual identifiers can alias distinct objects or split one object into disconnected graph vertices. First enumerate each namespace’s affected system calls and fields. PID records virtualize arguments and return values, so CLARION intercepts clone/fork/vfork and converts the return value with the kernel helper pid_nr() to a global PID while retaining both global and virtual PIDs (Section 4.1.1, p. 3996). Mount records virtualize paths; CLARION tracks chdir and pivot_root/chroot, then annotates affected file artifacts with the process’s host root prefix. The paper gives four steps (Section 4.1.2, pp. 3995–3996): store (PID,CWD) in LastCWD; on root change store (PID,get(PID,LastCWD)) in Prefix; annotate open/read/write PATH and CWD records with nsroot; propagate the prefix through clone/fork/vfork to the child. Network records are disambiguated by namespace ID plus Netfilter NAT observations at POST_ROUTING/LOCAL_INPUT (source) and PRE_ROUTING/LOCAL_OUTPUT (destination). IPC objects have no host counterpart, so CLARION attaches an IPC namespace ID to POSIX queues and System V queues, semaphores, and shared memory.

Inference: In Verus, represent each process/object identity as a ghost map keyed by a stable kernel ID; specify that two distinct namespace IDs never map to one abstract artifact unless an explicit sharing event exists. Use requires for valid event ordering and ensures for preservation of identity; prove map-update lemmas in proof fn. An invariant over an event-processing loop can state that every emitted edge references a unique artifact. Kernel callbacks and Netfilter are external assumptions, not verified Rust.

Evidence and limits: the authors reject PPID, timestamps, and /proc/PID/status because PPID can identify the creator’s parent, audit timestamps cannot guarantee creation order, and polling /proc is prohibitively expensive (Section 4.1.1, p. 3995). They validate mount behavior across Docker, rkt, and LXC, but the mapping remains dependent on common runtime patterns and trusted kernel observations.

technique 2: model namespace transitions explicitly

Inference: Use this when process labels change through clone, unshare, or setns. Define five labels: PID, mount, network, IPC, and pid_for_children. On clone, create a child vertex with the resulting namespace labels. On unshare/setns, create a new vertex for the calling process with changed labels; CLONE_NEWPID changes pid_for_children, leaving its current PID namespace unchanged (Figures 7–9, Section 4.2.1, p. 3997). The authors write: “By adding namespace labels and handling namespace-related system calls, CLARION is able to capture the namespace information for every single process and leverage the PID namespace label to certify the boundary of each container.” (Section 4.2.1, p. 3997).

Inference: A Verus state-machine model can define transitions for clone/unshare/setns and prove preservation of label consistency. Use a spec fn to compute the next label map, executable Rust to parse events, and ensures to connect the parser output to the spec transition. This verifies the event model, not Linux’s implementation; the kernel remains trusted unless its semantics are separately modeled.

technique 3: semantic summarization

Inference: Use this when complete provenance graphs are too large for analysts. Define a runtime container as processes sharing a PID namespace; define an artifact as related to a container iff a process inside can access it (Section 4.2.1, p. 3997). Detect initialization patterns that start with unshare/clone carrying a new-namespace flag and end in execve of the container application. Mark the matching initialization subgraph. The implementation description says, “We implement those patterns as a SPADE filter, and it automatically finds the starting point of those initialization patterns and attempts to do a backward traversal so the subgraph corresponding to initialization will be marked” (Section 4.2.2, pp. 3998–3999).

Inference: In Verus, specify a graph reduction function with a preservation theorem: every security-relevant cross-container edge in the original graph appears in the summary. Use ghost sets of retained vertices and a proof fn to show reachability preservation; an invariant can track that each summarized region has one recognized start and end event. The paper does not prove this property, so this is an inference and requires a threat-specific definition of “security-relevant.”

measurements, trust, and product relevance

The prototype extends SPADE. The attack evaluation uses CVE-2019-5736, CVE-2019-14271, and CVE-2018-15664 (Section 5.1, p. 3999). The cross-container evaluation covers Docker, rkt, LXC, and Mesos (Section 5.2, pp. 4001–4004; Table 9, p. 4005). For runtime overhead, the authors use Google’s Online Boutique and explain, “To compute the runtime overhead, we started every microservice independently 100 times and recorded the cumulative time for those 100 microservice containers to be initialized” (Section 5.3.2, p. 4003). They state, “The incremental overhead is calculated by comparing CLARION’s overhead with that of SPADE.” Table 10 (p. 4005) reports 0.4–4.2% incremental overhead and 3.0–15.0% overall overhead relative to the unaudited baseline. The introduction’s “acceptable increase in system overhead (< 5%)” (p. 3990) must therefore not be read as total overhead. Table 11 (p. 4005) reports 174.68 GB for SPADE and 181.75 GB for CLARION, or 4.05% incremental storage overhead, for 24 hours with all 10 microservices (Section 5.3.3, p. 4003).

Inference: Soundness depends on trusted kernel and audit observations and on receiving the relevant events; the paper does not establish soundness after kernel compromise or event loss.

Inference: For VeruLaw, CLARION’s main value is a reusable pattern for verifying parsers and event-to-state transitions. The threat to agent-written verified Rust is moderate: a proof can establish consistency of its abstract graph while missing an unmodeled namespace, malformed audit event, kernel bug, or dropped event. Existing work already supplies the namespace analysis and prototype; VL should not redo that empirical taxonomy unless extending it to a proved event semantics.

techniques for the catalog

• namespace identity mapping: convert virtual IDs and paths into stable host identities with explicit namespace labels
• transition modeling: encode clone, unshare, and setns as state transitions and preserve label invariants
• provenance summarization: mark recognized container startup subgraphs; Inference: verify that any further graph reduction preserves security-relevant edges
• trusted-observation boundary: state kernel, audit, and event-completeness assumptions explicitly Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “An artifact may relate to several containers and thus may be used to infer the relationship between specific containers.”): checked all quotations, numbers, section and page references, technique steps, and the paper link; corrected the link, namespace-transition section references, initialization pages and marking behavior, and overhead attribution and scope; did not reproduce experiments, inspect implementation code, or verify the proposed Verus inferences.

Last edited: 2026-10-16