Sound Enforcement of Dynamic Release Information Flow Policy-Full Version
2026-08-10 • Programming Languages
Programming LanguagesCryptography and Security
AI summaryⓘ
The authors address a problem in keeping sensitive information secure when rules about what can be shared change over time. They build a new system that can correctly check and enforce these flexible rules, called dynamic release policy. To do this, they created a simple programming language, designed a method to check the rules, proved mathematically that this method works, and tested it by adding it to the Rust programming language. Their work helps bridge the gap between theoretical security ideas and practical use in real software.
information flow analysisdynamic release policytype systemdeclassificationendorsementformal verificationRust languagesecurity policy enforcementconfidentialityintegrity
Authors
Jeffrey C. Ching, Danfeng Zhang
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.