AI 中文总结
研究信息流中稳健降级与非干扰的协调问题，引入参数化信息流，利用模态类型理论见解，通过二元逻辑关系论证展示非干扰，实现兼顾保密性和完整性的单一框架，揭示降级机制与抽象、模块化机制的兼容性。
AI 中文摘要
非干扰属性，涵盖保密性和完整性，长期以来一直是程序安全保障的高标准。信息流类型系统是获取程序非干扰属性的主要手段，但其作为安全编程圣杯的潜力尚未充分发挥。先前工作将类型系统按保密性和完整性进行二分，导致重复的推理机制和复杂的规范。此外，长期以来的观点认为，必须通过降级机制削弱非干扰，以适应实际程序的需求，几乎所有实际程序在实现其目的的过程中都会违反保密性和完整性，这常常突破抽象屏障并损害模块化推理。我们引入参数化信息流，利用模态类型理论的最新见解来阐明这些问题。特别是，我们从关于开放和封闭模态的工作中汲取灵感，突出它们丰富的相互作用。尽管每个单独的模态在文献中都有应用，但我们的关键见解是它们的联合交互足以重建全谱信息流推理，产生一个兼顾保密性和完整性的单一框架。在不扩展我们理论的情况下，恢复了稳健解密谱系中的降级和高级推理工具的类似物，强化了先前的结果。我们通过二元逻辑关系论证展示了非干扰，将稳健性实现为由我们的模态介导的普通 2 - 超属性。我们的工作表明，最先进的降级机制与抽象和模块化机制完全兼容，正是源于在完全强度非干扰下后者的语义。
英文摘要
Non-interference properties, spanning confidentiality and integrity, have long enjoyed a position as the high water mark of program security guarantees. Information flow type systems comprise the primary means for obtaining non-interference properties of programs, but their potential as a holy grail for secure programming has remained latent. Prior work bifurcates the type system along confidentiality and integrity, resulting in duplicate reasoning machinery and complex specifications. Furthermore, long-held wisdom dictates that non-interference must be weakened with downgrading mechanisms to accommodate the needs of practical programs, nearly all of which violate confidentiality and integrity in the course of fulfilling their purpose. This often pierces abstraction barriers and compromises modular reasoning. We introduce parametric information flow, which uses recent insights from modal type theory to shed light on these issues. In particular, we draw inspiration from work on the open and closed modalities, highlighting their rich interplay. Though each individual modality finds uses throughout the literature, our key insight is that their joint interaction suffices to reconstruct full-spectrum information flow reasoning, producing a single framework accounting for both confidentiality and integrity. Downgrading and analogues of advanced reasoning tools in the lineage of robust declassification are recovered without extensions to our theory, strengthening prior results. We show non-interference via a binary logical relations argument, realizing robustness as an ordinary 2-hyperproperty mediated by our modalities. Our work reveals state-of-the-art downgrading mechanisms to be wholly compatible with those for abstraction and modularity, arising precisely from the semantics of the latter under full-strength non-interference.
