AI 中文总结
本文提出首个实施动态发布信息流策略的类型系统，完成其可靠性形式化证明，并将该系统实现为Rust扩展原型，通过会议评审系统和Civitas案例研究验证了方案。
AI 中文摘要
信息流分析是评估机密性和完整性问题的实际方法，但在实际系统中仍缺乏广泛应用，部分原因在于理论与实践之间存在根本差距：实际系统中安全问题的动态特性超出了现有技术的范围，现有技术假设策略是静态的（即数据保密性不会改变）。认识到这一根本差距，大量研究已针对该问题的各个方面展开（例如，支持去分类、背书和调用策略）。近期一项研究更进一步，将一种有前景的端到端策略“动态发布”形式化，该策略通过允许信息流限制以任意方式降级和升级，统一了先前的形式化方法。然而，如何可靠地实施强大的动态发布策略仍是一个开放问题。本文提出了首个实施动态发布策略的类型系统，并对其可靠性进行了形式化证明。更具体地说，我们（1）形式化了支持动态发布策略的核心语言，（2）开发了用于检查动态发布策略的类型系统，（3）开发了新的证明技术并形式化证明该类型系统可实施动态发布策略，（4）将该类型系统实现为Rust语言的扩展原型，并在会议评审系统和Civitas上进行了案例研究。
英文摘要
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.
DOI：10.1145/3839492
