任务完成：渐进式安全的圣杯

具有渐进式信息流控制的语言结合了静态和动态技术以防止安全泄漏。渐进式语言应满足渐进性保证：仅在类型标注精度上有所不同的程序，除了强制类型转换错误外，其行为应当一致。遗憾的是，Toro 等人 [2018] 指出了渐进性保证与信息安全之间存在张力；他们无法在语言 $\mathrm{GSL}_\mathsf{Ref}$ 中同时满足这两个属性，不得不退而求其次仅满足信息流安全。Azevedo de Amorim 等人 [2020] 表明，通过牺牲类型引导的分类，可以得到一种同时满足不干涉性和渐进性保证的语言。Bichhawat 等人 [2021] 表明，通过牺牲无敏感升级机制并用静态分析取而代之，这两个属性均可被满足。在本文中，我们提出了一种语言设计 $\lambda_{\mathtt{IFC}}^\star$，它在不作任何牺牲的情况下同时满足不干涉性和渐进性保证。我们保留了 $\mathrm{GSL}_\mathsf{Ref}$ 的类型引导分类，并使用标准的无敏感升级机制来防止通过可变引用产生的隐式流。$\lambda_{\mathtt{IFC}}^\star$ 设计的关键在于退回 $\mathrm{GSL}_\mathsf{Ref}$ 中将未知标签 $\star$ 包含在运行时安全标签之中的决定。我们给出了 $\lambda_{\mathtt{IFC}}^\star$ 的形式化定义，证明了渐进性保证，并证明了不干涉性。在技术层面上，$\lambda_{\mathtt{IFC}}^\star$ 的语义是首个使用强制转换演算（仿 Henglein）来指定的渐进式信息流控制语言，从而扩展了渐进式类型转换的强制转换理论。