Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI David A. Naumann[0000−0002−7634−6150] ⋆
arXiv:2608.00882v1 [cs.AI] 1 Aug 2026
Stevens Institute of Technology, USA
Abstract. Many high-level security requirements are about the allowed flow of information in programs and are difficult to make precise because they involve selective downgrading. Notions from epistemic logic have emerged as a good approach to policy semantics but a robust general framework remains elusive. A paper appearing in CSF 2018, entitled “Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies”, attempted to provide a unifying framework—but the formalization was sketchy and a correction was announced during the conference presentation. With aid from an agentic AI coding assistant, a corrected formalization has been machine checked in the Rocq proof assistant. The simplicity and generality of the framework may help compare different policy specification styles and enforce them by leveraging existing techniques. Keywords: information flow security · epistemic logic · program annotations · relational verification · agentic AI coding assistants
1
Introduction
Security and privacy requirements for computing systems restrict the flow of information and involve subtle tradeoffs such as utility versus privacy and strength of assurance versus cost of system development and enforcement. The malleability of data, control, and communication in computing makes it difficult to precisely model information and its flow as needed for high assurance, but much has been learned through decades of research and practice. An established and influential approach to formalization is epistemic [3,6]. Confidentiality requirements are formulated as what an observer at a given level of privilege is permitted to know about sensitive information. This can enable expression of downgrading policies with state/event-dependent conditions—when can who learn what information derived from secrets. There have been a number of technical developments of the epistemic approach for confidentiality and integrity, formulated for program models including batch, reactive, concurrent, and higher order. A key criterion is for it to be possible for stakeholders to audit candidate policy specs extensionally, that is, in terms of program behavior independent from the code of the program ⋆
This work was partially supported by NSF SaTC award CNS 2426414.
2
in question. This is in tension with the convenience to specify downgrading by some form of program construct or annotation, which has two benefits: facilitating enforcement (e.g., by type systems) and expressing policies where program state and control point clearly represents the conditions or events under which downgrading is intended. In a paper we refer to as CN [17], the authors1 present a formalization for a reactive program model where policies are expressed using assume statements in the code but a derived release policy is expressed solely in terms of the input stream. This was intended to address the aforementioned tension and explore how an observation-oriented epistemic security property can be enforced via reasoning about program annotations, specifically relational assertions and assumptions. The main result was a theorem stating that security follows from so-called safety, where the latter is a program-oriented property amenable to runtime monitoring and proof by induction on execution steps. Unfortunately, as announced during the paper’s presentation at CSF’18, there is a significant flaw in the published version’s proof. A corrected definition of release policy and the proof was sketched at the time [17]. This paper works out the details and makes further revisions culminating in a fully machine checked proof of the main result using the Rocq proof assistant [35]. Murray et al [26] adapt the approach of CN to concurrent C programs, featuring a policy language separate from the code and a clear separation between verification that the code satisfies the relevant annotations (policy-agnostic) and confirmation that a separately given policy spec is consistent with the code annotations. The theory of [26] has been machine checked, providing high assurance for an embodiment of the approach; but the security property is constant-time, a very strong property that trivializes the complications aligning multiple executions in reasoning about epistemic properties. In brief, our contributions here are as follows. (a) An epistemic semantics that revises the one in CN but still makes explicit the semantics of release policy as such. (b) A slightly revised formulation of the safety condition from CN, and machine checked proof that safety implies security. (c) Remarks on our experience using an agentic AI coding assistant to develop the Rocq proof. Machine checking seems essential for verification of practical systems, with all the complexities of their programming languages and platforms, and even for high level designs [8]. The story of this paper is one of many instances where even a careful theoretical development in an idealized setting has mistakes. Our machine checked result confirms that the announced corrections of CN are basically correct but machine checking uncovered details that were not correct. Although the program model and main definitions are fairly simple, some proofs are intricate as is often the case when reasoning about multi-run properties. Outline: Section 2 uses a simple example to introduce the programming and specification notations. The example is taken from CN and throughout this document we have borrowed liberally from the text of that paper. We refer the 1
Apropos authorship: the authors of CN collaborated on high level ideas and examples but the second author is to blame for the formal development, especially its flaws.
Assuming You Knew
3
reader to that paper for more extensive discussion of the appoach and further examples. The formal development begins in Section 2 with programs and their annotations. Throughout the paper we use standard math style. The intent is to faithfully render the machine checked develpment in a readable way. Section 4 defines release policy and security, Section 5 defines safety and Section 5.2 gives the main theorem. Section 6 discusses related works. Section 7 describes how the agentic tool Claude Code [2] was guided to translate from the LATEX file of the corrected CN to the Rocq specs and to complete the proofs. The original proof sketches have been updated for the revised definitions; for lack of space they are relegated to an appendix.
2
Declassification by example
We introduce our specifications with an example, written in a small imperative reactive language inspired by [12]. We add relational assertions and assumptions, inspired by [16], for specifying information flow requirements. Our example is a randomized response sampling algorithm (Figure 1). The purpose of the algorithm is to provide differential privacy and plausible deniability to the respondents to a sensitive yes/no question, preserving the statistical characteristics of the underlying data [20]. The idea is that a respondent’s answer may or may not be used depending on a random coin flip. We use three communication channels, Private (P ) input that feeds binary private responses to the sampler, Random (R) input providing a source of secure random bits, and Public (L) output, that expects the anonymized responses. Programs consist of input handlers, one for each input channel. Variables including handler parameters are initialized to 0 at system start. Handlers run to completion and optionally produce output. The first handler (inputP ) is the input sampler. The second handler ensures the first always has two fresh random bits. We source randomness from a single channel and thus have to ensure there are two fresh random bits, stored in variables r1 (for the coin flip) and r2 for the randomized reply. This contrived program is intended to be used in an environment where two bits of randomness are sent prior to each response bit. Loss of additional random bits would not matter but dropping response bits would be unsatisfactory. We can ensure security of this program by enforcing the following information flow policy. Private data is only disclosed to the public under the condition that r1 is true. We can formalize this policy by considering channel identifiers to be labels and arranging the labels in a partial order, such that for any labels ℓ1 , ℓ2 related by the ordering ℓ1 ⊑ ℓ2 information from the input channel with a label ℓ1 is allowed to flow to the output channel with a label ℓ2 . The attack model is a standard one. Principals are labeled. The principal at level ℓ can provide inputs and observe outputs at all levels ℓ′ ⊑ ℓ. The program is known to all. In the example, the labels are ordered such that L ⊑ P and L ⊑ R. This baseline policy disallows direct disclosure of the both the randomness and the responses to the public observer. However, it also disallows the intended disclosure. We resolve this issue by relaxing the policy in two places in the program
4
using downgrading annotations in Figure 1. The annotation assumeL Ar declassifies the received bit r to the public label L. The notation alludes to the standard two-run semantics of dependency: the agreement formula Ar says a pair of states agree on the value of r. So the policy says if two runs agree on r then outputs on L also agree. The annotation assumeL Br1 ⇒ Ap effectively relabels the private response bit p with the label L, but only in the case the value of r1 in that program execution is true. The formula Br1 says r1 is true (non-zero) in both runs. inputP p. if ready > 1 then/ ∗ user ∗ / assumeL Br1 ⇒ Ap; if r1 then o := p; else o := r2 ; fi outputL o; ready := 0; fi
inputR r. assumeL Ar; / ∗ randomness ∗ / if ready = 0 then r1 := r; else if ready = 1 then r2 := r; fi ready := ready + 1; fi
Fig. 1. Randomized response sampling algorithm
Whether this is a reasonable program and policy depends on the statistical properties of the channel R. In general, the policy specification needs to be justified in terms of the quantitative notions of differential privacy. However, that also requires reasoning about the environment in which the program is run and the statistical properties of its inputs. In contrast, the specification in the code expresses what the observer is allowed to learn: the R values and the P values, but only under a certain condition. This can be understood in non-quantitative, epistemic terms as we formalize later. Together with the assumption of randomness of the R inputs, this gives us the security guarantee.2 These examples express downgrading in terms of current values of program variables, although only inputs and outputs are considered to be observable. In CN we introduce as second form of agreement (written Aℓ@n) for agreement on the nth value on input channel ℓ, to express policy directly in terms of observables. (Auxiliary state can also be used for that [7,26].) An example of its use is a simple packet sniffer that logs the source IP addresses of packets while ensuring confidentiality of payloads. The formalization here is abridged for brevity.
3
Programs, annotations, and event traces
As shown in the example we formulate policy in terms of a fixed labeling of channels and a fixed may-flow relation on labels, together with annotations to 2
This is not an isolated example of the issue: The security of the well-known in the literature password checking example, where only the outcome of the password test but not the password itself can be declassified, depends in a large part on the length of passwords and their distribution. A typical policy can be expressed, in our notation, as Anumguesses ∧ (B(numguesses < 10) ⇒ A(guess = pass)). If the set of possible secret values is too small, even disclosing the result of this small number of tries is unacceptable.
Assuming You Knew
5
express conditional flows that would not be allowed by the baseline policy. This section begins the technical development by formalizing these building blocks. We assume given a partially ordered set L of security levels, and write ℓ ⊑ ℓ′ for the ordering. Events t are given by the grammar t ::= inℓ n | outℓ n | •
where ℓ ∈ L, n ∈ Z
Identifiers t, u, v range over events. The event inℓ n represents the input of value n on ℓ’s input channel; outℓ n is for ℓ’s output channel. The tick event • lets us associate an event with every transition. An event t is visible at ℓ if t is an ′ input or output at some level ℓ′ ⊑ ℓ. Let Inℓ = {inℓ n | ℓ′ ⊑ ℓ and n ∈ Z}, let ′ Outℓ = {outℓ n | ℓ′ ⊑ ℓ and n ∈ Z} and Evℓ = Inℓ ∪ Outℓ . For a sequence ts of events we write visℓ (ts) for the sub-sequence of ℓ-visible ones, i.e., those in Evℓ . 3.1
Programs
A program consists of a set of input handlers, one for each security level. The program consumes a sequence of inputs, handling each one in turn. The syntax inputℓ x. c is for handler associated with channel ℓ, with body c, in which variable x is initialized to the input value. A handler may produce zero or more outputs, which may be on different channels from its input. If a handler diverges, no further input is consumed. Programs are input total in the sense that, unless the last handler is diverging, the next input event can be consumed. inputℓ x. c
Handlers
e ::= n | x | e ⊕ e | ¬e (n ∈ Z, x ∈ Vars, ⊕ ∈ {+, ∗, =, ≤, ∧, . . .}) expression c ::= skip | x := e | outputℓ e | if e then c else c | while e do c | c ; c command | assertℓ Φ | assumeℓ Φ ′
′
An ℓ-annotation is a command of the form assertℓ Φ or assumeℓ Φ such that ′ ℓ ⊑ ℓ. Annotations have no influence on the observable behavior of the program. The ℓ-annotations that are assumptions specify what the observer at level ℓ— seeing inputs and outputs on channels ℓ′ ⊑ ℓ—is allowed to learn. Assertions are only needed for enforcement (Section 5). As shown by the introductory example, the handler for some level ℓ may have annotations for unrelated levels. Relational formulas Φ for annotations φ ::= e | φ ∨ φ | ¬φ | ∀x.φ state predicate Φ ::= Ae | Bφ | Bφ ⇒ Ae basic relational formula Φ ::= Φ ∧ Φ conjunction of basic formulas The form Bφ ⇒ Ae can be used together with auxiliary variables to encode various forms of state dependent downgrading policies [7].
6
3.2
Program semantics
In the rest of the paper, we consider a fixed program i.e. set of handlers, which is left as an implicit parameter to streamline notation. A state σ maps variables to integers. At the start of a handler execution, the designated variable is set to the input value and all other variables are unchanged (i.e., variables are global to all handlers). Configurations are of two kinds. A receptive configuration ⟨σ⟩ contains just a state σ. An active configuration ⟨c, σ⟩ represents the execution of a handler, where c represents the current control and σ is a state. The initial configuration is ⟨σ0 ⟩ where σ0 t maps all variables to 0. We write g → h to indicate that g transitions to h with associated event t. t
g→h
Transition semantics inputℓ x.c is the handler for ℓ
σ ′ = (σ | x : n)
•
⟨skip, σ⟩ → ⟨σ⟩
ℓ
in n
⟨σ⟩ → ⟨c, σ ′ ⟩ σ(e) ̸= 0
σ(e) = n outℓ n
⟨outputℓ e, σ⟩ → ⟨skip, σ⟩ •
⟨assumeℓ Φ, σ⟩ → ⟨skip, σ⟩
•
⟨if e then c else d, σ⟩ → ⟨c, σ⟩ •
⟨x := e, σ⟩ → ⟨skip, (σ | x : σ(e))⟩ t
•
⟨assertℓ Φ, σ⟩ → ⟨skip, σ⟩
•
⟨skip; c, σ⟩ → ⟨c, σ⟩
⟨c, σ⟩ → ⟨c′ , σ ′ ⟩ t
⟨c; d, σ⟩ → ⟨c′ ; d, σ ′ ⟩
The first rule consumes an input, transitioning from a receptive configuration to an active one. The updated state (σ | x : n) maps x to the input value n and leaves the other variables unchanged. The other rules all start from an active configuration, and produce either an output event or •. The second rule transitions to a receptive configuration from an active one in which the handler has terminated. The remaining rules involve only active configurations. In the rule for output we write σ(e) for the value of expression e in state σ. Comparisons (=, ≤) and logical operators (∧, ¬) return 1 or 0, and non-zero values are interpreted as true. Omitted rules for assignment, loop, and conditional are standard, as are the last two rules which are for sequencing. If c is different from skip then we can define redex(⟨c, σ⟩) to be the unique command b such that b is not a sequential composition and either c ≡ b ; d for some d, or b ≡ c. For example, in the penultimate rule the redex is skip, and redex(⟨(x := 0; y := 1); z := 2, σ⟩) is x := 0. The last rule allows the redex in a sequence to take a step. Lemma 1. For every active configuration there is a unique output or • event and unique successor configuration. For every receptive configuration and every input event there is a unique successor configuration for that event.
Assuming You Knew
3.3
7
Program pre-runs and event traces
Knowledge is defined in terms of the trace of events a program engages in, but specifications are expressed as program annotations, so we need to work with both computations and event traces. A pre-run 3 is a non-empty list of consecutive program configurations, starting with the initial configuration ⟨σ0 ⟩. We use letters g, h for configurations, and plural identifiers gs, hs for finite sequences thereof—lists for short. Likewise we use ts for lists of events, and sometimes ins for lists of input events. We write |gs| for the length of gs, [ ] for the empty list, and · for catenation of lists—and also for appending an element at the start or end of a list. We also treat lists as functions from an initial segment of the naturals. So gs0 is the first configuration and dom(gs) is the set of indices 0, . . . , |gs| − 1. We write last(gs) for gs|gs|−1 , and gs⇂i for the first i elements of gs (i.e., the prefix up to but not including the element gsi ). We write gs ⪯ gs′ to say gs is a prefix of gs′ . For any event list ts, let inp(ts) be the subsequence of input events. Every list ins of input events gives rise to a unique execution which consumes the inputs or diverges trying to. Before formalizing this, we define the unique list of input and output events, called a trace, associated with a pre-run. gs ⇓ ts
Event trace admitted by a pre-run t
[⟨σ0 ⟩] ⇓ [ ]
gs ⇓ ts last(gs) → g gs · g ⇓ ts · t
So a pre-run is just a configuration list that admits a trace. The pre-runs of the program under consideration comprise the set {gs | ∃ts. gs ⇓ ts}. It is closed under nonempty prefixes but does not contain [ ]. In subsequent definitions and results, quantifications over pre-runs implicitly range over this set. As an example consider the program with handlers inputP x. outputQ x + 1
inputQ y. outputQ w; w := w + x + y
It has a pre-run which admits the trace ts = [inQ 3, outQ 0, •, •, •, inP 1, outQ 2, •]. This trace has inputs inp(ts) = [inQ 3, inP 1]. The pre-run has distinct states (x:0, y:0, w:0), (x:0, y:3, w:0), (x:0, y:3, w:3), (x:1, y:3, w:3). The second and third states are in the Q-handler and the last in the P -handler. In light of determinacy (Lemma 1), one may expect that a pre-run gs determines a unique ts with gs ⇓ ts. There is a minor wrinkle for receptive configurations. In the configuration following an input transition one can see from the handler body which channel’s handler is running—unless two channels have identical handlers! Starting in Section 3.4 we impose a mild condition that makes handler bodies distinct and ensures the expected result (Lemma 2). 3
In the literature on epistemic logic [6] a “run” is a complete program execution; so we use the term pre-run as we are considering finite prefixes only.
8
3.4
Well specified programs
Henceforth we require that the program under consideration satisfies the following condition. A program is well specified provided that for every ℓ, with handler inputℓ x.c, we have (a) c has the form assumeℓ Ax ; d, for some command ′ d; and (b) every output command outputℓ e in d is immediately preceded in ′ sequence by assertℓ Ae. Let us call these boilerplate annotations. They help streamline the formalization by encoding the baseline policy designated by channel labels and the ordering on labels.4 Boilerplate assumptions are used in the definition of release policy (Section 4.2). Boilerplate assertions are used to make security enforceable (Section 5). The requirement loses no generality because the requisite annotations can be added without altering the behavior—except for adding • events, which are not observable. Lemma 2. If gs ⇓ ts and gs ⇓ ts′ then ts = ts′ . In light of Lemma 2 we can define the input history, inp(gs), of a pre-run gs. It is simply inp(ts) where ts is the unique event list with gs ⇓ ts. Owing to the possibility of divergence, input totality does not imply that every input list can be fully consumed. However, an input list produces a unique possibly infinite execution, so we can talk about the pre-runs that arise in consuming an input list ins. The gist is that we build gs by executing the handlers on ins0 , ins1 , . . . , until either a handler diverges or all inputs have been consumed. In order to describe gs in a way that is unique in the divergence case, without recourse to infinite sequences, the following result truncates a divergent pre-run just before the start of the divergent handler invocation. If some input, say insk , causes its handler to diverge, that is described in terms of a series of finite prefixes of the diverging sequence, each ending with steps of the handler for insk . Lemma 3. For any list ins of input events, there is a unique pre-run gs such that (a) inp(gs) ⪯ ins, (b) last(gs) is receptive, and (c) if inp(gs) ̸= ins, i.e., inp(gs) = ins⇂k for some k < |ins|, then there is an infinite sequence G of lists of active configurations such that, for all i, j we have: |Gi | = i + 1, gs · Gi is a pre-run, inp(gs · Gi ) = ins⇂(k + 1), and i < j ⇒ Gi ⪯ Gj .
4
Knowledge semantics for declassification
In this section we define what it is for a pre-run to be secure. Section 4.1 defines the notion of knowledge at a level ℓ: What can be learned by observing channels visible to ℓ and reasoning about the program, which is known to the observer. Section 4.2 defines the notion of release policy at ℓ, expressed by ℓ-assumptions in the program, and defines security, which says that knowledge is gained only in accord with release policy. 4
For a practical notation one would bake the effect of these annotations into the semantics and explicit annotations would then be needed only for declassification.
Assuming You Knew
4.1
9
Knowledge
Conceptually, the ℓ-observer decides what inputs to provide at levels ℓ′ ⊑ ℓ, and learns from observing outputs on channels at levels ℓ′ ⊑ ℓ. Following Beringer’s [10] terminology, the major pre-run or trace is the actual execution and minor ones are the possible executions about which the observer reasons. For a given list ts of events, the ℓ-observer’s knowledge of the inputs (on all channels) is based on their observation of the ℓ-visible inputs and outputs. Knowledge from a trace
kℓ
kℓ (ts) = {inp(us) | ∃gs. gs ⇓ us ∧ visℓ (ts) ⪯ visℓ (us)} The condition captures knowledge as follows. Having observed visℓ (ts), the observer knows that the possible complete inputs are those that arise from some pre-run gs of the program with trace us that is consistent with what was seen so far. Lemma 4. (a) If t is not ℓ-visible then kℓ (ts · t) = kℓ (ts). (b) If t ∈ Evℓ then kℓ (ts · t) ⊆ kℓ (ts). The difference kℓ (ts) \ kℓ (ts · t) represents what is learned by observing output event t. The baseline policy expressed by labels—noninterference—can be expressed by saying nothing is ever learned: for all ts and all output events t, kℓ (ts) \ kℓ (ts · t) = ∅ or equivalently kℓ (ts · t) ⊇ kℓ (ts). The notion of knowledge defined above is progress-sensitive: kℓ (ts) excludes input lists that drive the program to divergence before the last input is handled. In reality, one cannot observe the absence of progress—only stronger properties such as the passage of a fixed amount of time. Moreover, enforcement of progress-sensitive security can be costly and restrictive. So we aim for a progressinsensitive security property. A simple way to formulate such a property is to entirely disregard diverging pre-runs (as in [3,21]), but this fails to address the security of visible events prior to divergence. A more nuanced approach (e.g., [4]) formulates security in a way that essentially declassifies, at each step of execution, the fact whether the program will diverge without producing or enabling the consumption of further visible events. In this approach one formulates a notion of progress knowledge kℓ→ defined like kℓ except that in addition the observer knows there will be another visible event. Progress knowledge
kℓ→
kℓ→ (ts) = {inp(us · t · vs) | t ∈ Evℓ ∧ ∃hs. hs ⇓ us · t · vs ∧ visℓ (ts) ⪯ visℓ (us)} Lemma 5. (a) kℓ→ (ts) ⊆ kℓ (ts), and (b) if t ∈ Evℓ then kℓ (ts · t) ⊆ kℓ→ (ts). Progress-insensitive noninterference definitions in the literature are roughly equivalent to kℓ (ts · t) ⊇ kℓ→ (ts) holding for all ts and all visible outputs t. We cannot do an exact comparision with, say, ID security of Bohannon et al. [12] because our model is not exactly the same.
10
4.2
Release policy and security
A relational formula Φ is interpreted as a relation on states. (In CN the states are paired with input lists, to interpret channel agreements.) Semantics of relational formulas σ|σ ′ |= Ae σ|σ ′ |= Bφ σ|σ ′ |= Bφ ⇒ Ae σ|σ ′ |= Φ0 ∧ Φ1
σ | σ ′ |= Φ
iff σ(e) = σ ′ (e) iff σ |= φ and σ ′ |= φ iff σ|σ ′ |= Bφ implies σ|σ ′ |= Ae iff σ|σ ′ |= Φ0 and σ|σ ′ |= Φ1
g | h |= Φ iff sta(g) | sta(h) |= Φ (where sta projects the state of a configuration) Next we define the release policy RPℓ (gs) for a pre-run gs. Like knowledge, it is a set of input lists. The policy says the ℓ-observer is allowed to know the declassifying ℓ-assumptions were reached as well as the information they convey (the value of expressions in agreement). First some technical notions. Alignment, semi-proper alignment for ℓ, coverage For pre-runs gs, hs, an alignment from gs to hs is a relation α ⊆ dom(gs) × dom(hs) that (a) is monotone, i.e., ∀i, j, k, l with iαj and kαl, i < k ⇒ j ≤ l and j < l ⇒ i ≤ k; and (b) has prefix-closed domain and range, i.e., i ∈ dom(α) (resp. rng(α)) and 0 ≤ j < i imply j ∈ dom(α) (resp. rng(α)). A semi-proper alignment for ℓ from gs to hs is an alignment α such that for all i, j with iαj, if either redex(gsi ) or redex(hsj ) is an ℓ-assumption then redex(gsi ) = redex(hsj ). A semi-ℓ-aligned pre-run pair is a triple (gs, hs, α) where α is a semiproper alignment for ℓ from gs to hs. For α to cover the major pre-run gs (resp. the minor pre-run hs) means that dom(α) = dom(gs) (resp. rng(α) = dom(hs)). The condition redex(gsi ) = redex(hsj ) is meant to express that gsi and hsj are both active configurations, with exactly the same assumption: not just the same level and formula but exactly the same occurrence in the program text, i.e., point in control flow. (To make that precise one can provide each annotation occurrence with a unique identifying label.) Semi-conformance
SCℓ
A semi-conformance at ℓ is a semi-ℓ-aligned pre-run pair (gs, hs, α) where α covers both gs and hs, and for all i, j, if iαj and redex(gsi ) is an ℓ-assumption Φ then gsi | hsj |= Φ. We write SCℓ (gs, hs, α) in this case. The key definition makes explicit the semantics of declassification policy as expressed by assumptions.
Assuming You Knew
Release policy for a pre-run
11
RPℓ
RPℓ (gs) = {inp(us) | ∃hs, α. SCℓ (gs, hs, α) ∧ hs ⇓ us} Owing to the boilerplate assumptions and coverage conditions, RPℓ (gs) only includes ins such that visℓ (ins) = visℓ (inp(gs)). Owing to non-boilerplate assumptions it includes only ins from pre-runs that agree with respect to declassified expressions, which may have been influenced by non-observable inputs (e.g., the L-assumption in the P -handler in Figure 1). Secure pre-run A pre-run gs is secure at level ℓ provided that for every prefix hs · g ⪯ gs (with hs nonempty) the step to g is secure at level ℓ. For the step to be secure at ℓ means that, for all ts, t if hs ⇓ ts and hs · g ⇓ ts · t then kℓ (ts · t) ⊇ kℓ→ (ts) ∩ RPℓ (hs · g)
(1)
Recall that ts, t are uniquely determined by hs, g (see Lemma 2). For t ∈ / Evℓ , ℓ ℓ ℓ (1) always holds because k→ (ts) ⊆ k (ts) = k (ts · t) by Lemmas 5(a) and 4(a). For t ∈ Evℓ , always kℓ (ts · t) ⊆ kℓ→ (ts) by Lemma 5(b), so (1) says that kℓ (ts · t) is no smaller—the learning no greater—than allowed by RPℓ .
5
Safety and Security
In this section we define a notion called safety,5 adapted from Chudnov et al. [16], which connects a major pre-run to minor pre-runs with alternate input histories. This makes no reference to observations or release policy but instead directly interprets annotations in terms of aligned steps of the major and minor pre-run. 5.1
Safety
In [16] the concern is to account for all possible initial states. Here we aim to account for all possible input lists and their associated pre-runs. This account is based on a classification: Given a (major) pre-run gs and an input list ins, the (minor) pre-run associated with ins may diverge or violate an assumption, in which case it can be disregarded—we call those ‘fiats’. Alternatively, it may be in conformance with policy, or violate policy due to a mis-aligned annotation (called alignment failure) or due to an assertion failure. The idea is that gs is safe if there are no alternate pre-runs resulting in assertion or alignment failure. 5
Apropos the word ‘safety’, it will be defined in terms of major/minor pre-run pairs in a way akin to 2-safety, in the terminology of trace and hyperproperties [18], but technically our safety condition is a property of pre-runs paired with input lists.
12
A proper alignment for ℓ from gs to hs is an alignment α such that for all i, j with iαj, if either redex(gsi ) or redex(hsj ) is an ℓ-annotation then redex(gsi ) = redex(hsj ). An ℓ-aligned pre-run pair is a triple (gs, hs, α) where α is a proper alignment from gs to hs for ℓ Remark 1. The following definitions take advantage of a fine point about the transition semantics. It is defined so that the redex in the step following an annotation is skip. If redex(gsi ) is an annotation then redex(gsi−1 ) and redex(gsi+1 ) are not annotations. Remark 2. In any proper alignment α for ℓ, if i is the index of the nth ℓannotation in gs and j is the index of the nth ℓ-annotation in hs then iαj and α does not relate i (on left) or j (on right) to anything else. Classification of aligned pre-run pairs The following notions are parameterized on a given level ℓ and input list ins. A conformance is an ℓ-aligned pre-run pair (gs, hs, α) where inp(hs) ⪯ ins, α covers hs, and for all i, j, if iαj and redex(gsi ) is an ℓ-annotation with formula Φ then gsi | hsj |= Φ (2) Moreover either α covers gs or inp(hs) = ins and last(hs) is receptive. An assumption fiat is ℓ-aligned (gs, hs, α) where inp(hs) ⪯ ins, α covers ′ hs, and there are i, j, Φ such that i < |gs|, j = |hs|−1, iαj, redex(gsi ) is assumeℓ Φ with ℓ′ ⊑ ℓ, Eqn. (2) does not hold, and (gs⇂i, hs⇂j, β) is a conformance for ℓ, ins that covers gs⇂i, where β = {(k, l) | kαl ∧ k < i ∧ l < j}. An assertion failure is the same as an assumption fiat, except that redex(gsi ) ′ is assertℓ Φ with ℓ′ ⊑ ℓ. An alignment failure is ℓ-aligned (gs, hs, α) where inp(hs) ⪯ ins, α covers hs, and there are i, j such that i < |gs|, j = |hs|−1, redex(gsi ) is an ℓ-annotation, redex(hsj ) is an ℓ-annotation different from redex(gsi ), and (gs⇂i, hs⇂j, α) is a conformance for ℓ, ins that covers gs⇂i. A divergence fiat is ℓ-aligned (gs, hs, α) where inp(hs) ⪯ ins and there are i, j, k with i < k < |gs| and j = |hs| − 1 such that (gs⇂(i + 1), hs, α) is a conformance (for ℓ, ins), redex(gsk ) is an ℓ-annotation, and no ℓ-annotation occurs as redex in gs between i and k. Moreover iαj and either i = 0 = j or redex(gsi ) is an ℓ-annotation or redex(gsi ) and redex(hsj ) are ℓ-outputs.6 Finally, there is an infinite sequence H of configuration lists such that for all n ∈ N, |Hn | = n, hs · Hn is a pre-run with inp(hs · Hn ) ⪯ ins, and Hn contains no ℓ-annotation or ℓ-output. For example, suppose the input history of the major pre-run gs is [inℓ 1, inℓ 2]. At level ℓ, with ins = [inℓ 3, inℓ 2], we get an assumption fiat regardless of the program. That is because a well specified ℓ-handler begins with an assumption that 6
That is, outputs at some level ℓ′ ⊑ ℓ. A nontrivial semantic fact is that under these conditions they will in fact be the same output owing to boilerplate assertions.
Assuming You Knew
13
the inputs agree, so any minor pre-run aligns properly and the initial agreement is false. A subtlety in the definition of (ℓ, ins)-conformance has to do with the intention to account for all steps of gs. If ins provides enough inputs, this can be achieved, in which case α covers gs. If ins fails to provide enough inputs for the minor pre-run hs to fully align with gs, nonetheless hs should be as long as possible, i.e., reach a receptive configuration. The case where gs is not covered is not a satisfactory account of the security of gs, but this is not a problem because the safety condition (below) quantifies over all input lists ins. Divergence fiat needs to be understood in connection with programs being well specified and input total. Because ℓ-visible inputs are accompanied by annotations for ℓ, a divergence fiat indicates that the minor pre-run is continuing without producing visible output or consuming visible input. That could be due to a nonterminating loop with no outputs, or one with non-visible outputs. By contrast, in an alignment failure, the minor pre-run definitely reaches another ℓ-annotation, but one that does not match gs. Safe pre-run A pre-run gs is safe for level ℓ and inputs ins iff there are hs, α such that (gs, hs, α) is a conformance, an assumption fiat, or a divergence fiat for ℓ, ins. A pre-run is safe for ℓ if for every ins it is safe for ℓ, ins. If gs is safe, every alternative input list is either not a leak (owing to boilerplate asserts and conformance) or can be disregarded due to either (a) divergence, (b) inconsistency with visible inputs (owing to boilerplate assumptions), or (c) intentional release (owing to non-boilerplate assumptions). Extending a failed or fiatted pre-run yields the same. Lemma 6. If gs · g and gs are pre-runs and (gs, hs, α) is an assumption or divergence fiat for ℓ, ins, or an assertion or alignment failure for ℓ, ins, then so is (gs · g, hs, α). Lemma 7. If gs · g and gs are pre-runs and gs · g is safe for ℓ then so is gs. The details in the definitions of failures, fiats, and conformance are motivated by the need to make these conditions mutually exclusive (unlike in [16]) and exhaustive, as confirmed by the following classification result. Theorem 1. For any gs, ins, and ℓ there are hs and α such that (gs, hs, α) is either a conformance, an assertion or alignment failure, or an assumption or divergence fiat, for ℓ, ins. Furthermore, a given gs, ins, ℓ fits in only one category, although there may be more than one hs, α that witnesses its membership in the category. The proof goes by induction on gs and constructs the requisite hs and α. For the sake of induction hypothesis, a stronger property is proved for conformance, namely that if last(hs) is an ℓ-annotation then so is last(gs).
14
The construction of hs and α amounts to the design of an ideal monitor. Simultaneously for the minor pre-runs of all ins, the monitor tracks the steps of the major run and reasons about the minor run for ins. If any ins results in an assertion or alignment failure, then continuing execution of gs is unsafe. 5.2
Relational safety implies epistemic security
Security says that for each observer level ℓ, what they may learn is within what is allowed by the release policy as specified by (non-boilerplate) ℓ-assumptions. Our main result is that safety implies security. Theorem 2. For all ℓ, any pre-run that is safe for ℓ is secure for ℓ. A detailed proof is sketched in Appendix A, including the assumption fiat case which was wrong in CN. The crux is to consider the three safe possibilities for the last step in pre-run hs · g in Eqn. (1). We must show, for any ins, that ins ∈ kℓ→ (ts) and ins ∈ RPℓ (hs · g) imply ins ∈ kℓ (ts · t). Conformance lets us establish the consequent. Assumption fiat contradicts ins ∈ RPℓ (gs · g). Divergence fiat contradicts ins ∈ kℓ→ (ts). A condition similar to safety was shown to be monitorable in [16]. The idea is that the monitor abstracts from a collecting semantics [31,5] that tracks the classification of every ins (and at every level) with respect to the current pre-run. For static verification, safety can be proved by induction on the major pre-run, considering an arbitrary ins with its corresponding pre-run, along the lines of the proof of Theorem 1—the key point being to show that from a conformance the next step yields either conformance, assumption fiat, or divergence.
6
Related work
The reader can consult CN for relevant work as of 2018 so for brevity we just highlight a few more recent works. Works that enable specification of state dependent downgrading policies include [7,13,36,24,23] and typically feature epistemic security definitions. State can be used to designate ‘where’ in the code declassification occurs as well as ‘what’ is declassified (using terminology from [32]). Instead of an epistemic semantics, Menz et al [25] use logical relations for semantics of ‘where’ declassification in higher order programs. Inspired by epistemic logics, Soloviev et al [34] use modal operators—both for knowledge and for agents’ ability to read or write variables—to give elegant specifications of security properties including robust declassification. Robust declassification means that whatever is declassified cannot be influenced by the adversary [38]. Bay and Askarov [9] use an epistemic formulation to define the declassification of progress. Li and Zhang [21] use an epistemic style semantics for a system of dynamic policies that can express erasure which in some sense decreases knowledge. Cecchetti [14] uses infinite runs in the style of hyperproperties [18]
Assuming You Knew
15
to define progress-sensitive and progress-insensitive variations of robust declassification and the related properties like transparent endorsement [15]; the theory is machine checked in Rocq. CN aimed for extensional interpretation of policy not overly tied with the program, despite the policy being expressed by assumptions in the code. Murray et al [26] take the same approach and have a security condition like Eqn. (1) with an explicit release policy derived from assume commands. They make the connection between assumptions in code and external observation via ghost state that tracks application-specific notional event traces, an approach first suggested in [7] and compatible with the present work. But the technical development involves instrumented semantics: events track occurrences of assumptions as well as control branches, memory accesses, and thread scheduling, as needed for the strong constant-time security property. Their theory is machine checked in Isabelle/HOL; as noted in Section 1 the strong property greatly simplifies the alignment of minor and major runs. McCall et al [23] use an epistemic security condition for monitoring of eventdriven web programs where page elements and handlers can be added dynamically. Their system features state dependent declassification akin to what can be expressed in our system and in [26] although policies are not given a meaning independent of the security condition. Like [26], the security condition refers to instrumented semantics. A key contribution is to ensure robustness using lightweight taint tracking; robustness is proved as a corollary of the epistemic confidentiality condition. Although our semantics does not generate instrumentation events, annotations do take steps and our release policy makes reference to those via alignments. The flawed definition of RPℓ in CN made it a predicate on observed event traces whereas our fix makes it a predicate on pre-runs—though still designating possible input lists. Murray et al [26] make the connection between assertions in code and external observation via ghost state that tracks application-specific notional event traces, an approach first suggested in [7] and compatible with the present work. It seems difficult to formulate semantics for downgrading in a way that is fully extensional with respect to an un-instrumented semantics.
7
Remarks on the use of AI
In this section I switch to first person and report on my experience developing the Rocq formalization using Claude Code [2] (henceforth CC ). Two recent preprints [30,37] report on experiments using LLM-based coding assistants for substantial developments in Rocq, extending sizeable existing developments. Unlike those authors, I have not systematically analyzed the logs of my interactions. My main goal was to machine check the paper. I am an experienced user of Rocq and had previously used CC for a small inconclusive exploration in an existing Rocq development [28]. I ran CC on an isolated virtual machine and gave CC access to bash shell commands (used for reading and editing files), the LATEX file, the Rocq files it was developing, and
16
the Rocq MCP server7 which enables CC to inspect intermediate proof goals during processing of a proof script. I provided an initial Rocq file with only import directives for some libraries including classical extensionality and excluded-middle axioms. I gave the following initial prompt. “I want your help to create Rocq code to formalize the math in the Latex file paper-8June2026.tex. We will do this step by step. The math starts in the section labelled sec:programs. Think hard and create a detailed, step-by-step plan to formalize what’s in that section up to the Programs subsection”. I also instructed it not to alter definitions or statements of results without consulting me. I proceeded section by section over about three weeks, averaging an hour a day, pausing the session and resuming from compacted chat summaries and saved ’memories’. Twice I ended the session and started a new one, when CC seemed bogged down, distracted by its prior English proof sketches while not remembering an overall plan. Although I saved snapshots in a repository, CC only had access to the current version of the file. I was impressed that CC could develop nontrivial supporting infrastructure and do routine proofs on its own. For example, my proof sketches are imprecise about running the program for a few steps until something is reached, e.g., an assumption, or the program diverges. It developed an eval-with-fuel function and lemmas about that. CC pointed out some minor improvements while missing other obvious ones. For the original version of Lemma 3 it proposed a plausible but wrong formalization, which did bring my attention to a strengthing already suggested in the original expository text. CC intermittently presented me with design decisions because it was stuck or convinced a claim was false. I reviewed progress and occasionally corrected clear mistakes, e.g., its initial definitions for the classification of aligned pairs used semi-proper ℓ-alignment where it should be proper. While trying to prove a result akin to Lemma 3, to prove Theorem 1, it became clear that the definition of divergence failure in CN was flawed: it needed to allow additional inputs to be consumed before reaching the input whose handler diverges. This is how it was actually used in my proof sketches, but the paper’s formal definition had a constraint that every config is active. Oddly, CC failed to spot that the best fix is simply drop that constraint. Mutual exclusivity of the categories was vague in the original statement of Theorem 1. CC had trouble proving exclusivity of divergence fiat from alignment fault and presented me with an unconvincing counterexample. So I sketched a proof which helped sharpen the needed ingredients, e.g., the n-the visible annotation in pre-run. About Lemma 4(b), it found a counterexample. A proof had not been sketched in CN and it’s not used for main results, just a conceptual check that knowledge is defined sensibly. Similarly remarks apply to Lemma 5(b). CC’s proposed fixes included to require the program to be safe (noninterferent, it said, showing that it knows the literature), which is ridiculous. I gave it a proof sketch in which it found a flaw. This interaction led me to devise the current definitions of kℓ and 7
https://github.com/LLM4Rocq/rocq-mcp
Assuming You Knew
17
kℓ→ , using prefix where CN used equality. (Prefix is also explicit in the security condition of [23].) CC was prone to overly specific and intricate lemmas, where humans would step back and think about abstraction and elegance. For auxiliary definitions it was prone to using decidability hypotheses which is gratuitous because my initial Rocq imports included classical axioms. Here is an example of missing an obvious generalization. With the revised definition of knowledge, a lemma in CN about visible input no longer holds. It was never needed, just conceptual, and tied with the fact that definition of security excluded visible inputs. (With informal rationale that the observer of course learns what input they choose.) When revising the proof sketches after CC had completely proved the main theorem, I realized there’s no longer a need to exclude visible input in the definition of security. In a fresh CC session I asked it to drop the hypotheses t ∈ / Inℓ from definition of step_secure and plan a revised proof. It appeared to go off in the weeds so I had to point out how the hypothesis was also unnecessary in subsidiary lemmas it had introduced for the proof of Theorem 2. Similarly, Lemmas 4(b) and 5(b) had also been unnecessarily restricted to outputs. CC was keen to summarize progress and achieve progress in terms of number of Qed results. It was prone to cheating by strengthening assumptions in its lemmas (an oft-reported issue [30]) and by factoring out the hard part of a proof into a separate lemma. The sycophantic and over-confident tone of chatbots has been widely remarked and applies to CC. Occasionally it drifted from humanlike reasonable commentary to skating on thin ice. In a summary of progress it extruded this text: “So the substantive mechanization is complete: the security theorem safe_implies_secure, the classification (classification_exists), the whole annotation-rank cluster, the conformance-extension lemmas, and all the exclusivity lemmas are proven—resting only on the determinacy-axiom layer the development always intended to keep abstract.” To which I responded: “I’m not sure where you got the idea that ‘the development always intended to keep abstract’. Developments don’t have intentions. As a user I do have intentions, and in particular my intention is to fully machine check everything.” The proof scripts make pedestrian but intricate use of basic tactics to construct proofs. Though scripts are notoriously unreadable, humans have tactic usage styles to enhance readability for maintenance and adaptation. But with the advent of agentic AI coding tools such considerations may shift (as noted by Paraskevopoulou [30]). Wang [37] emphasizes the importance to use the coding tool to assist with cleanup, which I plan to do. The current Rocq code is available temporarily at https://www.cs.stevens.edu/~naumann/pub/temp_ assumeKnow.tgz and will be put somewhere permanent once it’s cleaned up. Human curation is surely needed for comments in the code. CC seems prone to documenting lemmas with wordy comments that are obscure due to references to some context where the lemma is used. That is also a sign that the lemmas do not factorize the proofs well. The proof of Theorem 2 is complete. The development currently comprises 9747 non-blank lines of code and 1057 lines of
18
comments. I suspect that, even without aggressive use of tactic automation, the development can be done in a third of that. Use of CC probably saved me time, especially if I amortize the time spent installing and getting familiar with the tools and improving my prompting. On the other hand, with a human collaborator, even an inexperienced student, our discussions might have sparked interesting new ideas.
8
Conclusion
We presented a machine checked knowledge based theory that accounts for declassification of secrets in accord with policy expressed by assume statements in code akin to declassif statements in prior works (e.g., [22,1]). The theory gives an explicit meaning to policy that is disentangled from the definition of security. The main result says that a condition called safety, amenable to monitoring and inductive proof, implies security. The development is a corrected version of the paper CN which also sketched the idea of static verification using relational Hoare logic. However, there is a considerable difference between our safety condition and the pre-post relational properties for which such logics have been developed [29]. One difference is that it explicitly asserts existence of a minor run whereas most relational Hoare logics are for an ∀∀ property (though some handle ∀∃, see [27,11,19]). Another difference is that it connects not a pair of executions but an execution and an input trace. Developing compositional proof rules for safety is left as an open problem. This paper is dedicated to David Basin on the occasion of his retirement. He recognized early on the importance of machine checked formalization for security. His pioneering works (e.g., [33]) have helped bring that vision to practical fruition [8].
References 1. Acay, C., Recto, R., Gancher, J., Myers, A.C., Shi, E.: Viaduct: an extensible, optimizing compiler for secure distributed programs. In: ACM Conference on Programming Language Design and Implementation (2021) 2. Anthropic: Claude code (2026), https://claude.com/claude-code, version using model Opus 4.8, accessed June 2026 3. Askarov, A., Sabelfeld, A.: Gradual release: Unifying declassification, encryption and key release policies. In: IEEE Symposium on Security and Privacy (2007) 4. Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. IEEE Computer Security Foundations Symposium (2009) 5. Assaf, M., Naumann, D.A.: Calculational design of information flow monitors. In: IEEE Computer Security Foundations Symposium (2016) 6. Balliu, M., Dam, M., Le Guernic, G.: Epistemic temporal logic for information flow security. In: ACM Workshop on Programming Languages and Analysis for Security (2011) 7. Banerjee, A., Naumann, D.A., Rosenberg, S.: Expressive declassification policies and modular static enforcement. In: IEEE Symposium on Security and Privacy (2008)
Assuming You Knew
19
8. Basin, D.A., Foster, N., McMillan, K.L., Namjoshi, K.S., Nita-Rotaru, C., Smith, J.M., Zave, P., Zuck, L.D.: It takes a village: Bridging the gaps between current and formal specifications for protocols. Commun. ACM 68(8) (2025) 9. Bay, J., Askarov, A.: Reconciling progress-insensitive noninterference and declassification. In: IEEE Computer Security Foundations Symposium (2020) 10. Beringer, L.: End-to-end multilevel hybrid information flow control. In: Asian Symposium on Programming Languages and Systems (2012) 11. Beutner, R.: Automated software verification of hyperliveness. In: Tools and Algorithms for the Construction and Analysis of Systems (2024) 12. Bohannon, A., Pierce, B.C., Sjöberg, V., Weirich, S., Zdancewic, S.: Reactive noninterference. In: ACM Computer and Communications Security (2009) 13. Broberg, N., Sands, D.: Paralocks: role-based information flow control and beyond. In: ACM Symposium on Principles of Programming Languages (2010) 14. Cecchetti, E.: Nonmalleable progress leakage. In: IEEE Computer Security Foundations Symposium (2025), https://doi.org/10.1109/CSF64896.2025.00029 15. Cecchetti, E., Myers, A.C., Arden, O.: Nonmalleable information flow control. In: ACM Computer and Communications Security. pp. 1875–1891 (2017) 16. Chudnov, A., Kuan, G., Naumann, D.A.: Information flow monitoring as abstract interpretation for relational logic. In: IEEE Computer Security Foundations Symposium (2014) 17. Chudnov, A., Naumann, D.A.: Assuming you know: Epistemic semantics of relational annotations for expressive flow policies. In: IEEE Computer Security Foundations Symposium (2018). https://doi.org/10.1109/CSF.2018.00021, corrected version dated July 29, 2018 has been available at https://www.cs.stevens.edu/ ~naumann/pub/csf2018corrected.pdf 18. Clarkson, M.R., Schneider, F.B.: Hyperproperties. Journal of Computer Security 18(6) (2010) 19. Dardinier, T., Müller, P.: Hyper Hoare logic: (dis-)proving program hyperproperties. Proc. ACM Program. Lang. 8(PLDI) (2024) 20. Dwork, C., Roth, A., et al.: The algorithmic foundations of differential privacy. Foundations and Trends® in Theoretical Computer Science 9(3–4) (2014) 21. Li, P., Zhang, D.: Towards a general-purpose dynamic information flow policy. In: IEEE Computer Security Foundations Symposium (2022) 22. Liu, J., Arden, O., George, M.D., Myers, A.C.: Fabric: Building open distributed systems securely by construction. J. Comput. Secur. 25(4-5) (2017) 23. McCall, M., Bichhawat, A., Jia, L.: Tainted secure multi-execution to restrict attacker influence. In: ACM Computer and Communications Security (2023) 24. McCall, M., Zhang, H., Jia, L.: Knowledge-based security of dynamic secrets for reactive programs. In: IEEE Computer Security Foundations Symposium (2018) 25. Menz, J., Hirsch, A.K., Li, P., Garg, D.: Compositional security definitions for higher-order where declassification. Proc. ACM Program. Lang. 7(OOPSLA1) (2023) 26. Murray, T., Tiwari, M., Ernst, G., Naumann, D.A.: Assume but verify: Deductive verification of leaked information in concurrent applications. In: ACM Computer and Communications Security (2023). https://doi.org/10.1145/3576915.3623141 27. Nagasamudram, R., Banerjee, A., Naumann, D.A.: Alignment complete relational Hoare logics for some and all. Log. Methods Comput. Sci. 21(4) (2025). https://doi. org/10.46298/LMCS-21(4:21)2025, https://doi.org/10.46298/lmcs-21(4:21)2025 28. Nagasamudram, R., Banerjee, A., Naumann, D.A.: Forall-exists relational verification by filtering to forall-forall (2025), submitted for publication; preprint at https://arxiv.org/abs/2509.04777
20 29. Naumann, D.A.: Thirty-seven years of relational Hoare logic: Remarks on its principles and history. In: 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA) (2020) 30. Paraskevopoulou, Z.: Machine-generated, machine-checked proofs for a verified compiler (experience report) (2026), https://arxiv.org/abs/2602.20082 31. Rival, X., Yi, K.: Introduction to Static Analysis. MIT Press (2020) 32. Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. Journal of Computer Security (2007) 33. Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of DiffieHellman protocols and advanced security properties. In: IEEE Computer Security Foundations Symposium (2012) 34. Soloviev, M., Balliu, M., Guanciale, R.: Security properties through the lens of modal logic. In: IEEE Computer Security Foundations Symposium (2024) 35. The Rocq Development Team: Rocq prover (2026), https://rocq-prover.org/, version 8.20 accessed June 2026 36. Vanhoef, M., Groef, W.D., Devriese, D., Piessens, F., Rezk, T.: Stateful declassification policies for event-driven programs. In: IEEE Computer Security Foundations Symposium (2014) 37. Wang, S.: AI-assisted completion of CertiGC proofs: An experience report. CoRR abs/2606.21167 (2026), https://doi.org/10.48550/arXiv.2606.21167 38. Zdancewic, S., Myers, A.: Robust declassification. In: IEEE Computer Security Foundations Symposium (2001)
Assuming You Knew
A
21
Proofs
The following proof sketches are very similar to the original LATEX document that was given to CC. But they have been revised to be consistent with the machine checked definitions and results. Lemma 1. For every active configuration there is a unique output or • event and unique successor configuration. For every receptive configuration and every input event there is a unique successor configuration for that event. Proof. Direct from definitions. Lemma 2. If gs ⇓ ts and gs ⇓ ts′ then ts = ts′ . Proof. By induction on gs and cases on transition rules. For steps other than input, the argument is direct from Lemma 1. For input, consider a step from ⟨σ⟩ to ⟨c, σ ′ ⟩. By semantics, c is the handler body. Because the program is well specified, c begins with assumeℓ Ax, from which we have that the channel is ℓ and the input value was assigned to variable x. So the event is inℓ n where n is σ ′ (x). For subsequent proofs it is helpful to generalize pre-runs to execution sequences that start from arbitrary initial configuration. Then we define frun(g, ins, n), by recursion on n ∈ N, to be the consecutive sequence of configurations starting from g (but excluding g) and consuming inputs ins until n steps have been taken or all of ins have been handled and a receptive configuration is reached. Lemma 3. For any list ins of input events, there is a unique pre-run gs such that (a) inp(gs) ⪯ ins, (b) last(gs) is receptive, and (c) if inp(gs) ̸= ins, i.e., inp(gs) = ins⇂k for some k < |ins|, then there is an infinite sequence G of lists of active configurations such that, for all i, j we have: |Gi | = i + 1, gs · Gi is a pre-run, inp(gs · Gi ) = ins⇂(k + 1), and i < j ⇒ Gi ⪯ Gj . Proof. If there is some n with |frun(⟨σ0 ⟩, ins, n)| < n then we get (a) and (b) straightforwardly, and have ins consumed which falsifies the antecedent of (c). If |frun(⟨σ0 ⟩, ins, n)| = n for all n then we get (c) as follows. There must be some m, k such that frun(⟨σ0 ⟩, ins, m) has consumed k inputs and reached the receptive configuration that steps to the handler for insk which never terminates. So gs is ⟨σ0 ⟩ · frun(⟨σ0 ⟩, ins, m) and the Gi are defined as the suffixes of frun(⟨σ0 ⟩, ins, m + i). Uniqueness can be shown using determinacy. Lemma 3 is formulated for conceptual clarity. To prove prove Theorems 1 and 2 we actually rely on similar but slightly more intricate properties along these lines: given a pre-run one can extend it in accord with an input list to reach the next visible annotation or output, unless execution diverges. Lemma 4. (a) If t is not ℓ-visible then kℓ (ts · t) = kℓ (ts). (b) If t ∈ Evℓ then kℓ (ts · t) ⊆ kℓ (ts).
22
Proof. (a) is direct from the definition. For (b), suppose ins ∈ kℓ (ts · t), so there are gs, us with ins = inp(us) and gs ⇓ us and visℓ (ts · t) ⪯ visℓ (us). We have visℓ (ts) ⪯ visℓ (ts · t) by definition of visℓ . So gs, us witness ins ∈ kℓ (ts). Lemma 5. (a) kℓ→ (ts) ⊆ kℓ (ts), and (b) if t ∈ Evℓ then kℓ (ts · t) ⊆ kℓ→ (ts). Proof. (a) is direct from the definitions. For (b), suppose ins ∈ kℓ (ts · t). Thus there are gs, us with gs ⇓ us, visℓ (ts · t) ⪯ visℓ (us), and ins = inp(us). Now visℓ (ts · t) = visℓ (ts) · t using t ∈ Evℓ . So there are vs, vs′ with us = vs · t · vs′ and visℓ (us) = visℓ (vs) · t · visℓ (vs′ ). So we get ins ∈ kℓ→ (ts) by instantiating the definition of kℓ→ (ts) with us, t, vs, hs := vs, t, vs′ , gs. Theorem 1. For any gs, ins, and ℓ there are hs and α such that (gs, hs, α) is either a conformance, an assertion or alignment failure, or an assumption or divergence fiat, for ℓ, ins. Furthermore, a given gs, ins, ℓ fits in only one category, although there may be more than one hs, α that witnesses its membership in the category. Proof. For mutual exclusivity see the Rocq proof. Here we show existence. To have a suitable induction hypothesis we show the slightly stronger result that in the conformance case the redex of the last configuration in the minor prerun is an ℓ-annotation only if the last redex in the major pre-run is also an ℓ-annotation. We gloss over that in this sketch. Consider any ℓ and ins, and go by induction on gs. The idea is to explore the minor pre-run hs determined by ins. In the base case, gs is [⟨σ0 ⟩]; we take hs := [⟨σ0 ⟩] and α := {(0, 0)}. This forms a conformance. In the induction case, gs has the form f s · g and by induction we have hs, α with (f s, hs, α) a conformance, fiat, or failure for ℓ, ins. If it is a fiat or failure then so is (f s · g, hs, α), by Lemma 6, and we are done. If ins has been exhausted, i.e., (f s, hs, α) is a conformance such that inp(hs) = ins and last(hs) is receptive, then (f s · g, hs, α) is a conformance and we are done. It remains to consider the case that (f s, hs, α) is a conformance such that α covers f s and either inp(hs) ≺ ins or last(hs) is active. We proceed by cases of last(f s). – If last(f s) is receptive (in which case inp(hs) ≺ ins) and the transition to g is for a visible input on some ℓ′ ⊑ ℓ, then (because the program is well ′ specified) redex(g) is assumeℓ Ax for some x. We construct hs′ ⪰ hs by successive steps, maintaining inp(hs′ ) ⪯ ins, until redex(last(hs′ )) is an ℓannotation, or ins is exhausted and a receptive configuration is reached, or there is divergence without reaching either. • If inp(hs′ ) = ins and last(hs′ ) is receptive, then (f s · g, hs′ , β) is a conformance, where β = α ∪ {(|f s| − 1, j) | |hs| ≤ j ⪯ |hs′ |}. • If an ℓ-annotation is reached at last(hs′ ) then there are three sub-cases: ∗ If the annotation redex(last(hs′ )) is the same as redex(g), and g | last(hs′ ) |= Ax (i.e., sta(g), sta(last(hs′ )) agree on x) then (f s · g, hs′ , γ) is a conformance, where γ = α ∪ {(|f s| − 1, j) | |hs| ≤ j < |hs′ | − 1} ∪ {(|f s|, |hs′ | − 1)}.
Assuming You Knew
23
∗ If the annotation is the same as redex(g) but the states do not agree on x, then (f s · g, hs′ , δ) is an assumption fiat or assertion failure, where δ = α ∪ {(|f s| − 1, j) | |hs| ≤ j < |hs′ | − 1} ∪ {(|f s|, |hs′ | − 1)}. ∗ If redex(last(hs′ )) differs from redex(g) then (f s · g, hs′ , δ) is an alignment failure, where δ is as in the preceding bullet. • If neither ins is exhausted nor an ℓ-annotation reached while growing hs′ , then the minor pre-run is diverging without doing further visible input or output. So (f s · g, hs, α) is a divergence fiat. – If last(f s) is receptive and the transition to g is for a non-visible input, so redex(g) is an assumption for some ℓ′ ̸⊑ ℓ, then (f s·g, hs, α∪{(|f s|, |hs|−1)}) is a conformance. Here we use that redex(last(f s)) cannot be an annotation, so neither can redex(last(hs)) (recall Remark 1). – If last(f s) is active, we have these sub-cases: • If redex(g) is not an ℓ-annotation then (f s · g, hs, α ∪ {(|f s|, |hs| − 1)}) is a conformance that covers f s · g. • If redex(g) is an ℓ-annotation then construct hs′ ⪰ hs by successive steps, maintaining inp(hs′ ) ⪯ ins, until redex(last(hs′ )) is an ℓ-annotation. ∗ If this is not possible because inp(hs′ ) = ins and last(hs′ ) is receptive, then (f s · g, hs′ , β) is a conformance, where β is defined like earlier in this proof. (That is, β = α ∪ {(|f s| − 1, j) | |hs| ≤ j < |hs′ |}.) ∗ If an ℓ-annotation is reached, but redex(last(hs′ )) is different from redex(g), then we obtain an alignment failure. ∗ If redex(last(hs′ )) is the same as redex(g), and the annotation’s formula is Φ such that g, last(hs′ ) |= Φ, then (f s · g, hs′ , γ) is a conformance, where γ = β ∪ {(|f s|, |hs′ | − 1)} for β from above. ∗ If redex(last(hs′ )) is the same as redex(g) but the formula does not hold, we obtain an assumption fiat or assertion failure. ∗ If none of the above apply, then we obtain divergence fiat at i, k where k = |f s| and i is the index of the last ℓ-annotation before k in f s, truncating the minor pre-run where it matches i and restricting α accordingly. Theorem 2. For all ℓ, any pre-run that is safe for ℓ is secure for ℓ. Proof. Consider any ℓ. In accord with the definitions, we consider an arbitrary pre-run and go by induction on it. The base case is the shortest pre-run, [⟨σ0 ⟩], which is secure by definition: it has no prefixes hs · g with hs nonempty. For the induction step, consider a pre-run gs · g that is safe. Safe pre-runs are prefix closed (Lemma 7), so gs is safe, hence gs is secure by induction hypothesis. So to prove gs · g is secure it remains to consider the last step. We must show kℓ (ts · t) ⊇ kℓ→ (ts) ∩ RPℓ (gs · g)
(3)
for the unique (Lemma 2) ts, t that satisfy gs ⇓ ts
gs · g ⇓ ts · t
(4)
24
By Lemma 4(a), we have kℓ (ts · t) = kℓ→ (ts) unless t is ℓ-visible, and this proves (3) for all transitions except for visible t ∈ Evℓ . To prove (3) for t ∈ Evℓ , consider any list of inputs ins. By safety of gs · g for ℓ, ins we have fs, α such that (gs · g, fs, α) is a conformance, assumption fiat, or divergence fiat for ℓ, ins. We must prove that ins ∈ kℓ→ (ts) and ins ∈ RPℓ (gs · g) imply ins ∈ kℓ (ts · t) either by refuting one of the antecedents or by showing the consequent. By definitions, ins ∈ kℓ→ (ts) means there are hs, us, ws and u ∈ Evℓ with ins = inp(us · u · ws)
hs ⇓ us · u · ws
visℓ (ts) ⪯ visℓ (us)
(5)
Also, the goal ins ∈ kℓ (ts · t) means there are fs ′ , vs such that ins = inp(vs)
fs ′ ⇓ vs
visℓ (ts · t) ⪯ visℓ (vs)
(6)
There are quite a number of variables in play so let us review the situation. The major pre-run gs · g has trace ts · t. The minor pre-run hs, with trace us · u, witnesses that inputs ins were possible according to prior knowledge, because visℓ (ts) ⪯ visℓ (us). Safety of gs · g accounts for the inputs ins by a pre-run fs that is either in conformance or is ruled out by assumption or divergence fiat. We complete the proof by cases on whether (gs · g, fs, α) is a conformance, assumption fiat, or divergence fiat. Conformance lets us derive fs ′ such that (6) holds. Assumption fiat lets us refute the policy hypothesis ins ∈ RPℓ (gs · g). Divergence fiat refutes the progress hypothesis ins ∈ kℓ→ (ts). Here are the details. Case conformance: Suppose (gs · g, fs, α) is a conformance for ℓ, ins. So α covers fs and inp(f s) ⪯ ins. We go by the two cases of conformance: either α covers gs · g or ins = inp(fs) and last(fs) is receptive. Suppose α covers gs · g. By coverage and conformance, visℓ (fs) = visℓ (ts · t). (In particular, if t is an input then redex(g) is an assumption about the input value and if t is an output then a preceding assertion ensures agreement on the output value; either way, last(visℓ (fs)) is t.) By inp(fs) ⪯ ins (by conformance) and ins = inp(hs) (by (5)), using determinacy we can extend fs to fs ′ ⪰ fs with ins = inp(vs) where vs are the events of fs ′ , i.e., fs ′ ⇓ vs. So visℓ (ts · t) ⪯ visℓ (vs) and (6) holds for fs ′ , vs. Suppose α does not cover gs · g but ins = inp(fs) and last(fs) is receptive. Let vs satisfy fs ⇓ vs. To show (6) instantiated with fs ′ , vs := fs, vs, it remains to show visℓ (ts · t) ⪯ visℓ (vs). Since last(fs) is receptive, fs is the maximal run on ins, so from (5) using determinacy we have us · u · ws ⪯ fs. By conformance the visible annotations of fs align with those of gs since we consider the case where g isn’t covered, so u must be t and we get visℓ (ts · t) ⪯ visℓ (vs). Case divergence fiat: Suppose (gs · g, fs, α) is a divergence fiat for ℓ, ins. Suppose the divergence fiat is at i, k so that ((gs · g)⇂i, fs, α) is an ℓ-conformance for ins but redex((gs · g)k ) is an ℓ-annotation and neither fs nor any of its continuations reach an ℓ-annotation or ℓ-output as redex. Thus pre-run fs and its continuations are not doing further visible events following last(inp(fs)). Owing
Assuming You Knew
25
to inp(fs) ⪯ ins and determinacy, if the progress condition (5) holds then the handler for last(inp(fs)) progresses at least as far as event u. So divergence fiat contradicts the progress hypothesis ins ∈ kℓ→ (ts). Case assumption fiat: Suppose (gs·g, fs, α) is an assumption fiat for ℓ, ins. Suppose the assumption fiat is at i, j where j = |f s| − 1. Thus ((gs · g)⇂i, fs⇂j, α) is a conformance and redex((gs · g)i ) is an ℓ-assumption of formula Φ (and so is redex(fs j )) but (gs · g)i |fs j ̸|= Φ. Let ins′ be inp(fs⇂j) hence ins′ = inp(fs⇂(j + 1)) = inp(fs), because that step is not an input. Note ins′ ⪯ ins. We now show that the policy hypothesis ins ∈ RPℓ (gs · g) yields a contradiction. Suppose hs′ witnesses ins ∈ RPℓ (gs · g). So ins = inp(us′ ) for the us′ with hs′ ⇓ us′ , and SCℓ ((gs · g), hs′ , β) for some β. But inp(ins) determines hs′ so we have f s ⪯ hs′ and the condition (gs · g)i |fs j ̸|= Φ contradicts SCℓ ((gs · g), hs′ , β).