{"id":"525eb90b-d0ac-407c-ab17-06ea3af1189c","arxiv_id":"2608.00882","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A corrected, machine-checked proof shows that relational safety implies epistemic security for reactive programs with declassification annotations.","lead":"This paper fixes a flawed 2018 proof that a program safety condition guarantees information flow security, and reports that the corrected proof is machine checked in the Rocq proof assistant. It matters because carefully controlled release of secret data can then be specified and enforced with much higher assurance.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Central claim rests on a temporary, unhashed Rocq artifact; without checking the formal theorem statement and axiom foundation, Theorem 2 cannot be independently confirmed.","rationale":"Both the reader and I identify the same load-bearing vulnerability: the machine-checked proof cannot be audited from the manuscript as submitted, because the Rocq artifact is temporary, unversioned, and not hashed, and because the prose gives only proof sketches. This is especially important because the paper is a correction of a paper whose original proof had a significant flaw; the entire value added over CN is the machine-checked assurance. The condition is concrete and addressable: provide a permanent, versioned artifact and show that the Rocq theorem statement matches the LaTeX definitions. I examined the underlying definitions and did not find an independent mathematical inconsistency in the prose; the safety/security framework is coherent and the proof sketch in Appendix A is plausible. Thus the correct final verdict remains conditional on artifact availability and faithfulness, with no change from the reader's verdict.","tokens_in":18859,"tokens_out":8686,"duration_ms":82634,"concrete_test":"Download the tarball from Section 7, record its SHA-256, and compile it with Rocq 8.20. Then run `Print Assumptions safe_implies_secure.` and `Print safe_implies_secure.`, comparing the printed statement with Eqn. (1) and Theorem 2; also grep for `admit`, `Admitted`, and non-classical `Axiom`. If the statement matches and the only axioms are classical_extensionality and excluded_middle, the concern is resolved; if the artifact is unavailable or any extra assumption appears, the central claim is not independently supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The strongest claim is 'safety implies security, with a fully machine checked proof in Rocq'. The paper's own Section 7 says the code is available only through a temporary tarball (temp_assumeKnow.tgz) and that a permanent location is planned; no commit hash or checksum is given. The Appendix proof of Theorem 2 is explicitly a sketch, and Theorem 1's mutual-exclusivity part is deferred to the Rocq code. The nonstandard definitions (semi-proper alignment, fiats, release policy in Eqn. (1), progress knowledge) are intricate, and Section 7 reports that the AI assistant repeatedly produced wrong statements, including a plausible but wrong formalization of Lemma 3 and a tendency to strengthen assumptions in lemmas. If any Rocq lemma silently strengthens an assumption, or if `safe_implies_secure` is stated over a different RP or alignment relation than the LaTeX version, the machine-checked result would not establish the theorem as printed. The manuscript also imports classical extensionality and excluded-middle axioms; those are acceptable, but the reader cannot currently verify that no further axioms are present. This is a verifiability gap in the central claim, not evidence of a specific mathematical error.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":19093,"tokens_out":3546,"duration_ms":33756,"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":[{"comment":"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.","section":"§7, final paragraph; Appendix A"},{"comment":"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.","section":"Appendix A, remark following Lemma 3"},{"comment":"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).","section":"§5.2, Theorem 1; Appendix A, proof of Theorem 1"}],"minor_comments":[{"comment":"Typos: \"appoach\" should be \"approach\" and \"develpment\" should be \"development\" in the opening paragraphs.","section":"§1"},{"comment":"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.","section":"§3.3"},{"comment":"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.","section":"§4.2"},{"comment":"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.","section":"§7"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is honest about the provenance of the formalization, and the AI-assistant narrative is not itself a reason for rejection. The decision should hinge on whether the authors can provide a stable, inspectable Rocq artifact together with a precise statement of what is proved. If they cannot, the machine-checked claim would have to be downgraded to a verified-with-unavailable-code claim, which would materially weaken the contribution."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This paper fixes the known flaw in the CN 2018 framework for epistemic flow policies: it corrects the release policy definition, revises progress knowledge to use prefix rather than equality, and machine-checks the safety-implies-security theorem in Rocq. The main theorem is now backed by a real artifact, not just a sketch. The paper is honest about the process, including that the AI assistant proposed a plausible but wrong formalization of Lemma 3 and tended to strengthen assumptions. That transparency works in its favor.\n\nWhat is actually new: the revised release policy, the prefix-based knowledge definitions, and the classification theorem with mutual exclusivity of conformance, fiats, and failures. The correction of the flawed RP is the core contribution, and the machine-checked proof supplies the missing assurance. The claim that safety implies security is now supported by a complete proof; the previous proof had a hole, and filling it in a proof assistant is real progress. The self-citation to CN is the object being corrected, not a crutch.\n\nSoft spots: the artifact is only available as a temporary tarball with no commit hash or checksum. The appendix proof of Theorem 2 is explicitly a sketch, and the exclusivity part of Theorem 1 is deferred to the Rocq code. Given the intricate nonstandard definitions, an independent reader cannot currently confirm that the Rocq statements match the LaTeX. That is a verifiability gap, not evidence of an error. The AI-experience section is interesting but tangential to the security result; the paper should not be judged by the novelty of the tooling. The reliance on classical axioms is unremarkable and not a concern.\n\nWho should read it: people working on declassification semantics, epistemic security, and machine-checked verification of information-flow properties. It deserves a serious referee. The main acceptance condition should be a persistent, pinned repository for the Rocq development so the claims can be independently checked. As it stands, I trust the author's description but cannot verify the central artifact myself; that is the one thing standing between this and a clean accept.","headline":"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.","tokens_in":19546,"tokens_out":2291,"would_cite":true,"duration_ms":20629,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A checked proof repairs the semantics of declassification.","keywords":["information flow security","declassification","epistemic logic","relational annotations","safety implies security","machine-checked proof","agentic AI coding assistant"],"falsifier":"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.","tokens_in":18665,"feed_emoji":"🔒","tokens_out":7720,"duration_ms":65697,"temperature":0.7,"pith_summary":"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.","feed_headline":"A checked proof repairs the semantics of declassification","feed_subtitle":"A corrected epistemic theory shows that assumption-based flow policies can be enforced by safety monitoring.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"The original CSF 2018 paper whose release-policy definition and proof are corrected here.","marker":"[17]"},{"why":"The earlier monitoring framework from which the safety condition and the classification idea are adapted.","marker":"[16]"},{"why":"The proof assistant used to machine check the formal development.","marker":"[35]"},{"why":"The agentic AI coding assistant that helped translate and complete the proof.","marker":"[2]"}],"fun_headline_variants":["Machine-checked proof fixes declassification semantics","Safety now implies security in flow policies","Agentic AI aids machine-checked policy fix","Corrected epistemic semantics for declassification","Every safe run is secure: a checked theorem"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Machine-checked proof fixes declassification semantics","Safety now implies security in flow policies","Agentic AI aids machine-checked policy fix","Corrected epistemic semantics for declassification","Every safe run is secure: a checked theorem"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000901,"raw_usage":{"total_tokens":3827,"prompt_tokens":844,"completion_tokens":2983,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":460,"completion_tokens_details":{"reasoning_tokens":2917}},"tokens_in":460,"tokens_out":2983,"duration_ms":21379,"temperature":1.0,"reasoning_tokens":2917,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T15:14:32.949808+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"In: IEEE Computer Security Foundations Sym- posium (2014)","cited_arxiv_id":null,"evidence_quote":"The earlier monitoring framework from which the safety condition and the classification idea are adapted."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The proof assistant used to machine check the formal development."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The agentic AI coding assistant that helped translate and complete the proof."}],"review_version":2}