Pith. sign in

REVIEW 3 major objections 4 minor 38 references

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

T0 review · 3 major / 4 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A checked proof repairs the semantics of declassification.

desk verdict A machine-checked correction of a flawed but influential flow-policy framework; the central theorem is credible, but the artifact must be pinned down before acceptance. read the letter →

arxiv 2608.00882 v1 pith:XMADZBO5 submitted 2026-08-01 cs.AI cs.CRcs.LOcs.PL

David A. Naumann This is my paper · ORCID
classification cs.AIcs.CRcs.LOcs.PL
keywords informationflowsecuritydeclassificationepistemiclogicrelationalannotationssafetyimpliesmachine-checkedproofagenticAIcodingassistant
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper repairs a flawed 2018 formalization of declassification policies for information-flow security. It defines what an observer at a security level may know, expresses downgrading through assume annotations in program code, and proves that a program-oriented condition called safety implies the epistemic security property. The proof is machine checked, so the corrected definitions carry the assurance of a formal proof. If the result holds, policy authors can state conditional releases in code and enforce them by monitoring safety, without losing an extensional meaning for the policy.

What carries the argument

The load-bearing machinery is an alignment relation between a major pre-run and a minor pre-run: a monotone, prefix-closed pairing of configuration indices that matches corresponding occurrences of annotations in the two runs. Semi-proper alignment (used for release policy) matches only ℓ-assumptions; proper alignment (used for safety) matches all ℓ-annotations. From alignments come conformance, which says the minor run satisfies every matched annotation, and the release policy RPℓ, the set of input lists that an observer is allowed to consider possible. The proof of Theorem 2 uses Eq. (1) and the classification theorem (Theorem 1) to show that every alternative input list is either conformance-covered, contradicted by its own divergence, or excluded by an assumption fiat.

What would settle it

Inspect the formal development for any use of 'admit', 'axiom', or an unproven assumption, and compare the code's definitions of release policy and security with Section 4; if the code differs on RPℓ or uses an axiom beyond classical logic, the paper's claim that safety implies security is not established by that code.

Watch

Extended reading notes

Core claim

The central claim is Theorem 2: for every security level ℓ, every pre-run that is safe for ℓ is secure for ℓ. Security is stated as Eq. (1): at each step, the observer's knowledge after a visible event must be no smaller than the intersection of their progress knowledge before the step and the release policy RPℓ. Safety is a purely program-oriented classification of every alternative input list as a conformance, an assumption or divergence fiat, or an assertion or alignment failure; fiats and failures are discarded or refute the security antecedents. The paper's correction to the 2018 version makes release policy a predicate on pre-runs rather than on observed event traces, which is what allows the main proof to go through. The machine-checked development confirms the announced corrections and also exposes further details, such as the need for prefix rather than equality in the knowledge definitions.

Load-bearing premise

If the machine-checked development contains an admitted axiom or diverges from the paper's prose definition of RPℓ, the checked theorem no longer supports the stated result.

Editorial extensions

If this is right

  • An enforcement strategy becomes available: safety is stated so that it can be checked by induction over execution steps, so a runtime monitor can reject programs whose pre-runs are unsafe.
  • Policy writers can keep assume annotations in code while treating the release policy as an extensional object: Eq. (1) says exactly which input histories the observer may believe are possible.
  • The corrected proof validates the repair announced for the 2018 paper and supplies a machine-checked baseline for future work on relational annotations.
  • Because the framework is simple and general, it can serve as a common semantics for comparing different declassification policy styles and for lifting existing verification techniques.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The alignment-based safety condition could plausibly be extended to robust declassification, where the adversary also controls declassified inputs; the paper's definitions already make the distinction between visible and non-visible inputs explicit.
  • The machine-checked development suggests a practical audit recipe for other flawed conference formalizations: state the correction, formalize it with an AI assistant, and check for hidden assumptions the prose missed.
  • A testable next step is to build the ideal monitor suggested by Theorem 1 and test whether enforcing safety at runtime accepts programs that a direct epistemic monitor would flag, and vice versa.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper revises the epistemic semantics for information-flow policies originally proposed in the CSF 2018 paper "Assuming You Know" (CN). It redefines the release policy so that it is a predicate on pre-runs rather than on observed event traces, introduces a corrected safety condition, and claims the main theorem that safety implies security (Theorem 2), with a proof machine-checked in the Rocq proof assistant. The development was carried out with the assistance of an agentic AI coding tool (Claude Code), and the paper reports extensively on that experience.

Significance. If the machine-checked formalization is faithful to the paper's definitions, this is a valuable contribution: it provides a corrected, validated semantics for declassification by assumptions, gives a clean separation between the release policy and the security condition, and demonstrates that the announced corrections to CN are essentially sound. The use of machine checking is a genuine strength, as is the candid account of how the AI assistant was used and where it made mistakes. However, the central claim currently cannot be independently verified from the manuscript alone, because the Rocq development is available only through a temporary tarball with no checksum or permanent archive, and the paper defers key parts of the proof (notably mutual exclusivity in Theorem 1) to that code.

major comments (3)
  1. [§7, final paragraph; Appendix A] The central evidence for Theorem 2 is the claim of a fully machine-checked Rocq proof, but the artifact is not part of the manuscript and is available only via a temporary tarball with no commit hash or checksum. The paper states that a permanent location is planned. Without a stable, inspectable artifact that states the exact theorem proved (and its axioms beyond classical extensionality and excluded middle, which are mentioned in §7), the reader cannot verify that the machine-checked result matches the LaTeX definitions and Theorem 2. This is a load-bearing verifiability gap, not a cosmetic one.
  2. [Appendix A, remark following Lemma 3] The paper states: "Lemma 3 is formulated for conceptual clarity. To prove Theorems 1 and 2 we actually rely on similar but slightly more intricate properties along these lines." This explicitly acknowledges that the lemma stated in the body is not the one used in the proofs. Since Lemma 3 underpins the construction of the minor pre-run in the proofs of Theorems 1 and 2, the actual lemma and its proof should be stated in the paper or, failing that, the Rocq development containing it must be made available in a verifiable form. As it stands, the proof chain has a missing link.
  3. [§5.2, Theorem 1; Appendix A, proof of Theorem 1] The proof of Theorem 1 says "For mutual exclusivity see the Rocq proof" and gives only a sketch for existence. The mutual-exclusivity part is essential because Theorem 2's case analysis (conformance, assumption fiat, divergence fiat) relies on the classification being exhaustive and exclusive. Deferring this to code that is not available with the paper makes the published proof incomplete on a point that the paper itself identifies as having been problematic in earlier work (Section 7 notes that CC initially proposed an unconvincing counterexample to exclusivity).
minor comments (4)
  1. [§1] Typos: "appoach" should be "approach" and "develpment" should be "development" in the opening paragraphs.
  2. [§3.3] The parenthetical remark "unless two channels have identical handlers!" is informal; the formal condition is introduced only in §3.4. Consider adding a forward reference when the wrinkle is first mentioned.
  3. [§4.2] The definition of semi-proper alignment uses equality of redexes to express "exactly the same occurrence in the program text," but redex equality alone does not identify occurrences if two annotations are syntactically identical. The remark about unique identifying labels should be made part of the formal definition if it is used in the machine-checked development.
  4. [§7] The report on the AI-assisted development is interesting and candid, but it is substantially longer than the technical proofs in the appendix. If the artifact is made available, consider moving some of the AI-interaction details to a separate appendix or supplement so that the technical content remains the focus.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: Theorem 2 is derived from independent definitions with a machine-checked Rocq proof; the temporary unhashed artifact is a verifiability gap, not circularity.

full rationale

The paper's central claim, Theorem 2, states that safety implies security. Safety (Section 5.1) is defined without reference to observations, release policy, or the knowledge operators: it is phrased in terms of aligned pre-run pairs, conformances, assertion/alignment failures, and assumption/divergence fiats. Security (Section 4.2, Eqn. (1)) is defined independently via the knowledge sets k_l and k_l^→ and the release policy RP_l. The release policy is itself defined from semi-conformances, i.e., from the agreement of declassifying assumptions in aligned pre-runs. The proof of Theorem 2 (Appendix A) genuinely uses safety to pick, for each input list, either a conformance (which establishes the consequent through the release-policy hypothesis), an assumption fiat (which contradicts membership in RP_l), or a divergence fiat (which contradicts the progress-knowledge hypothesis). These are three mathematically distinct cases, not notational variants of one another. The derivation is therefore not self-definitional: safety is not defined in terms of security, and security is not defined in terms of safety. The self-citation to CN [17] is the flawed object being corrected, not a load-bearing authority; no uniqueness theorem or nonstandard axiom is imported from the authors' prior work to force the conclusion. The cited machine-checked work [26] is used for comparison, not as the basis of Theorem 2. The paper's own Section 7 reports that the Rocq development is only temporarily available (https://www.cs.stevens.edu/~naumann/pub/temp_assumeKnow.tgz) with no commit hash or checksum, and that the Appendix proof of Theorem 2 is a sketch while Theorem 1's mutual-exclusivity part is deferred to the Rocq code. Section 7 also candidly reports that the AI assistant produced a plausible but wrong formalization of Lemma 3 and had a tendency to strengthen assumptions in lemmas. These are important verifiability and provenance limitations: an independent reader cannot currently confirm that the machine-checked theorem statement matches the LaTeX definitions, or that no hidden axioms are present beyond the stated classical extensionality and excluded-middle imports. But a reproducibility gap is not circularity. Nothing in the paper reduces Theorem 2 to its own inputs, fits a parameter and calls it a prediction, or renames a known result as a derivation. The derivation is self-contained relative to the stated definitions, and the honest finding is no significant circularity.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No numbers are fitted and no new entities are postulated. The proof relies on standard classical logic axioms, the well-specified program model, and the unverified-in-paper faithfulness of the Rocq artifact.

assumptions (3)
  • standard math Classical extensionality and excluded-middle axioms are assumed (imported into the Rocq development).
    Section 7 states the initial Rocq file imports 'classical extensionality and excluded-middle axioms.' These are standard in classical theorem proving but go beyond constructive logic.
  • domain assumption Programs are well specified: every handler begins with assume ℓ A x, and every output is immediately preceded by assert ℓ' A e.
    Section 3.4 imposes this condition and argues it loses no generality. It is used to prove trace determinacy (Lemma 2) and in the classification argument (Theorem 1) and security proof.
  • ad hoc to paper The Rocq development, available only through a temporary URL, faithfully formalizes the definitions in this paper and compiles.
    The paper claims a fully machine-checked proof of Theorem 2, but the code is not included and the URL is temporary with no commit hash. The entire central claim depends on this artifact being complete and faithful.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI." pith.science (2026). https://pith.science/paper/XMADZBO5

@misc{pith2026260800882,
  author       = {Pith},
  title        = {Pith review of: Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XMADZBO5}},
  note         = {Machine review of arXiv:2608.00882}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2608.00882 by the authors.

Figure 1
Figure 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 jus￾tified 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 spe… view at source ↗

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

38 extracted references · 34 canonical work pages

  1. [1]

    In: ACM Conference on Pro- gramming Language Design and Implementation (2021)

    Acay, C., Recto, R., Gancher, J., Myers, A.C., Shi, E.: Viaduct: an extensible, optimizing compiler for secure distributed programs. In: ACM Conference on Pro- gramming Language Design and Implementation (2021)

    work page 2021

  2. [2]

    Anthropic: Claude code (2026), https://claude.com/claude-code, version using model Opus 4.8, accessed June 2026

    work page 2026

  3. [3]

    In: IEEE Symposium on Security and Privacy (2007)

    Askarov, A., Sabelfeld, A.: Gradual release: Unifying declassification, encryption and key release policies. In: IEEE Symposium on Security and Privacy (2007)

    work page 2007

  4. [4]

    IEEE Computer Security Foundations Symposium (2009)

    Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. IEEE Computer Security Foundations Symposium (2009)

    work page 2009

  5. [5]

    In: IEEE Computer Security Foundations Symposium (2016)

    Assaf, M., Naumann, D.A.: Calculational design of information flow monitors. In: IEEE Computer Security Foundations Symposium (2016)

    work page 2016

  6. [6]

    In: ACM Workshop on Programming Languages and Analysis for Security (2011)

    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)

    work page 2011

  7. [7]

    In: IEEE Symposium on Security and Privacy (2008) Assuming You Knew 19

    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

    work page 2008

  8. [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. ACM68(8) (2025)

    work page 2025

Show all 38 references
  1. [9]

    In: IEEE Computer Security Foundations Symposium (2020)

    Bay, J., Askarov, A.: Reconciling progress-insensitive noninterference and declas- sification. In: IEEE Computer Security Foundations Symposium (2020)

    2020

  2. [10]

    In: Asian Sym- posium on Programming Languages and Systems (2012)

    Beringer, L.: End-to-end multilevel hybrid information flow control. In: Asian Sym- posium on Programming Languages and Systems (2012)

    2012

  3. [11]

    In: Tools and Algo- rithms for the Construction and Analysis of Systems (2024)

    Beutner, R.: Automated software verification of hyperliveness. In: Tools and Algo- rithms for the Construction and Analysis of Systems (2024)

    2024

  4. [12]

    In: ACM Computer and Communications Security (2009)

    Bohannon, A., Pierce, B.C., Sjöberg, V., Weirich, S., Zdancewic, S.: Reactive non- interference. In: ACM Computer and Communications Security (2009)

    2009

  5. [13]

    In: ACM Symposium on Principles of Programming Languages (2010)

    Broberg, N., Sands, D.: Paralocks: role-based information flow control and beyond. In: ACM Symposium on Principles of Programming Languages (2010)

    2010

  6. [14]

    In: IEEE Computer Security Foun- dations Symposium (2025), https://doi.org/10.1109/CSF64896.2025.00029

    Cecchetti, E.: Nonmalleable progress leakage. In: IEEE Computer Security Foun- dations Symposium (2025), https://doi.org/10.1109/CSF64896.2025.00029

    2025

  7. [15]

    In: ACM Computer and Communications Security

    Cecchetti, E., Myers, A.C., Arden, O.: Nonmalleable information flow control. In: ACM Computer and Communications Security. pp. 1875–1891 (2017)

    2017

  8. [16]

    In: IEEE Computer Security Foundations Sym- posium (2014)

    Chudnov, A., Kuan, G., Naumann, D.A.: Information flow monitoring as abstract interpretation for relational logic. In: IEEE Computer Security Foundations Sym- posium (2014)

    2014

  9. [17]

    In: IEEE Computer Security Foun- dations Symposium (2018)

    Chudnov, A., Naumann, D.A.: Assuming you know: Epistemic semantics of rela- tional annotations for expressive flow policies. In: IEEE Computer Security Foun- dations Symposium (2018). https://doi.org/10.1109/CSF.2018.00021, corrected version dated July 29, 2018 has been availa...

    2018

  10. [18]

    Journal of Computer Security 18(6) (2010)

    Clarkson, M.R., Schneider, F.B.: Hyperproperties. Journal of Computer Security 18(6) (2010)

    2010

  11. [19]

    Dardinier, T., Müller, P.: Hyper Hoare logic: (dis-)proving program hyperproper- ties. Proc. ACM Program. Lang.8(PLDI) (2024)

    2024

  12. [20]

    Foundations and Trends®in Theoretical Computer Science9(3–4) (2014)

    Dwork, C., Roth, A., et al.: The algorithmic foundations of differential privacy. Foundations and Trends®in Theoretical Computer Science9(3–4) (2014)

    2014

  13. [21]

    In: IEEE Computer Security Foundations Symposium (2022)

    Li, P., Zhang, D.: Towards a general-purpose dynamic information flow policy. In: IEEE Computer Security Foundations Symposium (2022)

    2022

  14. [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)

    2017

  15. [23]

    In: ACM Computer and Communications Security (2023)

    McCall, M., Bichhawat, A., Jia, L.: Tainted secure multi-execution to restrict at- tacker influence. In: ACM Computer and Communications Security (2023)

    2023

  16. [24]

    In: IEEE Computer Security Foundations Symposium (2018)

    McCall, M., Zhang, H., Jia, L.: Knowledge-based security of dynamic secrets for reactive programs. In: IEEE Computer Security Foundations Symposium (2018)

    2018

  17. [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)

    2023

  18. [26]

    In: ACM Computer and Communications Security (2023)

    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

    2023

  19. [27]

    org/10.46298/LMCS-21(4:21)2025, https://doi.org/10.46298/lmcs-21(4:21)2025

    Nagasamudram, R., Banerjee, A., Naumann, D.A.: Alignment complete relational Hoarelogicsforsomeandall.Log.MethodsComput.Sci.21(4)(2025).https://doi. org/10.46298/LMCS-21(4:21)2025, https://doi.org/10.46298/lmcs-21(4:21)2025

    2025 doi

  20. [28]

    Nagasamudram, R., Banerjee, A., Naumann, D.A.: Forall-exists relational verifi- cation by filtering to forall-forall (2025), submitted for publication; preprint at https://arxiv.org/abs/2509.04777 20

    2025 arXiv

  21. [29]

    In: 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA) (2020)

    Naumann, D.A.: Thirty-seven years of relational Hoare logic: Remarks on its prin- ciples and history. In: 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA) (2020)

    2020

  22. [30]

    Paraskevopoulou, Z.: Machine-generated, machine-checked proofs for a verified compiler (experience report) (2026), https://arxiv.org/abs/2602.20082

    2026

  23. [31]

    MIT Press (2020)

    Rival, X., Yi, K.: Introduction to Static Analysis. MIT Press (2020)

    2020

  24. [32]

    Journal of Computer Security (2007)

    Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. Journal of Computer Security (2007)

    2007

  25. [33]

    In: IEEE Computer Security Foundations Symposium (2012)

    Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie- Hellman protocols and advanced security properties. In: IEEE Computer Security Foundations Symposium (2012)

    2012

  26. [34]

    In: IEEE Computer Security Foundations Symposium (2024)

    Soloviev, M., Balliu, M., Guanciale, R.: Security properties through the lens of modal logic. In: IEEE Computer Security Foundations Symposium (2024)

    2024

  27. [35]

    The Rocq Development Team: Rocq prover (2026), https://rocq-prover.org/, ver- sion 8.20 accessed June 2026

    2026

  28. [36]

    Vanhoef, M., Groef, W.D., Devriese, D., Piessens, F., Rezk, T.: Stateful declassifi- cationpoliciesforevent-drivenprograms.In:IEEEComputerSecurityFoundations Symposium (2014)

    2014

  29. [37]

    CoRR abs/2606.21167(2026), https://doi.org/10.48550/arXiv.2606.21167

    Wang, S.: AI-assisted completion of CertiGC proofs: An experience report. CoRR abs/2606.21167(2026), https://doi.org/10.48550/arXiv.2606.21167

    2026 doi arXiv

  30. [38]

    Zdancewic, S., Myers, A.: Robust declassification. In: IEEE Computer Security Foundations Symposium (2001) Assuming You Knew 21 A 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 consiste...

    2001

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.