vCause: Efficient and Verifiable Causality Analysis for Cloud-based Endpoint Auditing

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

The paper presents VCAUSE, a cloud auditing system that lets a remote administrator check both the point-of-interest node selected by a causality query and the node’s backward and forward causal components. The cloud is assumed to have Byzantine faults: it can “(i) manipulate system event logs by inserting, modifying, or deleting arbitrary data; and (ii) return incomplete, outdated, or falsified causality analysis results” (§3.1, PDF p. 3581). The system combines a graph accumulator for node-query proofs with a verifiable versioned provenance graph for path proofs. The paper states: “V C AUSE integrates two authenticated data structures: a graph accumulator and a verifiable provenance graph.” (Abstract, PDF p. 1 / proceedings p. 3579.)

technique: versioned provenance graph

What it is. A conventional provenance graph has entities as nodes and dependencies as edges but lacks temporal order. VCAUSE creates a new version node whenever an entity changes state, adding a temporal and a dependency edge. Definition 1 starts with a node query N(s, ⪯ t) that selects the version of entity s whose creation time is the nearest one at or before t (§3.2, PDF p. 3581); §4.2 adds the relation ⪰ t, the nearest timestamp at or after t (PDF p. 3583). Backward and forward components are the nodes and edges on all paths into and out of the selected node, extracted by backward and forward depth-first searches; the paper formulates this as a subgraph query (Definition 1, §3.2, PDF p. 3581).

When to use it. Use this representation when an event stream needs causal analysis whose answer must preserve event time and be independently checked. The paper’s system targets endpoint logs and cloud analysis; it says: “versioned provenance graphs [40] encode event sequences by creating a new version of an entity whenever its state changes.” (§2.1, PDF p. 3581.)

How to apply it, from the paper. (1) For every system event, create a node for the new version of the affected entity (§2.1). (2) Add a temporal edge and a dependency edge that capture the temporal and causal relations (§2.1); each node connects to two predecessors via these edges (§5.3, PDF p. 3585). (3) Compute the node’s incoming and outgoing path digests described below on creation and update the digests of affected ancestors (§6, PDF pp. 3586–3587). (4) Answer the entity/time query and run backward and forward depth-first searches (§3.2). (5) Return the selected node’s proof, its component nodes and edges, and the path digests (§6).

Verus form. Inference: represent a node and edge as Rust structs, and represent the mathematical graph and path relation with spec fns over ghost sequences or maps. Put the query result and graph-consistency promises in requires and ensures; use loop invariant clauses for DFS visited-set, edge-membership, and digest-preservation facts. Inference: the paper’s cloud protocol and cryptographic hashes do not become executable Verus specifications automatically; a Rust implementation must prove that its concrete graph operations refine the ghost graph.

Evidence and limits. The paper evaluates graphs built from StreamSpot and DARPA OpTC. Table 1 reports 600 StreamSpot endpoints (average 149K events, 149K nodes, 290K edges) and 1,000 OpTC endpoints (average 17M events, 17M nodes, 32M edges) (§8, PDF p. 3587). The paper argues that a node’s incoming edges capture its creation history, which is immutable, so the node “cannot receive new incoming edges” and its incoming digest stays unchanged (§5.1, PDF p. 3584). Inference: mutable historical edges, dropped event records before commitment, or a mismatch between logger semantics and the graph model can invalidate the intended evidence.

technique: hierarchical indexed Merkle graph accumulator

What it is. A single indexed Merkle tree supports only single-keyword queries, but a node query has two keywords (entity ID and timestamp). VCAUSE uses one indexed Merkle tree per entity, indexing version nodes by timestamp, and a global Merkle tree whose leaves are the local-tree roots indexed by entity ID (§4.1, PDF pp. 3582–3583). Each internal node records the minimum and maximum keywords in its subtree, enabling binary search. The global root is a cryptographic commitment to the entire graph (§4.1, PDF p. 3583).

How to generate and validate a membership or non-membership proof. (1) Search the global tree exactly for entity s; the sibling nodes on the search path form ρG (§4.2, PDF p. 3583; Algorithm 1, Appendix A.1, PDF p. 3595). (2) Search that entity’s local tree with ⪯ t or ⪰ t; the sibling nodes form ρL. (3) Return (ρG, ρL) and the matched node; for non-membership, the proof holds only ρ̃G if no node matches s, or ρ̃G and ρ̃L if s exists but no node satisfies the relation (Appendix A.1, PDF p. 3596). (4) The verifier reconstructs the search path and tree structure from the proofs. (5) The proof is valid if the reconstructed root matches the committed root; membership holds if the node lies in entity s’s local tree and satisfies the relation, and non-membership holds if no such node is found (§4.2, PDF p. 3583). The paper gives the reason for the two-level proof: “By combining the proofs from both levels, our accumulator can produce complete proofs for any node queries.” (§4.1, PDF p. 3583.) Appendix A.2 adds entity-temporal range proofs (ρG, (ρlL, ρrL)), which reduce verifying m nodes from O(m log N) to O(m) (PDF p. 3596).

Verus form. Inference: model each tree node with a spec fn hash summary and min/max bounds, and state a function contract that a returned path reconstructs the committed root and satisfies the query relation. A proof fn can establish that combining sibling summaries preserves the root; assert steps can discharge bound cases. Inference: SHA3 and ECDSA remain cryptographic primitives with trusted specifications or verified wrappers; Verus does not prove their cryptographic security from these paper results.

Evidence and limits. The implementation uses SHA3-256 for the accumulator and signs the Merkle root with ECDSA (§8, PDF p. 3587). Theorem 1 assumes an EUF-CMA-secure signature scheme, a position-binding Merkle tree structure, and causality relation unforgeability of the provenance graph (§7, PDF p. 3587). Inference: non-membership only means no matching node exists in the committed tree; it does not recover logs never included in that commitment.

technique: dynamic indexed Merkle tree (DIM-Tree)

What it is. Graph nodes arrive continuously, and in a conventional tree each insertion “may require updating the hashes of numerous affected nodes” (§4.3, PDF p. 3584). DIM-Tree stores multiple perfect binary subtrees. Each new node is a height-1 subtree merged recursively with preceding subtrees from right to left; only affected internal hashes are updated. The insertion algorithm is Algorithm 3 (Appendix B, PDF p. 3596). The paper states O(1) amortized time per insertion and O(log Nsb) update cost, where Nsb is the subtree size, smaller than the total size N (§4.3, PDF pp. 3583–3584).

How to apply it. (1) Append the new leaf to the leaf vector. (2) While the stack top has the same height as the new subtree, merge them with TreeMerge, increment the height, and pop the stack top. (3) Push the resulting subtree root (Algorithm 3). (4) For a changed node, recompute hashes of internal nodes on its path to the root of its subtree. (5) To finalize, merge subtree roots right to left into the overall root; in the accumulator, finalize local trees first, then the global tree (§4.3, PDF p. 3584).

Verus form. Inference: implement the stack and merge loop in executable Rust; specify that the stack represents a binary-counter decomposition of the inserted prefix. Use a loop invariant relating each stack height to its subtree size and a decreases measure for the merge loop. A proof fn can prove that TreeMerge preserves the Merkle summary. Inference: O(1) amortized complexity is a cost claim, not a functional postcondition; it needs a separate resource or operation-count model.

Evidence and limits. On one OpTC endpoint’s 25-million-node graph, inserting 25 million nodes took about 14 seconds, about 0.57 µs per insertion, and the DIM-Tree accumulator was “significantly faster” than a Merkle B+ tree baseline; its update time was “slightly lower” (Figure 11, §8.1, PDF p. 3588). The machine is an Ubuntu 22.04 PC with 4 Intel Xeon 3.60GHz processors and 32GB RAM (§8, PDF p. 3588). Inference: this single-dataset measurement does not establish the same constant for all workloads.

technique: incoming path digest for backward-causality proof

What it is. For an entry node, set ΠI = H(∅). For each other node, set ΠI to the hash of the set of pairs, each an incoming edge’s string representation concatenated with that edge’s source ΠI (Equation 3, §5.1, PDF p. 3584). The digest therefore commits recursively to every node and edge on incoming paths. To validate, recursively hash the supplied components from entry nodes and compare with the node’s original digest (§5.2, PDF p. 3584). Algorithm 4 (Appendix C, PDF p. 3597) does this by DFS: its recursion returns early if an incoming edge or its source is not in the supplied set, and Main returns True only if the recomputed ΠI equals the original.

How to apply it. (1) Encode each edge s(e) by concatenating the associated nodes’ fields and event data (§5.1). (2) Initialize entry-node digests to H(∅). (3) For each newly created node, hash incoming edge encodings and predecessor digests. (4) In validation, DFS from the queried node over incoming edges, checking that every traversed edge and source belongs to the supplied component. (5) Recompute and compare ΠI (Algorithm 4).

Verus form. Inference: define a recursive spec fn for the incoming digest over a ghost graph and a proof fn that the DFS result equals that specification. Use requires to require acyclic or visited-safe traversal and ensures to state digest equality. Inference: the paper’s second-preimage argument can be represented as an assumption about the hash function; it is not a Verus proof of SHA3 second-preimage resistance.

Evidence and limits. Theorem 2 (Appendix D.1, PDF p. 3597) states causality relation unforgeability “if the used hash function is second-preimage resistant.” The digest relies on the incoming history being immutable after node creation (§5.1). Inference: Algorithm 4 as printed does not show how its early return on a missing edge or source makes Main return False; an implementation must make that case reject explicitly.

technique: outgoing and segmented outgoing path digests

What it is. Outgoing digests reverse the direction: an exit node has ΠO = H(∅), and each node hashes its outgoing-edge encodings with successor ΠO (Equation 4, §5.3, PDF p. 3585). VCAUSE uses ordering-invariant incremental hashing to add or subtract only changed components (Equations 5–6, §5.3, PDF p. 3585). Because each node has two predecessors, paths of length L mean adding a node may affect 2^L ancestors (§5.3, PDF p. 3585). VCAUSE therefore segments the graph. Temporal edge segmentation replaces each temporal edge’s destination with a terminal node that has no outgoing edges and points to the original destination, turning the graph into trees; deep tree segmentation moves a dependency edge that makes a tree’s depth exceed L, with its connected nodes, into a new tree (§5.4, PDF pp. 3585–3586).

How to apply it. (1) Initialize a new node’s outgoing digest to H(∅). (2) Add the new component digest to each immediate predecessor with homomorphic hash addition (Equation 5). (3) Recursively update earlier ancestors, subtracting the old child contribution and adding the new one (Equation 6). (4) Detach temporal edges into terminal nodes. (5) If a dependency edge would exceed depth L, move it and its connected nodes into a new tree, put a terminal node at the old position, and update the affected nodes’ segmented digests in the old and new trees (§5.4, PDF p. 3586). (6) During validation, check the initial tree using its segmented digest, validate later tree roots with accumulator node proofs (optionally batched with temporal range proofs), and check each root’s remaining components (§5.5 and Figure 9, PDF p. 3586; Algorithm 5, PDF p. 3597).

Verus form. Inference: model each tree’s digest and terminal-node rule in spec fns, and prove update equations with proof fns over a ghost map of child contributions. Use loop invariants for DFS and a decreases bound on traversal. Inference: incremental hash addition and subtraction require a trusted algebraic specification of the chosen hash; Verus cannot infer homomorphic cryptographic behavior from an implementation without such a contract.

Evidence and limits. The paper states that segmentation reduces the update overhead “to linear complexity O(L), where L is the predefined tree segmentation depth” (§5.4, PDF pp. 3586–3587). A single segmented digest is “insufficient for validating its complete causality relations” (§5.5, PDF p. 3586). Figure 12 measures depths 1, 2 and 16 for update time and 1, 4 and 16 for forward proof and validation; the paper finds depth 1 “offers the best trade-off” (§8.2, PDF pp. 3589–3590). The security proof in Appendix D.2 covers unsegmented outgoing digests and states that the analysis “naturally extends to the segmented setting” without proving it (PDF p. 3598).

technique: signed commitment and four-phase protocol

The endpoint logger periodically commits node changes into the accumulator’s Merkle trees, signs the root R with the current timestamp t, and sends (R,t,σR) with event logs to the cloud (§6, PDF p. 3587). The cloud reconstructs both authenticated structures from the logs, answers a query, and returns the node proof, path digests, and node proofs of segmented tree roots. The administrator verifies the signature, the node proof, and the incoming and (segmented) outgoing digests. The four named phases are Event Recording, Commitment, Causality Analysis Proof, and Causality Analysis Validation (§3.3, PDF p. 3582).

Verus form. Inference: expose each phase as a Rust function with requires/ensures contracts linking the signed root, reconstructed graph, and returned proofs. Keep cryptographic signing and verification behind a separately specified API; do not mark the function being verified with external_body. Inference: a Verus proof can establish protocol-state consistency under the contracts, while signature unforgeability and endpoint/cloud behavior remain assumptions.

Evidence, trust, and product threat. The security game lets an adaptive adversary add, delete, or modify components in causality analysis results. Theorem 1 states unforgeability if the signature scheme is EUF-CMA-secure, the Merkle tree structure is position-binding, and the provenance graph upholds causality relation unforgeability (§7, PDF p. 3587). The prototype has 3,500 lines of C++ using OpenSSL 1.1.1w (§8, PDF p. 3587). The paper reports 25 million logs processed in 2 minutes and a proof for a 100,000-node causality analysis in 49 ms (§1, PDF p. 3580; §8.3, PDF p. 3590), and less than 1% overhead on endpoints and 3.36% on the cloud (Abstract, PDF p. 3579). The 3.36% figure is the average forward-proof-generation overhead over 1,000 random queries against a baseline without validation (Figure 14, §8.4, PDF p. 3591); backward proof generation is 8.92%. With auditd as the logger, Table 3 (Apache Bench, 10,000 requests, 10 threads) reports 0.11% for Apache2 and 0.10% for Nginx, and 0.35% for seven NAS Parallel Benchmarks programs (§8.4, PDF p. 3591). Table 4 reports authenticated-data-structure storage overhead of 19.81% on StreamSpot and 6.98% on OpTC, per endpoint (§8.5, PDF p. 3591).

The paper proves unforgeability under the assumptions above and reports performance measurements. It says it builds “upon existing log protection schemes” for endpoint-side log collection (§3.1, PDF p. 3581). Inference: the result also trusts endpoint event capture, the graph reconstruction code, the cryptographic libraries, operating system and compiler, and the adequacy of the causality specification; the paper verifies none of these. Inference: for agent-written verified Rust, this is a high threat to any product claim that a cloud-returned provenance result is complete or untampered; the reusable idea is proof-carrying authenticated state, while the paper does not verify Rust memory safety or the logger implementation. Inference: VL should reuse the decomposition into query proofs, path-digest proofs, and signed commitments, and should avoid redoing generic Merkle-tree or hash-proof research unless it targets Verus-specific APIs, contracts, or end-to-end logger refinement. The paper’s evaluated system is C++, not Verus, and no experiment measures agent-generated code.

techniques for the catalog

• versioned provenance graphs — create immutable entity versions with temporal and dependency edges so causal queries have a time-aware graph
• hierarchical indexed Merkle proofs — combine global entity search and local fuzzy-time search to prove node membership or non-membership
• DIM-Tree insertion — maintain a stream-friendly Merkle accumulator with subtree merges and constant amortized insertion
• incoming path digests — recursively hash predecessor paths to prove backward causal components
• incremental outgoing digests — update successor-path commitments by homomorphic add/subtract of changed components
• segmented outgoing trees — cap dependency depth and use terminal nodes plus root proofs to make forward validation update-efficient
• signed four-phase protocol — record events, sign roots, generate query/path proofs, and independently validate the result Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “To evaluate its efficiency, we use data from an endpoint in the larger dataset (OpTC), yielding a versioned provenance graph with 25 million nodes.”): checked every quotation, number, section and page reference, and technique step against the paper text; changed the link to the publisher page from the paper text, replaced the threat-model paraphrase with the paper’s words, corrected page references (§2.1, §4.1, §4.3, §5.3, §8.1, Algorithms 4–5, Figure 14, Table 3), fixed the Algorithm 4 and deep-tree-segmentation descriptions, added the segmented-proof gap in Appendix D.2 and the tested depths, and marked unsupported conclusions as Inference; did not check figure plots beyond their captions and text, or the paper’s cited works.

Last edited: 2026-10-16