Renaming or Tightness: Enforcing Disjunctive Information Flow Policies

• URL: http://arxiv.org/abs/2608.09120v1
• Date: Mon, 10 Aug 2026 04:53:10 GMT
• Title: Renaming or Tightness: Enforcing Disjunctive Information Flow Policies
• Abstract summary: A disjunctive policy allows a value to depend on at most one of two secrets and never on both.<n>Hunt and Sands introduced the quantale of information to give them a semantics, leaving the enforcement layer open.<n>We build the flow-sensitive type system family that the quantale calls for, and show that the object which makes such families useful splits in two.
• Score: 7.541234468065092
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: A disjunctive policy allows a value to depend on at most one of two secrets and never on both: an analyst may consult one client's file or the other's, a share of a split secret may be released but not its sibling. Such policies are not lattice-shaped, and Hunt and Sands introduced the quantale of information to give them a semantics, leaving the enforcement layer open. We build the flow-sensitive type system family that the quantale calls for, and show that the object which makes such families useful, the universal type object from which every member specialises, splits in two, with a consequence for enforcement. Over the free commutative quantale on the program variables the whole mechanism survives for every policy: monotone renaming, canonical derivations, principal typings, internal completeness. Over the free object with idempotent generators the certified bound is strictly more precise and still sound, because it records that two reads of one source honour one disjunct. The gap cannot be closed from inside the independent-attribute family: no mechanism of that shape whose labelling maps support monotone renaming certifies a bound more precise than the first, and for principal typings under generator-exact homomorphic specialisation the two coincide. Under the ethical-wall and secret-sharing labels the second read of a disjunctive source therefore drives every such certificate to no guarantee, and programs that satisfy the policy are rejected. The literal transcription of the lattice-era object is no escape either: it is a further quotient that loses branch disjunction. Precision is recovered by deferring specialisation to the judgement level, and the resulting read-out map is the least sound join-preserving one.

Related papers

• Differentially Private Semantic Plans for Aggregate Insight Generation [4.832750949021042]
  We introduce textttDP-SPIN, a trusted-curator framework for aggregate measurement and summarization over semantic concepts.<n>We evaluate textttDP-SPIN under record-level privacy on CFPB complaint narratives, Amazon All Beauty reviews, and Yelp restaurant reviews.
  arXiv  Detail & Related papers  (2026-09-14T19:39:26Z)
• Capability-Gated Language Models: Security Composes, Utility Does Not [0.0]
  Security composes: provably at meets under a monotone-elicitation assumption we falsify pointwise.<n>In two lineages the median held-out meet deepens suppression; the one effect surviving correction strengthens it.
  arXiv  Detail & Related papers  (2026-08-31T22:35:49Z)
• Canonicalization Failures as a Recurring Vulnerability Class: Representation Divergence in Cryptographic Systems and Its Avoidance [0.0]
  This work organizes the scattered findings systematically.<n>It shows that they are instances of one violated uniqueness condition, along two basic directions.<n>The contribution is explicitly not the discovery of the phenomenon, but is threefold.
  arXiv  Detail & Related papers  (2026-08-06T18:47:32Z)
• Self-Certification of Representation Adequacy: Sequential Certification at Minimum Task Loss [4.6304326752276985]
  This paper develops a four-layer theory of self-certification of representation adequacy.<n>The sequential layer poses certification as an optimal-stopping problem in the currency of task loss.<n>A final boundary layer identifies the open theorem needed to cover policy switching or representation repair.
  arXiv  Detail & Related papers  (2026-08-03T14:09:34Z)
• A Compositional Theory of Causally Masked Transformers [50.88598486616582]
  We develop a formalization that derives expressivity directly from the model's implemented dynamics.<n>Each attention head updates its own state independently within a layer.<n>A modified form of soft attention supports irreversible, checklist-like state.
  arXiv  Detail & Related papers  (2026-07-29T14:47:19Z)
• Operational Identity: A Finite Audit of Declared and Implemented Rules of Sameness [0.0]
  A system can apply consistently and with every record individually correct, a rule of sameness that no artifact declares.<n>A declared identity regime partitions a finite record domain into co-reference classes.<n>A disclosed mechanism induces an operational identity partition of the same domain.
  arXiv  Detail & Related papers  (2026-07-22T21:02:37Z)
• From ambiguous utterances to governed reuse classes: canonicalization, quotient invariance, and conditional decidability [0.0]
  Reuse should operate on a mathematically characterized quotient of resolved conversational demands.<n> Reuse identity licenses the governed query key and its certified answer space.<n>The supporting layer is stated at exactly the strength proved.
  arXiv  Detail & Related papers  (2026-07-11T01:49:04Z)
• What Accuracy and Gradient Cosine Miss: Evaluating Feedback Alignment via Scale Stability, Reference Validity, and Depth Utility [48.10132234701036]
  We propose a diagnostic evaluation protocol based on three checks -- scale stability, reference validity, and depth utility -- together with per-layer rather than aggregate cosine reporting.<n>Across multiple architectures and methods, our protocol identifies all failures with wide calibration margins.
  arXiv  Detail & Related papers  (2026-06-19T06:04:17Z)
• Geometric Factual Recall in Transformers [57.48371649045765]
  A common view casts internal weight matrices as associative memories over pairs of embeddings, requiring memorization counts that scale linearly with the number of facts.<n>We develop a theoretical and empirical account of an alternative, emphgeometric form of memorization in which learned embeddings encode structure directly.<n>In a controlled setting where a single-layer transformer must memorize random vectors from subjects to a shared attribute set, we prove that a logarithmic embedding dimension suffices.<n>We extend these results to the multi-hop setting, providing constructions with and without chain-of-thought that exhibit a provable
  arXiv  Detail & Related papers  (2026-05-12T17:22:22Z)
• Language-Guided Open-World Anomaly Segmentation [81.13615952207685]
  We propose Clipomaly, the first CLIP-based open-world and anomaly segmentation method for autonomous driving.<n>Our zero-shot approach requires no anomaly-specific training data and leverages CLIP's shared image-text embedding space to segment unknown objects.<n>Our model dynamically extends its vocabulary at inference time without retraining, enabling robust detection and naming of anomalies beyond common class definitions.
  arXiv  Detail & Related papers  (2025-12-01T09:08:59Z)
• Graded Modal Types for Integrity and Confidentiality [0.25782420501870285]
  Graded type systems allow different properties of a program to be tracked via annotating types with additional information. One example is information flow control, in which types are graded by a lattice of security levels allowing noninterference properties to be automatically verified and enforced. Integrity, a property specifying that trusted outputs must not depend on untrusted inputs, has not been examined in this context. We analogize the situation to recent work on embedding both linear uniqueness and types in a graded framework, and use this framing to demonstrate that we can enforce both integrity and confidentiality alongside one another.
  arXiv  Detail & Related papers  (2023-09-08T13:40:52Z)
• Collective Robustness Certificates: Exploiting Interdependence in Graph Neural Networks [71.78900818931847]
  In tasks like node classification, image segmentation, and named-entity recognition we have a classifier that simultaneously outputs multiple predictions. Existing adversarial robustness certificates consider each prediction independently and are thus overly pessimistic for such tasks. We propose the first collective robustness certificate which computes the number of predictions that are simultaneously guaranteed to remain stable under perturbation.
  arXiv  Detail & Related papers  (2023-02-06T14:46:51Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.