{"id":"2c33def8-5a35-4cd0-a125-5633a17111d1","arxiv_id":"2504.20432","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper gives a lattice-based semantic model of asymmetric delegation for IFC and sound and complete algorithms for NMIF checking and bounded-polymorphic label inference.","lead":"This paper develops a semantic framework for information flow control labels that models asymmetric delegation, where one principal delegates confidentiality or integrity but not both. It contributes sound and complete algorithms for checking nonmalleable information flow and for label inference with bounded polymorphism, with an implementation in the Viaduct compiler.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 6's termination proof is invalid and Definition 7's minθ is assumed without proof, so the soundness/completeness of the NMIF check (Theorems 6–7) is not established as written.","rationale":"The reader's weakest assumption identifies the oracle/minθ machinery and the inconsistent termination proof of Algorithm 2; I agree that this is the load-bearing spot. The semantic framework (Theorems 1–4) is credible: it is an application of Stone duality for distributive lattices, and small finite examples check out. One additional formal gap is that the space of attackers A is never defined in Definition 1/2; Theorem 2 only makes sense if A is the set of prime filters, so the semantics needs one clarifying sentence. That gap is fixable and secondary. The main issue is the algorithmic claim: Theorem 7's sound/complete NMIF check is inherited from Theorem 6, and the submitted proof of Theorem 6 is invalid as written. The theorem may well be true for finite principal lattices with a factorization oracle, and Algorithm 2's termination can likely be proved by a |θ|-based measure, but that proof is absent. Theorem 8 is also only sketched, and the experimental section contains no benchmark numbers or reproducibility details beyond a code URL. These are presentation and proof gaps, not demonstrable falsehoods, so a conditional acceptance is the right call; I would not reject the paper.","tokens_in":17855,"tokens_out":39823,"duration_ms":419741,"concrete_test":"Independently re-derive termination of Algorithm 2 by defining a well-founded measure, e.g., the lexicographic pair (|θ|, number of join-prime factors of the current principal), and prove it decreases under every application of Min-Pick and Min-Factor. If the measure exists, the theorem holds and the defect is a proof gap; if not, enumerate all delegation contexts of size ≤3 over the 6-element distributive lattice 2×3 to look for a divergent or non-minimal run, which would refute Theorem 6.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Appendix C's proof of Theorem 6 does not prove termination. The relation ⪰ is defined by 'minθ(p) ⪰ minθ(q) if join-prime(q)', which is already reflexive when q=p and does not relate the recursive calls actually made by Algorithm 2; the claims 'a chain cannot be longer than 2' and 'each chain ... is no longer than 2|θ|' are unsupported, and no decreasing measure is supplied for the alternation of Min-Pick and Min-Factor. Definition 7 postulates a unique minθ(p) with θ|=p≤q iff minθ(p)⇒q, but existence is not proved and the paper only assumes an oracle for join-prime factorization. Because Algorithm 3 invokes minθi(q) and Theorem 7 is proved from Theorems 5 and 6, the paper currently fails to establish that the static NMIF check terminates and decides Definition 6. The semantic characterization (Theorem 4) is plausible and I found no counterexample in small distributive lattices, but the algorithmic half of the central claim is not backed by a valid proof.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This technical report develops an algebraic semantic framework for IFC labels with asymmetric delegation. Labels are pairs ⟨p,q⟩ of principals, delegation is a pair of contexts (θc, θi), and the central semantic result (Theorem 4) characterizes the NMIF-safe (uncompromised) labels as exactly those for which a witness principal r satisfies θi |= q ≤ r and θc |= r ≤ p. The paper then presents decision procedures: Algorithm 1 decides acts-for, Algorithm 2 computes a minimal representative minθ(p), Algorithm 3 checks uncompromised labels, and a constraint solver supports bounded label polymorphism. The framework is evaluated by extending the Viaduct compiler with delegation syntax and label inference.","tokens_in":18080,"tokens_out":8030,"duration_ms":85592,"significance":"The paper's conceptual contribution is real and useful: it connects delegation contexts to attacker models via prime filters, provides a clean witness criterion for safe downgrading, and gives a pragmatic route to polymorphic label inference over an algebraic model. The statement and proof structure are explicit, and the acts-for algorithm (Algorithm 1, Theorem 5) and the semantic characterization appear sound. However, the algorithmic core of the NMIF check and the constraint solver relies on a postulated oracle and contains proofs that do not establish termination. As written, the central claim that the static NMIF check and the label inference procedure are sound, complete, and terminating is not yet supported. That is a load-bearing gap.","major_comments":[{"comment":"The termination argument is internally inconsistent. It first says that a chain cannot be longer than 2 and then that each chain is no longer than 2|θ|; these two bounds are not reconciled. Moreover, the relation ⪰ is defined by 'minθ(p) ⪰ minθ(q) if join-prime(q)', which is reflexive when q = p and does not relate the recursive calls actually made by Algorithm 2: Min-Pick changes θ and replaces p by p∧q′, while Min-Factor replaces p by a join of join-prime components. No decreasing measure is supplied for the alternation of these rules, so Theorem 6 is not proved. Since Theorem 7 and Algorithm 3 depend on Theorem 6, the termination of the NMIF check is not established as written.","section":"Appendix C, proof of Theorem 6"},{"comment":"The minimal principal minθ(p) is introduced as a necessarily unique principal satisfying θ|=p≤q iff minθ(p)⇒q, but the paper provides no proof of existence or uniqueness and no construction of minθ(p) from the assumed join-prime factorization oracle. The surrounding text says only that the authors rely on an oracle for join-prime factorizations; no argument is given that such factorizations suffice to produce minθ(p). Because Algorithm 3 invokes minθi(q) and Theorem 7 is proved from Theorems 5 and 6, the NMIF decision procedure is currently contingent on an unverified oracle. The authors should either prove existence and uniqueness under explicit assumptions on P or state the oracle as an additional hypothesis of Theorems 6 and 7.","section":"Section 5.2, Definition 7"},{"comment":"The termination proof for the constraint solver is conditional in a way that does not match the theorem statement. It says the well-founded relation is well-founded 'in practice when M is a finite map and P is a finite lattice', but P has not been assumed finite at this point in the paper. The formalized update rule f(M) also does not mention the delegation contexts θ, constraints with constant left-hand sides, or the failure check. Finally, the proof concludes that iteration reaches the greatest fixpoint, while the theorem claims the minimal-authority solution; the paper does not explain how these notions coincide under its ordering. Thus Theorem 8 is not proved as stated.","section":"Section 6.2, proof of Theorem 8"}],"minor_comments":[{"comment":"The phrase 'Proofs can be found in the technical report [36]' is circular because [36] is this same technical report; the text should refer directly to the appendices.","section":"Throughout"},{"comment":"Theorem 3 is stated without proof; a one-line proof would make the hyperproperty-transformer intuition precise.","section":"Section 4"},{"comment":"In the definition of the relation ⪰, the condition 'if join-prime(q)' appears to be a typo; as written it does not constrain the expression p being reduced.","section":"Appendix C, Theorem 6 proof"},{"comment":"The proof says the update iteration reaches the 'greatest fixpoint' while Theorem 8 claims the 'minimum-authority solution'; the ordering convention should be clarified so that the direction of the fixed point is aligned with the stated result.","section":"Section 6.2, proof of Theorem 8"},{"comment":"The empirical claim that type inference 'terminates within 300 milliseconds' is reported without benchmark details; the paper should include the number and nature of the benchmarks, or a table with timing data.","section":"Section 6.3"}],"recommendation":"major_revision","confidential_remarks":"The stress-test concern about the termination proof of Theorem 6 and the unverified oracle in Definition 7 is accurate and should be addressed before publication. The issues are localized to the algorithmic appendices and appear repairable, so I would not reject the paper on these grounds if the authors can supply a constructive treatment of minθ and a valid termination argument for the NMIF check."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The core idea here is worth taking seriously. Modeling asymmetric delegation as a pair of delegation contexts (θc, θi) and characterizing uncompromised labels via a witnessing principal (Theorem 4) is a clean, plausible extension of the FLAM/FLAC line. The prime-filter attacker model is a nice piece of algebra, and the semantic development in Sections 3–4 is coherent. I checked the proof of Theorem 4 in the appendix and it follows from standard prime ideal/filter separation, modulo a few typos. The related work is handled honestly, and the paper is self-contained relative to its definitions.\n\nThe soft spots are real, and they are exactly where the reader and stress-test point. The termination proof of Algorithm 2 in Appendix C is not a proof. The relation ⪰ is stated with two clauses that do not obviously well-order the recursive calls, the claim that a chain cannot be longer than 2 is unsupported, and the conclusion 'no longer than 2|θ|' is both unexplained and inconsistent with the preceding sentence. Since Definition 7 postulates a unique minθ(p) and Algorithm 3 relies on that value, Theorems 6 and 7 are not established as written. This is a load-bearing flaw, but it feels fixable: a proper measure on (θ, p) would likely do the job, and the soundness argument for the Min rules is plausible. The paper should also state clearly whether existence of minθ(p) is assumed or derived from the join-prime factorization oracle; right now the assumption is implicit. Theorem 8's proof is a sketch in the same style—plausible but not rigorous enough as published. The empirical evaluation is one sentence about 300ms on a MacBook Air; no numbers, no benchmark table, so the practicality claim is essentially unvalidated.\n\nIf I were refereeing this, I would recommend major revision rather than rejection. The semantic contribution is solid and likely citable, and the algorithmic issues are localized. The paper deserves a serious referee who can dig into the lattice theory and check whether the termination measure can be repaired. I would bring it to a reading group and cite the semantic framework, but not the decision procedure as a proved result until the appendix is fixed.","headline":"The semantic framework for asymmetric delegation is genuinely new and the central Theorem 4 looks right, but the proof of termination for the NMIF decision procedure is broken as written, so the algorithmic half needs another pass.","tokens_in":18630,"tokens_out":4614,"would_cite":true,"duration_ms":48524,"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":"One witness principal determines whether a label may be safely downgraded under nonmalleable information flow.","keywords":["information flow control","asymmetric delegation","nonmalleable information flow","label inference","bounded label polymorphism","lattice of principals","prime filters"],"falsifier":"Take the smallest non-distributive lattice, the diamond $M_3$, with two delegation contexts and enumerate labels: if Algorithm 3 accepts a label that fails the existential-witness condition of Theorem 4, or rejects one that satisfies it, the claimed soundness and completeness fail. Alternatively, give two different join-prime factorizations of the same principal to the $\\min_\\theta$ oracle; any difference in the resulting NMIF verdict shows the method is oracle-dependent.","tokens_in":17637,"feed_emoji":"🔐","tokens_out":6979,"duration_ms":66495,"temperature":0.7,"pith_summary":"The paper claims that asymmetric delegation, where a principal delegates confidentiality and integrity separately, can be given a precise algebraic semantics rather than ad-hoc syntax. The central result is that a label $\\langle p,q\\rangle$ is safe to downgrade under nonmalleable information flow exactly when some principal $r$ satisfies $\\theta_i \\models q \\le r$ and $\\theta_c \\models r \\le p$. If this characterization holds, checking downgrade safety reduces to two acts-for decisions, and label inference with bounded polymorphism can be solved directly over the principal lattice. The paper presents terminating algorithms for these checks and reports that they work in practice.","feed_headline":"Safe downgrading reduces to a single witness principal","feed_subtitle":"An algebraic check makes asymmetric delegation checkable and labels inferable in one pass.","key_machinery":"The load-bearing identity is Theorem 4, the witness-principal characterization of uncompromised labels: $\\langle\\theta_c,\\theta_i\\rangle \\models \\blacktriangledown\\langle p,q\\rangle \\iff \\exists r\\in P.\\ (\\theta_i \\models q \\le r) \\land (\\theta_c \\models r \\le p)$. The argument runs on two supporting constructions: attackers-as-prime-filters, which gives delegation contexts a concrete model as consistent truth assignments, and the minimal-principal operation $\\min_\\theta(p)$, computed from join-prime factorizations, which replaces existential search for $r$ with a syntactic check. The solver additionally uses the relative pseudocomplement of the meet to solve constraints of the form $Y^\\pi \\land p_1 \\Rightarrow_\\pi P^\\pi_2$.","core_discovery":"The paper's central discovery is an algebraic characterization of when a label is uncompromised, hence safe to downgrade, under asymmetric delegation. With separate delegation contexts for confidentiality ($\\theta_c$) and integrity ($\\theta_i$), a label $\\langle p,q\\rangle$ is uncompromised iff there exists a principal $r$ with $\\theta_i \\models q \\le r$ and $\\theta_c \\models r \\le p$. The intuition is that $r$ witnesses that the label is at least as trusted as it is secret after both delegation contexts are applied. The paper proves this equivalence semantically from an attacker model built from prime filters, restricted to valid attackers, and then turns the characterization into Algorithm 3, which checks $\\theta_c \\vdash \\min_{\\theta_i}(q) \\le p$ and is proved sound and complete. The same algebraic machinery drives a constraint solver for bounded polymorphic labels that always terminates with the minimum-authority solution or reports failure.","pith_inferences":["The witness-principal characterization suggests a duality: confidentiality and integrity delegations are two halves of one acts-for relation, and safety is exactly the existence of an interpolant $r$; an analogous interpolant condition may govern other combined security hyperproperties.","The join-prime factorization oracle is the practical lever: implementing it for infinite or symbolically defined principal lattices, or approximating it lazily, would determine whether the approach scales beyond finite name sets.","One testable extension is to use the same $\\min_\\theta$ machinery for dynamic delegation, recomputing the witness $r$ incrementally when the context changes at runtime and turning the static check into a runtime monitor.","The constraint solver's minimum-authority solutions could be compared against greedy or heuristic label assignments on larger programs to see whether the optimality guarantee translates into measurable performance gains in secure compilation."],"forward_implications":["Nonmalleable downgrade safety becomes a decidable static check: a compiler can reject any declassification or endorsement whose label fails the witness-principal condition.","In the special case where confidentiality and integrity share one delegation context, the check collapses to the familiar acts-for test $q \\le p$, recovering prior NMIF enforcement.","Adding more delegation assumptions can only shrink the attacker set, so a program verified under fewer assumptions remains secure under more, supporting modular and separately compilable security policies.","Bounded polymorphic functions can be type-checked once and reused at many security levels, eliminating the exponential monomorphic specialization blow-up of nested calls.","Because inference targets the underlying algebra rather than a fixed label syntax, extending the principal set or adding delegations does not invalidate existing analyses."],"supporting_citations":[{"why":"Defines nonmalleable information flow and the notion of compromised labels that the paper's safety check must enforce.","marker":"[9]"},{"why":"Supplies the prime-filter representation of distributive lattices that identifies attackers with consistent truth assignments in Theorem 2.","marker":"[43]"},{"why":"Gives the fixed-point method for solving semi-lattice constraints that the label constraint solver adapts.","marker":"[35]"},{"why":"Introduces bounded label polymorphism in a prior IFC language, the baseline the inference procedure generalizes.","marker":"[34]"},{"why":"Provides the compiler and benchmarks used to evaluate the delegation syntax and one-pass label inference.","marker":"[3]"},{"why":"Contributes the delegation-based label model over a lattice of principals that the framework formalizes semantically.","marker":"[4]"},{"why":"Defines robust declassification, the confidentiality half that NMIF combines with transparent endorsement.","marker":"[47]"}],"fun_headline_variants":["One witness principal: safe downgrading decidable","Single witness check for asymmetric delegation safety","Algebraic labels: one check for delegation and inference","Safe delegation via a single witness principal","One pass: check NMIF and infer polymorphic labels"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole decision procedure leans on an oracle that produces join-prime factorizations and a unique minimal principal for every element of a distributive principal lattice; if the lattice is not distributive or that factorization is unavailable, Theorem 4's check and the algorithms built on it have no defined behavior.","fun_headline_variants_meta":{"raw":{"variants":["One witness principal: safe downgrading decidable","Single witness check for asymmetric delegation safety","Algebraic labels: one check for delegation and inference","Safe delegation via a single witness principal","One pass: check NMIF and infer polymorphic labels"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000471,"raw_usage":{"total_tokens":2311,"prompt_tokens":880,"completion_tokens":1431,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":496,"completion_tokens_details":{"reasoning_tokens":1361}},"tokens_in":496,"tokens_out":1431,"duration_ms":11102,"temperature":1.0,"reasoning_tokens":1361,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T05:29:14.596211+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take the smallest non-distributive lattice, the diamond $M_3$, with two delegation contexts and enumerate labels: if Algorithm 3 accepts a label that fails the existential-witness condition of Theorem 4, or rejects one that satisfies it, the claimed soundness and completeness fail. Alternatively, give two different join-prime factorizations of the same principal to the $\\min_\\theta$ oracle; any difference in the resulting NMIF verdict shows the method is oracle-dependent.","supporting_citations":[{"cited_title":"In: 3rd International Symposium on Static Analysis","cited_arxiv_id":null,"evidence_quote":"Gives the fixed-point method for solving semi-lattice constraints that the label constraint solver adapts."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces bounded label polymorphism in a prior IFC language, the baseline the inference procedure generalizes."}],"review_version":1}