Pith. sign in

REVIEW 3 major objections 5 minor 52 references

An Algebraic Approach to Asymmetric Delegation and Polymorphic Label Inference (Technical Report)

T0 review · 3 major / 5 minor · reviewed 2026-08-16 · deepseek-v4-flash

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

Pith's one-line read One witness principal determines whether a label may be safely downgraded under nonmalleable information flow.

desk verdict 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. read the letter →

arxiv 2504.20432 v2 pith:YLONH2D3 submitted 2025-04-29 cs.PL cs.CR

Silei Ren , Coşku Acay , Andrew C. Myers This is my paper · ORCID
classification cs.PLcs.CR
keywords informationflowcontrolasymmetricdelegationnonmalleablelabelinferenceboundedpolymorphismlatticeofprincipalsprimefilters
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

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.

What carries the argument

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$.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
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 / 5 minor

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.

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 (3)
  1. [Appendix C, proof of Theorem 6] 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.
  2. [Section 5.2, Definition 7] 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.
  3. [Section 6.2, proof of Theorem 8] 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.
minor comments (5)
  1. [Throughout] 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.
  2. [Section 4] Theorem 3 is stated without proof; a one-line proof would make the hyperproperty-transformer intuition precise.
  3. [Appendix C, Theorem 6 proof] 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.
  4. [Section 6.2, proof of Theorem 8] 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.
  5. [Section 6.3] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the semantic characterization is derived from external lattice/Stone-duality facts, and the algorithms implement rather than assume the semantics.

full rationale

The derivation chain is not circular. NMIF and uncompromised labels (Definition 6) are taken from prior work [9] as external semantic properties; Theorem 4 is proved from Definitions 1-6 using Theorem 9 (Prime Ideal/Filter, a standard external result) and the Stone representation of distributive lattices (Theorems 1-2). The proof in Appendix B does not assume Theorem 4 in its own derivation: the forward direction constructs a valid attacker from a filter/ideal separation, and the reverse direction is a direct closure argument. Theorem 4 is therefore a genuine derived equivalence, not a restatement of an input. Algorithm 3 is a syntactic rendering of the existential witness of Theorem 4 via the mintheta helper of Definition 7; since Theorem 4 is already established, using mintheta_i(q) as the witness is an implementation choice rather than a fitted input renamed as a prediction. The only self-reference in the paper is '[36]', which is the same technical report; the cited proofs are actually present in Appendices A-D, so the self-citation is not load-bearing. There are genuine correctness concerns unrelated to circularity: Definition 7 postulates a unique mintheta(p) and an oracle for join-prime factorizations without proof, and the termination argument for Algorithm 2 in Appendix C ('a chain cannot be longer than 2', 'no longer than 2|theta|') is not a valid decreasing measure and does not relate the recursive calls of Min-Pick and Min-Factor. These are unproved assumptions or invalid proof steps, but they do not make the derivation equivalent to its inputs by construction.

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

The paper fits no numerical parameters. Its assumptions are structural: distributivity of P, the join-prime factorization oracle, and the valid-attacker restriction. These are stated explicitly but the join-prime oracle is an extra structural requirement that is not constructed or verified in the implementation.

assumptions (4)
  • domain assumption The lattice of principals P is distributive (a Heyting algebra).
    Invoked in Section 3.1 (footnote 5) and used in the proofs of Theorems 2 and 4 via Stone representation and the prime ideal/filter theorem; without it the attacker-as-prime-filter model may fail.
  • ad hoc to paper Every principal has a join-prime factorization, and minθ(p) is unique.
    Assumed in Section 5.2 (Definition 7 and the paragraph introducing the factorization oracle) to make Algorithms 2 and 3 terminating and well-defined; the paper does not construct this oracle.
  • domain assumption Valid attackers satisfy I ⊆ C (they control no more integrity than confidentiality).
    Definition 5 restricts the attacker model so that NMIF is non-vacuous; the paper justifies it by prior work [46,47] and cryptographic attacker classes, but it excludes 'malicious but incurious' attackers.
  • domain assumption Delegation contexts are finite sets of acts-for rules and the semantics of consistency is as in Definition 1.
    The attacker model and all algorithms are relative to this finitary representation; the paper notes this is compatible with FLAM, Rx, and DLM.

how reviews work

0 comments
Cite this review

Pith. "Pith review of An Algebraic Approach to Asymmetric Delegation and Polymorphic Label Inference (Technical Report)." pith.science (2026). https://pith.science/paper/YLONH2D3

@misc{pith2026250420432,
  author       = {Pith},
  title        = {Pith review of: An Algebraic Approach to Asymmetric Delegation and Polymorphic Label Inference (Technical Report)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YLONH2D3}},
  note         = {Machine review of arXiv:2504.20432}
}
read the original abstract

Language-based information flow control (IFC) enables reasoning about and enforcing security policies in decentralized applications. While information flow properties are relatively extensional and compositional, designing expressive systems that enforce such properties remains challenging. In particular, it can be difficult to use IFC labels to model certain security assumptions, such as semi-honest agents. Motivated by these modeling limitations, we study the algebraic semantics of lattice-based IFC label models, and propose a semantic framework that allows formalizing asymmetric delegation, which is partial delegation of confidentiality or integrity. Our framework supports downgrading of information and ensures their safety through nonmalleable information flow (NMIF). To demonstrate the practicality of our framework, we design and implement a novel algorithm that statically checks NMIF and a label inference procedure that efficiently supports bounded label polymorphism, allowing users to write code generic with respect to labels.

Figures

Figures reproduced from arXiv: 2504.20432 by the authors.

Figure 1
Figure 1. Yao’s Millionaires’ problem in Viaduct [3]. The programmer must manu￾ally assign labels to hosts. 1 host Alice , Bob 2 assume Alice = Bob for integrity 3 4 val a : { Alice } = Alice . input 5 val b : { Bob } = Bob . input 6 val w : { Alice ⊔ Bob } = a > b 7 8 Alice . output ( 9 declassify w to { Alice }) 10 Bob . output ( 11 declassify w to { Bob }) [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 3
Figure 3. The lattice of labels (L, ≤) and the lattice of information flow (L, ⊑) share the same underlying set, but use a different ordering. The dotted line depicts labels with equal confidentiality and integrity: strictly above are compromised labels, and on or below are uncompromised labels. should make it easier for programs to be considered secure. To express delegation, we extend prior definitions of IFC security hyper… view at source ↗
Figure 4
Figure 4. The average function is implicitly polymorphic over the labels of its arguments. 6.1 Bounded Label Polymorphism As in traditional type systems, allowing code that is generic over labels increases expressiveness significantly. Existing IFC-based languages like Jif [34] and Flow Caml [40] support bounded label polymorphism, which allows functions to be parameterized over labels that are bounded by specified security l… view at source ↗
Figures from the paper (2 more)
Figure 6
Figure 6. Figure 6: Syntax of principal constraints. Label and Principal Constraints [PITH_FULL_IMAGE:figures/full_fig_p014_6.png]
Figure 7
Figure 7. Figure 7: Translating label constraints to principal constraints. axioms of Heyting algebra (e.g., associativity, absorption, distributivity, etc.) until no left-hand side of any constraint can be further simplified. As equational axioms are syntactic rewrites, it does not chang…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

52 extracted references · 28 canonical work pages

  1. [1]

    In: 11th ACM SIGPLAN Int’l Conf

    Abadi, M.: Access control in a core calculus of dependency. In: 11th ACM SIGPLAN Int’l Conf. on Functional Programming. pp. 263–273. ACM, New York, NY, USA (2006). https://doi.org/10.1145/1159803.1159839

    arXiv 2006

  2. [2]

    In: van der Meyden, R., van der Torre, L

    Abadi, M.: Variations in access control logic. In: van der Meyden, R., van der Torre, L. (eds.) Deontic Logic in Computer Science, Lecture Notes in Com- puter Science, vol. 5076, pp. 96–109. Springer Berlin Heidelberg (2008). https://doi.org/10.1007/978-3-540-70525-3_9

    work page doi:10.1007/978-3-540-70525-3_9 2008

  3. [3]

    In: 42nd ACM SIG- PLAN Conf

    Acay, C., Recto, R., Gancher, J., Myers, A., Shi, E.: Viaduct: An extensible, optimizing compiler for secure distributed programs. In: 42nd ACM SIG- PLAN Conf. on Programming Language Design and Implementation (PLDI). pp. 740–755. ACM (Jun 2021). https://doi.org/10.1145/3453483.3454074

    arXiv 2021

  4. [4]

    In: 28th IEEE Computer Security Foundations Symp

    Arden, O., Liu, J., Myers, A.C.: Flow-limited authorization. In: 28th IEEE Computer Security Foundations Symp. (CSF). pp. 569–583 (Jul 2015). https://doi.org/10.1109/CSF.2015.42

    doi:10.1109/csf.2015.42 2015

  5. [5]

    In: 29th IEEE Computer Security Foundations Symp

    Arden, O., Myers, A.C.: A calculus for flow-limited authorization. In: 29th IEEE Computer Security Foundations Symp. (CSF). pp. 135–147 (Jun 2016). https://doi.org/10.1109/CSF.2016.17

    doi:10.1109/csf.2016.17 2016

  6. [6]

    In: 2012 IEEE 25th Computer Security Founda- tions Symposium

    Askarov, A., Chong, S.: Learning is change in knowledge: Knowledge-based security for dynamic policies. In: 2012 IEEE 25th Computer Security Founda- tions Symposium. pp. 308–322 (2012). https://doi.org/10.1109/CSF.2012.31

    work page doi:10.1109/csf.2012.31 2012

  7. [7]

    Biba, K.J.: Integrity considerations for secure computer systems. Tech. Rep. ESD-TR-76-372, USAF Electronic Systems Division, Bedford, MA (Apr 1977), https://ban.ai/multics/doc/a039324.pdf, (Also available through National Technical Information Service, Springfield Va., NTIS AD-A039324.)

    work page 1977

  8. [8]

    Blok, W.J., Pigozzi, D.: Algebraizable Logics (1989)

    work page 1989

Show all 52 references
  1. [9]

    In: 24th ACM Conf

    Cecchetti, E., Myers, A.C., Arden, O.: Nonmalleable information flow control. In: 24th ACM Conf. on Computer and Communications Security (CCS). pp. 1875–1891. ACM (Oct 2017). https://doi.org/10.1145/3133956.3134054

    2017

  2. [10]

    In: 21st ACM Symp

    Chong, S., Liu, J., Myers, A.C., Qi, X., Vikram, K., Zheng, L., Zheng, X.: Secure web applications via automatic partitioning. In: 21st ACM Symp. on Operating System Principles (SOSP). pp. 31–44 (Oct 2007). https://doi. org/10.1145/1323293.1294265

    2007

  3. [11]

    In: 16th USENIX Security Symp

    Chong, S., Vikram, K., Myers, A.C.: SIF: Enforcing confidentiality and integrity in web applications. In: 16th USENIX Security Symp. (Aug 2007), http://www.cs.cornell.edu/andru/papers/sif.pdf

    2007

  4. [12]

    In: 21st IEEE Computer Security Foundations Symp

    Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: 21st IEEE Computer Security Foundations Symp. (CSF). pp. 51–65 (Jun 2008). https://doi.org/ 10.1109/CSF.2008.7

    2008 doi

  5. [13]

    Denning, D.E.: A lattice model of secure information flow. Comm. of the ACM 19(5), 236–243 (1976). https://doi.org/10.1145/360051.360056

    1976

  6. [14]

    BCS Learn- ing & Development Ltd, Swindon, GBR (2017)

    Dolan, S.: Algebraic subtyping: Distinguished Dissertation 2017. BCS Learn- ing & Development Ltd, Swindon, GBR (2017)

    2017

  7. [15]

    In: 16th ACM Conf

    Fournet, C., le Guernic, G., Rezk, T.: A security-preserving compiler for distributed programs: From information-flow policies to cryptographic mech- anisms. In: 16th ACM Conf. on Computer and Communications Security (CCS). pp. 432–441 (Nov 2009), https://doi.org/10.1145/16536...

    2009

  8. [16]

    In: 35th ACM Symp

    Fournet, C., Rezk, T.: Cryptographically sound implementations for typed information-flow security. In: 35th ACM Symp. on Principles of Program- ming Languages (POPL). pp. 323–335 (Jan 2008), https://doi.org/10.1145/ 1328438.1328478

    2008

  9. [17]

    In: 19th IEEE Computer Security Foundations Workshop (CSFW) (2006)

    Garg, D., Pfenning, F.: Non-interference in constructive authorization logic. In: 19th IEEE Computer Security Foundations Workshop (CSFW) (2006). https://doi.org/10.1109/CSFW.2006.18

    2006 doi

  10. [18]

    In: IEEE Symp

    Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symp. on Security and Privacy. pp. 11–20 (Apr 1982). https://doi.org/10. 1109/SP.1982.10014

    1982

  11. [19]

    In: IEEE Symp

    Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: IEEE Symp. on Security and Privacy. pp. 75–86 (Apr 1984). https://doi.org/10. 1109/SP.1984.10019

    1984

  12. [20]

    In: 2020 IEEE 33rd Computer Security Foundations Symposium (CSF)

    Hirsch, A.K., Amorim, P.H.A.d., Cecchetti, E., Tate, R., Arden, O.: First- order logic for flow-limited authorization. In: 2020 IEEE 33rd Computer Security Foundations Symposium (CSF). pp. 123–138 (2020). https://doi. org/10.1109/CSF49147.2020.00017

    2020

  13. [21]

    CCS ’13, Association for Computing Machinery, New York, NY, USA (2013)

    Hirsch, A.K., Clarkson, M.R.: Belief semantics of authorization logic. CCS ’13, Association for Computing Machinery, New York, NY, USA (2013). https://doi.org/10.1145/2508859.2516667

    2013

  14. [22]

    Hirt, M., Maurer, U.M.: Player simulation and general adversary structures in perfect multiparty computation. J. Cryptol.13(1), 31–60 (2000). https: //doi.org/10.1007/S001459910003

    2000 doi

  15. [23]

    Foundations and Trends in Privacy and Security3(1), 1–102 (2022)

    Kozyri, E., Chong, S., Myers, A.C.: Expressing information flow properties. Foundations and Trends in Privacy and Security3(1), 1–102 (2022). https: //doi.org/10.1561/3300000008

    2022 doi

  16. [24]

    In: 6th IEEE Computer Security Foundations Workshop (CSFW)

    Landauer, J., Redmond, T.: A lattice of information. In: 6th IEEE Computer Security Foundations Workshop (CSFW). pp. 65–70. IEEE Computer Society Press (Jun 1993). https://doi.org/10.1109/CSFW.1993.246638

    1993

  17. [25]

    ACM Transactions on Information and System Security (TISSEC)6(1), 128–171 (2003)

    Li, N., Grosof, B.N., Feigenbaum, J.: Delegation logic: A logic-based approach to distributed authorization. ACM Transactions on Information and System Security (TISSEC)6(1), 128–171 (2003). https://doi.org/10.1145/605434. 605438

    2003 doi

  18. [26]

    Li, P., Zhang, D.: Towards a general-purpose dynamic information flow policy (2021), https://arxiv.org/abs/2109.08096

    2021 arXiv

  19. [27]

    In: USENIX Security Symposium

    Matetic, S., Schneider, M., Miller, A., Juels, A., Capkun, S.: Delegatee: Brokered delegation using trusted execution environments. In: USENIX Security Symposium. pp. 1387–1403 (2018)

    2018

  20. [28]

    In: 26th IEEE Computer Security Foundations Symp

    Montagu, B., Pierce, B.C., Pollack, R.: A theory of information-flow labels. In: 26th IEEE Computer Security Foundations Symp. (CSF). pp. 3–17 (Jun 2013). https://doi.org/10.1109/CSF.2013.8 19

    2013 doi

  21. [29]

    Myers, A.C.: Mostly-Static Decentralized Information Flow Control. Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA (Jan 1999)

    1999

  22. [30]

    In: 16th ACM Symp

    Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: 16th ACM Symp. on Operating System Principles (SOSP). pp. 129–142 (Oct 1997). https://doi.org/10.1145/268998.266669

    1997

  23. [31]

    ACM Transactions on Software Engineering and Methodology9(4), 410–442 (Oct 2000)

    Myers, A.C., Liskov, B.: Protecting privacy using the decentralized label model. ACM Transactions on Software Engineering and Methodology9(4), 410–442 (Oct 2000). https://doi.org/10.1145/363516.363526

  24. [32]

    In: 17th IEEE Computer Security Foundations Workshop (CSFW)

    Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification. In: 17th IEEE Computer Security Foundations Workshop (CSFW). pp. 172–186 (Jun 2004). https://doi.org/10.1109/CSFW.2004.9

    2004 doi

  25. [33]

    Journal of Computer Security14(2), 157–196 (2006)

    Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification and qualified robustness. Journal of Computer Security14(2), 157–196 (2006). https://doi.org/10.3233/JCS-2006-14203

    2006 doi

  26. [34]

    Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: Jif 3.0: Java information flow (Jul 2006), http://www.cs.cornell.edu/jif, software release, http://www.cs.cornell.edu/jif

    2006

  27. [35]

    In: 3rd International Symposium on Static Analysis

    Rehof, J., Mogensen, T.A.: Tractable constraints in finite semilattices. In: 3rd International Symposium on Static Analysis. pp. 285–300. No. 1145 in Lecture Notes in Computer Science, Springer-Verlag (Sep 1996). https: //doi.org/10.1007/3-540-61739-6_48

    1996 doi

  28. [36]

    https://doi.org/10.48550/arXiv.2504.20432

    Ren, S., Acay, C., Myers, A.C.: An algebraic approach to asymmetric delegation and polymorphic label inference (technical report) (Apr 2025). https://doi.org/10.48550/arXiv.2504.20432

    2025 doi arXiv

  29. [37]

    Oliver and Boyd (1965)

    Rutherford, D.E.: Introduction to Lattice Theory. Oliver and Boyd (1965)

    1965

  30. [38]

    IEEE Journal on Selected Areas in Communications 21(1), 5–19 (Jan 2003)

    Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (Jan 2003). https://doi.org/10.1109/JSAC.2002.806121

    2003

  31. [39]

    In: 4th European Symp

    Sandhu, R.S.: Role hierarchies and constraints for lattice-based access con- trols. In: 4th European Symp. on Research in Computer Security (ESORICS) (Sep 1996)

    1996

  32. [40]

    Technical Report 0282, Institut National de Recherche en Informatique et en Automatique (INRIA) (Jul 2003)

    Simonet, V.: The Flow Caml System: documentation and user’s manual. Technical Report 0282, Institut National de Recherche en Informatique et en Automatique (INRIA) (Jul 2003)

    2003

  33. [41]

    https://doi.org/10.1109/csf61375.2024.00009

    Soloviev, M., Balliu, M., Guanciale, R.: Security properties through the lens of modal logic (2023). https://doi.org/10.1109/csf61375.2024.00009

    2023

  34. [42]

    In: Laud, P

    Stefan, D., Russo, A., Mazières, D., Mitchell, J.C.: Disjunction category labels. In: Laud, P. (ed.) Proceedings of the 16th Nordic conference on In- formation Security Technology for Applications. Lecture Notes in Computer Science, vol. 7161, pp. 223–239. Springer (2011). htt...

    2011

  35. [43]

    Časopis pro pěstování matematiky a fysiky067(1), 1–25 (1938)

    Stone, M.H.: Topological representations of distributive lattices and brouwe- rian logics. Časopis pro pěstování matematiky a fysiky067(1), 1–25 (1938). https://doi.org/10.21136/CPMF.1938.124080

    1938

  36. [44]

    In: 19th IEEE Computer Security Foundations 20 Workshop (CSFW)

    Swamy, N., Hicks, M., Tse, S., Zdancewic, S.: Managing policy updates in security-typed languages. In: 19th IEEE Computer Security Foundations 20 Workshop (CSFW). pp. 202–216 (Jul 2006). https://doi.org/10.1109/CSFW. 2006.17

    2006 doi

  37. [45]

    In: 23 rd annual IEEE Symposium on Foundations of Computer Science

    Yao, A.C.: Protocols for secure computations. In: 23 rd annual IEEE Symposium on Foundations of Computer Science. pp. 160–164 (1982). https://doi.org/10.1109/SFCS.1982.38

    1982 doi

  38. [46]

    In: 32nd IEEE Computer Security Foundations Symp

    Zagieboylo, D., Suh, G.E., Myers, A.C.: Using information flow to design an ISA that controls timing channels. In: 32nd IEEE Computer Security Foundations Symp. (CSF) (Jun 2019). https://doi.org/10.1109/CSF.2019. 00026

    2019 doi

  39. [47]

    In: 14th IEEE Computer Security Foundations Workshop (CSFW)

    Zdancewic, S., Myers, A.C.: Robust declassification. In: 14th IEEE Computer Security Foundations Workshop (CSFW). pp. 15–23 (Jun 2001). https: //doi.org/10.1109/CSFW.2001.930133

    2001

  40. [48]

    ACM Trans

    Zdancewic, S., Zheng, L., Nystrom, N., Myers, A.C.: Secure program par- titioning. ACM Trans. on Computer Systems20(3), 283–328 (Aug 2002). https://doi.org/10.1145/566340.566343

    2002

  41. [49]

    ACM Trans

    Zhang, D., Myers, A.C., Vytiniotis, D., Peyton Jones, S.: SHErrLoc: A static holistic error locator. ACM Trans. on Programming Languages and Systems 39(4), 18 (Aug 2017), http://dl.acm.org/citation.cfm?id=3121137

    2017

  42. [50]

    In: IEEE Symp

    Zheng, L., Chong, S., Myers, A.C., Zdancewic, S.: Using replication and partitioning to build secure distributed systems. In: IEEE Symp. on Security and Privacy. pp. 236–250 (May 2003). https://doi.org/10.1109/SECPRI. 2003.1199340

    2003 arXiv

  43. [51]

    In: 9th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS) (Aug 2014)

    Zheng, L., Myers, A.C.: A language-based approach to secure quorum replication. In: 9th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS) (Aug 2014). https://doi.org/10.1145/ 2637113.2637117 21 A Details for Section 3 (Semantic Framework) Theorem 1...

    2014

  44. [52]

    As rule Min-Pick and rule Min-F actorare both decreasing, the algorithm eventually reaches the base case and then terminates

    So each chain starting at minθ(p) is no longer than 2|θ|, which is finite. As rule Min-Pick and rule Min-F actorare both decreasing, the algorithm eventually reaches the base case and then terminates. Minimal elements are unique and algorithm 2 always terminates, so it suffice...

Pith tools

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