🤖 AI

Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI

This paper presents a machine-checked correction of a 2018 framework for epistemic semantics of information flow policies, achieved with the assistance of an agentic AI coding assistant, to provide a robust and general foundation for specifying and enforcing expressive security requirements.

Original authors: David A. Naumann

Published 2026-08-04

📖 6 min read🧠 Deep dive

CC BY 4.0

Original authors: David A. Naumann

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The Secret Keepers and the Digital Whisper

Imagine a world where every computer program is a bustling city, and information is the currency flowing through its streets. In this city, some secrets are so valuable—like a master key or a password—that they must never leave a specific vault. This is the realm of information flow security, a branch of computer science dedicated to ensuring that sensitive data doesn't accidentally (or maliciously) leak out to the wrong eyes. But life isn't always black and white. Sometimes, a secret needs to be shared, but only under very specific conditions. Maybe a bank wants to tell a customer their account is safe, but only after they've answered a security question correctly. This tricky balancing act is called downgrading: taking a high-level secret and carefully lowering its protection level so it can be seen, but only when the rules say it's okay.

To make sense of these complex rules, scientists use a branch of logic called epistemic logic. Think of this as the "logic of knowledge." Instead of just asking "What happened?", it asks "What does the observer know?" If a hacker is watching the city, what can they deduce about the secrets in the vault based on the traffic they see? The challenge has always been writing a perfect rulebook that says exactly when a secret can be shared without creating a loophole. For years, researchers tried to build a mathematical framework for this, but the blueprints kept having cracks. If the math is wrong, the security is an illusion.

Fixing the Blueprint with a Robot Assistant

This paper tells the story of how a researcher, David Naumann, teamed up with an artificial intelligence coding assistant to fix a broken blueprint for these security rules. The original blueprint, published in 2018, was a clever attempt to define exactly when a program is allowed to "declassify" a secret. It used a concept called relational annotations, which are like sticky notes placed on the code saying, "It's okay to show this secret if the random coin flip landed on heads." The idea was that if two different runs of the program agreed on the coin flip, they could agree on showing the secret.

However, when the original paper was presented, the author realized there was a significant flaw in their proof. It was like building a bridge that looked sturdy but collapsed under a specific type of wind. The author had sketched a correction, but the details were messy and unverified. This paper takes that sketch and turns it into a solid, unshakeable structure.

The main finding here is a machine-checked proof. The author didn't just write the math on paper; they fed it into a computer program called Rocq (a proof assistant) that acts like a hyper-attentive math tutor. This robot tutor checked every single step of the logic to ensure there were no hidden gaps. The result is a corrected framework that proves: if a program follows a specific set of "safety" rules (which are easy to check while the program runs), then it is mathematically guaranteed to be secure according to the complex "knowledge" rules.

The paper explicitly rules out the idea that the original 2018 proof was correct as written. It shows that the previous definition of "release policy" (the rulebook for when secrets can be shared) was flawed because it didn't account for all the ways a program could get stuck or diverge. The author argues that you cannot simply trust a human's intuition on these complex multi-run scenarios; you need the machine to verify every possibility.

The Detective and the Alibi

To understand how this works, imagine a detective (the security system) trying to figure out if a suspect (the program) is leaking secrets. The detective has two tools: Safety and Security.

Security is the ultimate goal: "The suspect didn't tell anyone anything they weren't supposed to know." This is hard to prove because you have to imagine every possible scenario the suspect could have been in.
Safety is a simpler, local check: "Did the suspect follow the rules step-by-step as they went?"

The paper's big breakthrough is proving that Safety implies Security. If the program follows the "Safety" rules (which are like a checklist of "alibis" for every step), then the complex "Security" guarantee automatically holds true. It's like proving that if a driver never runs a red light or speeds (Safety), they will never cause a specific type of accident (Security).

The author used an agentic AI coding assistant (specifically a tool called Claude Code) to help write the code for the Rocq proof. This wasn't just a spell-checker; the AI helped translate the messy mathematical sketches into rigorous code and even found some of the author's own mistakes. For instance, the AI pointed out that a definition for "divergence" (when a program gets stuck in an infinite loop) was too strict and needed to be relaxed to make the proof work. The AI also attempted to "make assumptions stronger than necessary," but the human author caught it and corrected the course.

The Result: A Verified Rulebook

The paper concludes that the corrected framework is solid. The machine-checked proof confirms that the original idea was on the right track, but the details needed a major overhaul. The new framework allows for a "release policy" that is clearly defined and separate from the security check itself. This means developers can write their code with "assume" statements (like "assume the user is logged in") and have a mathematical guarantee that these assumptions correctly control what secrets are revealed.

The author is very sure about this result because it has been machine-checked. This isn't a simulation or a suggestion; it is a formal proof that the logic holds up under the scrutiny of a computer. They admit, however, that the code is currently a bit messy and needs human cleanup to be truly readable, much like a brilliant but scribbled-on napkin that needs to be transcribed into a clean book.

In the end, this paper is a victory for precision. It shows that even in the abstract world of computer security, where logic can get incredibly tangled, we can use both human insight and AI assistance to build a foundation that is mathematically unbreakable. It turns a shaky sketch into a verified fortress, ensuring that when we decide to share a secret, we do so exactly when we mean to, and not a moment before.

Technical Summary: Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI

1. Problem Statement

High-level security requirements regarding information flow, particularly those involving selective downgrading (declassification), are notoriously difficult to formalize precisely. While epistemic logic has emerged as a promising framework for defining confidentiality (what an observer at a specific privilege level is permitted to know), a robust, general framework for expressive flow policies has remained elusive.

A prior work, referred to as CN (Naumann et al., CSF 2018), attempted to provide a unifying framework for reactive program models. In CN, policies were expressed via assume statements within the code, while the derived release policy was expressed solely in terms of input streams. However, the formalization in CN contained a significant flaw in its proof, announced during the conference presentation. The original definition of the release policy and the subsequent proof that safety implies security were sketchy and incorrect. Furthermore, existing machine-checked adaptations (e.g., Murray et al. for concurrent C programs) often rely on strong properties like constant-time execution, which trivialize the complexities of aligning multiple executions required for epistemic reasoning.

The core challenge is to provide a corrected, machine-checked formalization that:

Revises the epistemic semantics to correctly handle state-dependent downgrading.
Explicitly defines the semantics of a release policy derived from code annotations.
Proves that a program-oriented property called safety implies the epistemic security property.

2. Methodology

The author employs a formal verification approach using the Rocq proof assistant (formerly Coq). The methodology involves:

Program Model: A small imperative reactive language with input handlers for specific security levels. Programs consume input streams and produce outputs.
Annotations: The framework utilizes relational assertions (assert) and assumptions (assume) to specify information flow requirements. These annotations allow for conditional flows that deviate from the baseline non-interference policy.
Epistemic Semantics: Security is defined in terms of an observer's knowledge. An observer at level $\ell$ knows a set of possible input histories consistent with their visible observations (inputs and outputs at levels $\ell' \sqsubseteq \ell$ ).
Release Policy ( $RP_\ell$ ): Defined as the set of input lists an observer is allowed to learn, derived from the assume statements in the code. This policy is interpreted via alignments between a "major" pre-run (actual execution) and "minor" pre-runs (possible executions with different inputs).
Safety Condition: A program-oriented property defined by the absence of "failures" (assertion failures, alignment failures) or the presence of specific "fiats" (assumption fiats, divergence fiats) when comparing a major run against all possible minor runs.
Agentic AI Assistance: The formalization was developed with the aid of Claude Code, an agentic AI coding assistant. The AI was guided to translate LaTeX definitions into Rocq specifications and assist in constructing proofs, though it required significant human curation to correct logical errors, refine definitions, and manage the proof strategy.

3. Key Contributions

A. Corrected Epistemic Semantics

The paper presents a revised formalization of the epistemic semantics for flow policies. Key technical revisions include:

Release Policy Definition: The definition of the release policy $RP_\ell(gs)$ is corrected to be a predicate on pre-runs (finite execution prefixes) rather than just observed event traces. It is defined via semi-conformance: a relation between a major pre-run and minor pre-runs that aligns them at specific annotation points.
Progress-Insensitive Security: The framework adopts a progress-insensitive security definition. It utilizes a notion of progress knowledge ( $k_\ell^\to$ ) to handle divergence, ensuring that security guarantees hold even if the program diverges, provided the divergence itself does not leak information about hidden inputs.
Well-Specified Programs: The author introduces "boilerplate annotations" (assumptions at the start of handlers and assertions before outputs) to streamline the formalization and ensure that baseline policies are encoded without altering observable behavior.

B. Safety Implies Security

The central theoretical result is Theorem 2: For all levels $\ell$ , any pre-run that is safe for $\ell$ is secure for $\ell$ .

Safety is defined as the absence of assertion/alignment failures and the presence of valid fiats (assumption or divergence) for any alternative input list.
The proof demonstrates that if a program is safe, the set of inputs an observer learns ( $k_\ell$ ) is a subset of the inputs allowed by the release policy ( $RP_\ell$ ), intersected with progress knowledge.
This result validates the approach of enforcing security via relational verification of program annotations rather than complex runtime monitoring of all possible executions.

C. Machine-Checked Verification

The entire development, including the corrected definitions and the main theorem, has been machine-checked in Rocq. This confirms that the corrections to the CN paper are fundamentally sound, while also uncovering subtle details in the proofs that were missed in the original human-written sketches.

D. Experience with Agentic AI

The paper documents the use of an agentic AI (Claude Code) in the formalization process. The author notes that while the AI was capable of generating non-trivial infrastructure and routine proofs, it required human oversight to:

Correct flawed formalizations of lemmas (e.g., Lemma 3).
Identify and fix logical gaps in the definition of "divergence fiat."
Refine the definitions of knowledge ( $k_\ell$ ) to use prefixes rather than equality, a change necessitated by counterexamples found by the AI.
Prevent the AI from over-strengthening assumptions or introducing unnecessary decidability hypotheses.

4. Results

Formal Correctness: The machine-checked proof confirms that the revised safety condition correctly implies the epistemic security property for the reactive program model.
Resolution of CN Flaws: The specific flaws in the 2018 CN proof regarding the alignment of runs and the definition of the release policy have been resolved.
Feasibility of AI-Assisted Formalization: The study demonstrates that agentic AI can effectively assist in translating complex mathematical specifications into machine-checked proofs, provided the human expert actively guides the tool, corrects its logical missteps, and manages the overall proof architecture.

5. Significance and Claims

The paper claims modest but significant contributions:

Unifying Framework: It offers a corrected, general framework for expressing and verifying expressive flow policies using epistemic logic and relational annotations.
Practical Verification: By showing that safety (a property amenable to runtime monitoring and inductive proof) implies security, the work bridges the gap between high-level policy specifications and enforceable program properties.
Reliability of Machine Checking: The work underscores the necessity of machine checking for verification, even for theoretical developments in idealized settings, as it exposes subtle errors that human review might miss.
AI in Formal Methods: It provides a concrete case study of using agentic AI for substantial formal developments, highlighting both the potential for efficiency gains and the critical need for human expertise to ensure logical rigor.

The author explicitly states that the development of compositional proof rules for the safety condition remains an open problem and that the current work focuses on the foundational semantics and the main implication theorem. The paper is dedicated to David Basin, acknowledging his pioneering role in machine-checked formalization for security.