Sound Enforcement of Dynamic Release Information Flow Policy-Full Version
- URL: http://arxiv.org/abs/2608.09506v2
- Date: Wed, 19 Aug 2026 04:49:25 GMT
- Title: Sound Enforcement of Dynamic Release Information Flow Policy-Full Version
- Abstract summary: We present the first type system that enforces dynamic release policy and formally prove its soundness.<n>We formalize a core language that enables dynamic release policy and develop a type system that checks dynamic release policy.<n>We also implement a prototype of the type system as an extension to the Rust language.
- Score: 3.774259890134901
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Information flow analysis is the de facto method of assessing confidentiality and integrity issues. However, the widespread adoption of information flow analysis in real-world systems is still lacking, partly due to a fundamental gap between theory and practice: the dynamic nature of security concerns in real-world systems goes beyond the scope of existing techniques that assume a static policy (i.e., data secrecy does not change). Recognizing the fundamental gap, a substantial amount of research has studied various aspects of it (e.g., enabling declassification, endorsement, and invocation policies). A recent work takes a step further by formalizing a promising end-to-end policy called dynamic release that unifies prior formalizations by allowing information flow restrictions to downgrade and upgrade in arbitrary ways. However, how to soundly enforce the powerful dynamic release policy is still an open question. In this paper, we present the first type system that enforces dynamic release policy and formally prove its soundness. More specifically, we (1) formalize a core language that enables dynamic release policy, (2) develop a type system that checks dynamic release policy, (3) develop new proof techniques and formally prove that the type system enforces dynamic release policy, and (4) implement a prototype of the type system as an extension to the Rust language, along with case studies on conference reviewing system and Civitas.
Related papers
- PolicyMem: Geometric Policy Memory for LLM Governance [72.04962480384322]
We introduce PolicyMem, a geometric policy memory that externalizes natural-language policies as reusable geometric memory objects.<n>A memory writer compiles natural-language policies into policy memory slots, and query-response pairs read the policy memory through projection energy.<n>The resulting policy-evidence profile directly mediates the safety verdict and is reused for policy attribution and post-intervention verification.
arXiv Detail & Related papers (2026-09-12T06:07:43Z) - Type-based information flow analysis for $π$-calculus with a dynamically extensible security lattice [0.0]
We develop a type system for secure information flow where new security levels can be inserted into the security lattice dynamically.<n>Our system is formalized by extending Kobayashi's type-based secure information flow analysis for Milner's pi-calculus.
arXiv Detail & Related papers (2026-06-25T14:03:51Z) - PolicyBank: Evolving Policy Understanding for LLM Agents [51.86716874651299]
PolicyBank maintains structured, tool-level policy insights and iteratively refines them.<n>PolicyBank closes up to 82% of the gap toward a human oracle.
arXiv Detail & Related papers (2026-04-16T20:29:30Z) - PolicyLLM: Towards Excellent Comprehension of Public Policy for Large Language Models [56.37206340175191]
Large Language Models (LLMs) are increasingly integrated into real-world decision-making.<n>Yet, their ability to comprehend and reason about policy-related content remains underexplored.<n>We present textbftextitPolicyBench, the first large-scale cross-system benchmark (US-China) evaluating policy comprehension.
arXiv Detail & Related papers (2026-04-14T17:27:50Z) - A new measure for dynamic leakage based on quantitative information flow [2.3332469289621787]
Quantitative information flow (QIF) is concerned with assessing the leakage of information in computational systems.<n>The static perspective considers all possible runs of the system in the computation of information flow, and is usually employed when preemptively deciding whether or not to run the system.<n>The dynamic perspective is relevant for, e.g., system monitors and trackers, especially when deciding whether to continue or to abort a particular run.
arXiv Detail & Related papers (2025-10-23T18:22:39Z) - Multimodal Policy Internalization for Conversational Agents [48.11601444262434]
Multimodal Policy Internalization (MPI) is a new task that internalizes reasoning-intensive multimodal policies into model parameters.<n>We build two datasets spanning synthetic and real-world decision-making and tool-using tasks.<n>TriMPI achieves notable gains in end-to-end accuracy, generalization, and robustness.
arXiv Detail & Related papers (2025-10-10T15:28:30Z) - Dynamic Manipulation of Deformable Objects in 3D: Simulation, Benchmark and Learning Strategy [88.8665000676562]
Prior methods often simplify the problem to low-speed or 2D settings, limiting their applicability to real-world 3D tasks.<n>To mitigate data scarcity, we introduce a novel simulation framework and benchmark grounded in reduced-order dynamics.<n>We propose Dynamics Informed Diffusion Policy (DIDP), a framework that integrates imitation pretraining with physics-informed test-time adaptation.
arXiv Detail & Related papers (2025-05-23T03:28:25Z) - Dense Policy: Bidirectional Autoregressive Learning of Actions [51.60428100831717]
This paper introduces a bidirectionally expanded learning approach, termed Dense Policy, to establish a new paradigm for autoregressive policies in action prediction.<n>It employs a lightweight encoder-only architecture to iteratively unfold the action sequence from an initial single frame into the target sequence in a coarse-to-fine manner.<n>Experiments validate that our dense policy has superior autoregressive learning capabilities and can surpass existing holistic generative policies.
arXiv Detail & Related papers (2025-03-17T14:28:08Z) - Policy-as-Prompt: Rethinking Content Moderation in the Age of Large Language Models [10.549072684871478]
This paper formalises the emerging policy-as-prompt framework and identifies five key challenges across four domains.<n>It lays the groundwork for future exploration of scalable and adaptive content moderation systems in digital ecosystems.
arXiv Detail & Related papers (2025-02-25T23:15:16Z) - Quantification before Selection: Active Dynamics Preference for Robust
Reinforcement Learning [5.720802072821204]
We introduce Active Dynamics Preference(ADP), which quantifies the informativeness and density of sampled system parameters.
We validate our approach in four robotic locomotion tasks with various discrepancies between the training and testing environments.
arXiv Detail & Related papers (2022-09-23T13:59:55Z) - A System for Interactive Examination of Learned Security Policies [0.0]
We present a system for interactive examination of learned security policies.
It allows a user to traverse episodes of Markov decision processes in a controlled manner.
arXiv Detail & Related papers (2022-04-03T17:55:32Z) - Active Learning for Nonlinear System Identification with Guarantees [102.43355665393067]
We study a class of nonlinear dynamical systems whose state transitions depend linearly on a known feature embedding of state-action pairs.
We propose an active learning approach that achieves this by repeating three steps: trajectory planning, trajectory tracking, and re-estimation of the system from all available data.
We show that our method estimates nonlinear dynamical systems at a parametric rate, similar to the statistical rate of standard linear regression.
arXiv Detail & Related papers (2020-06-18T04:54:11Z)
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.