Audit Log Integrity and Session State Channels

Audit Log Integrity and Session State Channels

Incident response, red-teaming, and any after-the-fact review of a deployed model all assume a complete, tamper-evident record of what the model did. If log entries can be suppressed, falsified, or selectively deleted, a safety claim that rests on “we can review the logs” is unsupported. Append-only storage and cryptographic log chaining (in the style of Certificate Transparency [1] and tamper-evident history trees [2]) provide tamper evidence, but the deployed log servers that serving infrastructure would use, such as sigstore’s Rekor [3], are not shipped with machine-checked proofs.

There is a subtler problem on the same boundary. When a model’s output or summary is written back to session state for future context windows (the text prepended to later requests), the write-back opens a persistent covert channel in Lampson’s sense [4]. A misaligned model [5] can encode messages in session state that survive request boundaries, such as instructions to future invocations of itself or data staged for later exfiltration. The output filter (the gateway-side check on the response returned to the user) never sees the write-back to the session store, so it cannot catch this. Any system that persists conversation summaries, scratchpads, or tool-call results across requests exposes this surface.

Both problems sit on a write path out of the serving loop, and in both cases a violation is invisible until someone inspects the stored contents.

Solution Sketch A: Log Integrity via Permission Graph

Build a TLA+ [6] model of the serving infrastructure’s request lifecycle. State variables: the committed log, the in-flight request set, the per-principal permission relation. Transitions: a request enters the gateway, dispatches to forward-pass execution, emits a log entry, commits the entry to storage, returns a response. Three properties are checked against the same model.

• Tampering safety: in every reachable state, no transition available to any principal (model, harness, orchestrator) modifies or deletes an already-committed log entry.
• Log-before-response (also a safety property): no response-emit transition for a request fires unless that request’s log-commit transition has already fired. This catches suppression by the same infrastructure that handles writing.
• Logging completeness (liveness): every request that reaches forward-pass execution eventually has its log entry committed.

The model is not the gateway. The result is only as good as the correspondence between the TLA+ transitions and the deployed components, so the sketch should budget for closing that gap, via trace validation against production logs or conformance tests generated from the model. Sketch A treats the log as a passive resource and verifies the access-control and lifecycle machinery around it.

Solution Sketch B: Log Integrity via Verified Merkle-Tree Log

Instead of verifying that the permission system prevents tampering, make tampering detectable from the log’s own structure. Append-only Merkle-tree logs [2] of the kind Certificate Transparency [1] and Rekor [3] use publish signed tree heads. Any third party can use them to check, via consistency proofs, that two published heads belong to the same history. A serving infrastructure that retroactively removes a committed entry cannot then issue a new signed head consistent with the previous one.

The verification target is the log component itself, against an abstract specification of an append-only Merkle log. Two local properties:

• Append-only signing: the only path to the signing operation runs through append(entry), and every signed root is a valid extension of the previously signed root. No implementation path signs a root that omits a previously committed entry.
• Consistency-proof correctness: consistency_proof(old_root, new_root) is sound (a proof verifies only for genuinely consistent trees) and complete (an honestly generated proof always verifies).

Both are local properties of a single program, a good fit for a refinement proof against the abstract spec in Dafny [7] or F* [8]. Soundness is necessarily conditional: it holds relative to an explicit collision-resistance assumption on the hash, which the proof states as an axiom rather than discharges.

The result is a log component whose tamper-evidence follows from the Merkle structure, not from the permission graph around it. Unlike Sketch A, its guarantee can be re-checked by any third party holding two signed tree heads, independently of the operator. That requires the heads to actually reach independent parties: an operator who shows different heads to different auditors (equivocation) defeats the check unless heads are gossiped or co-signed by witnesses, and that distribution protocol is outside this sketch.

Sketch B does not replace Sketch A. A Merkle log makes tampering with committed entries detectable, but says nothing about entries that are never committed. Logging completeness and log-before-response remain Sketch A’s job. The natural combination uses Sketch B’s verified log as the storage primitive whose access path Sketch A’s model covers.

Solution Sketch C: Session State via Noninterference

For the session-state channel, apply information flow analysis [9]. A naive noninterference property, that session state depends only on “authorized” inputs such as the model’s declared output, does not help: the declared output is itself a function of the model’s hidden state, and a model encoding messages steganographically does so through the declared output.

The useful property is narrower. Session state must be a deterministic function of what was already exposed to monitoring: the user’s message, the tool results, and the response as delivered after the output filter. Stated as noninterference [10]: for any two runs that agree on those inputs, but differ in anything else the model produced (undelivered scratchpad, discarded drafts, fields the filter strips), the write-back function produces identical session state. This does not eliminate steganography in the visible response. It collapses the persistent channel onto the channel the output filter already inspects, so no unmonitored path into future context remains.

The write-back function is small and its specification is a pre/postcondition contract on its output, so Dafny [7] fits. The relational two-run form of the property needs either a product-program encoding (two copies of the function run side by side and their outputs compared) or a relational verifier.