CoCon: A Conference Management System with Formally Verified Document Confidentiality

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

system and security claim

CoCon verifies the functional kernel of a conference-management system in Isabelle/HOL, generates a functional implementation, and wraps it in a web application. The paper’s architecture “consists of a verified kernel and some trusted components” (Sec. 1, p. 322). It proves confidentiality, safety, and traceback properties for an input/output automaton. The running confidentiality properties bound what groups of users can learn about papers, reviews, discussions, and decisions.

technique 1: model the application as an I/O automaton

Use this when security depends on histories of requests, outputs, and secrets rather than on isolated functions. Define a state type, action type, output type, initial state, and deterministic step : State → Act → Out × State; a transition records source, action, output, and target. Define valid traces as lists of transitions whose sources and targets connect. Define observation O (what the attacker sees), secret sequence S, and trigger T (when a release bound stops applying). The authors require the model to identify “what the capabilities of the attacker are; which information is (potentially) confidential; which flows are allowed” (Sec. 3.2, p. 328).

Inference: in Verus, model the kernel state and actions as Rust datatypes, give spec fn step and spec fn valid_trace, and state safety with ensures over traces. Keep the executable API separate from the ghost trace model. Verus can prove inductive state invariants, but the paper’s relational trace theorem needs explicit ghost sequences and lemmas.

technique 2: bounded-deducibility security

Use bounded deducibility when some information may be released after a documented event, unlike absolute noninterference. Choose a relation B on original and alternative secret sequences. For every valid original trace with no trigger, and every alternative secret sequence related by B, prove there exists a valid alternative trace with the same observations and that alternative secret sequence. The paper states: “If trigger T never holds, then attacker O can learn nothing about secrets S beyond B” (Sec. 3.2, p. 328). In expanded form, keep observations synchronized while allowing the bounded secret difference; the resulting property is universally quantified over the original trace and alternative secrets and existentially quantified over the alternative trace.

Step by step: (1) define O, S, B, and T; (2) state the universal/existential trace property; (3) instantiate B for each document and workflow phase; (4) prove the property using the unwinding method below; (5) separately prove safety and traceback properties. Inference: a Verus encoding can use spec fn bd_secure over finite Seq traces and proof fn lemmas; quantifier-heavy existence proofs may need carefully chosen finite trace representations and solver guidance.

technique 3: game-like unwinding

Use unwinding to turn the trace existence proof into local transition obligations. Maintain a configuration (σ1, sl1, σ2, sl2) containing the current states of original and alternative traces and the remaining secret sequences. The opponent extends the original trace by one transition. The prover either ignores an unobservable transition or matches an observable transition in the alternative trace, preserving equal observations and consuming the next required secret. The paper explains: “The game starts with a pair of sequences of secrets, related by the bound B” and “Each time we, the Green, can choose between two options: (1) asking the opponent to move and then performing a Reaction, which can be either Ignore or Match, and (2) taking Independent Action” (Sec. 4.1, pp. 337–338). Prove an unwinding relation is initialized at the initial state, closed under reaction and independent-action rules, and has an exit rule when the required secrets are exhausted. The unwinding theorem then yields BD security.

Inference: in Verus, represent the relation as a spec fn over states and ghost sequences; prove closure with proof fns and requires/ensures. Do not write invariant(...) as a call or use modifies; loop invariants belong on the loop, and state mutation is described by Verus function contracts.

technique 4: compositional and sequential unwinding

A monolithic relation becomes difficult as the workflow grows. Split it into a network of relations. Each component may unwind to a set of continuation relations; prove each local unwind_to obligation and an initialization relation. The paper’s Corollary 5 says: “If we verify a condition as above for each component relation, we obtain an overall secure system” (Sec. 4.2, p. 342). For CoCon, relations follow conference milestones such as phase changes, paper registration, chair or reviewer registration, and review updates. A sequential network allows a relation to loop to itself, move to the next phase relation, or exit. Steps: identify workflow milestones; define one relation per phase; prove continuation and exit obligations; apply the compositional theorem.

Inference: Verus can encode each relation as a separate predicate and prove a chain of lemmas, allowing agent-written proofs to be checked per phase. The relation network is a proof decomposition; it does not automatically compose unverified API code.

implementation, evidence, and limits

The verified Isabelle kernel is translated to a functional language and wrapped by an API and GUI. The authors deployed CoCon to two conferences with approximately 70 and 110 users (Sec. 5.3, p. 347). The API, identity management, browser, Redis snapshots, and code generator remain trusted. “This trusted component is of course critical to the overall confidentiality guarantees, and is outside the scope of our verification” (Sec. 5.2, p. 347), referring to password hashing and authentication-token management. Deployment exposed a thread-unsafe API race that mixed users’ authentication tokens; it took 3.5 days to investigate and fix (Sec. 5.3, pp. 347–348). Thus the formal result covers the kernel under the stated identity assumptions, not end-to-end confidentiality. Inference: for VeruLaw, the key threat is a verified core surrounded by unverified wrappers, authentication, persistence, or serialization that violate the core’s state and identity assumptions. The paper already demonstrates phase-specific unwinding and compositional proof infrastructure; VL should reuse that pattern rather than redo a generic noninterference theorem.

techniques for the catalog

• i/o automaton security model — represent state, actions, outputs, observations, secrets, and valid traces explicitly
• bounded deducibility — permit only relation-bounded secret release until a trigger event
• unwinding game — maintain paired states and remaining secret sequences with ignore, match, and independent moves
• compositional unwinding — split workflow proofs into milestone relations linked by continuation and exit obligations Checked 2026-10-14 against the paper by a Codex agent: audit record popescu2020cocon; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15