终止不敏感非干扰的束语义
摘要：基于合成域论，我们提出了一种新的用于抽象行为空间上的安全信息流的束语义：安全类别是开放/封闭的分区，类型是层的结构，对敏感信息的削减对应于将层限制在封闭的子空间上。我们的安全感知计算模型可以自动满足终止不敏感的非干涉性，因此构成了非干涉性现有外部/关系模型的固有替代。我们的语义是Sterling和Harper最近对编程语言中的阶段区别和非干涉的重新解释的最新应用，这些重新解释基于Artin黏连和拓扑论的开放/封闭模态。之前的应用包括用于ML模块的参数化、Sterling和Angiuli对立方体类型论归一化的证明，以及Niu等人的成本感知逻辑框架。在本文中，我们两次采用阶段区别的视角：首先，将安全信息流的语法和语义重构为"更高"和"更低"安全性之间的阶段区别的格；其次，验证我们的层语义与Abadi等人的依赖核心演算扩展的计算充实性，其中包括一个用于解密终止信道的构造。
作者：Jonathan Sterling and Robert Harper
论文ID：2204.09421
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-04-21