推荐 3.5
Conf: 50%
本文研究分离式信息流策略的强制执行问题。分离式策略允许一个值最多依赖于两个秘密之一,而不能同时依赖于两者,例如分析师只能查阅一个客户的文件而不能同时查阅两个,或者分割的秘密只能释放其中一部分。这类策略不满足格结构,Hunt和Sands提出使用信息量quantale来给出其语义,但未能解决强制执行层的实现。本文构建了该quantale所要求的流敏感类型系统家族,并揭示了关键的通用类型对象在分离场景下分裂为两个不同对象,对强制执行产生重要影响。在程序变量上的自由交换quantale上,作者证明了整个类型机制对所有策略均成立,包括单调重命名、规范推导、主类型和内部完备性。而在具有幂等生成元的自由对象上,认证的界更为精确且保持健全,因为它能正确记录同一来源的两次读取仅对应一个析取项。然而,这一精度提升无法在独立属性家族内部实现:任何支持单调重命名的标记映射都无法认证比第一个机制更精确的界,且在生成元精确同态特化下两者主类型重合。在道德墙和秘密共享标签下,对析取源的第二次读取将导致所有此类证书失效,从而拒绝本应满足策略的程序。作者还指出,直接采用格时代的通用类型对象会进一步商掉分支析取的信息。为恢复精度,他们提出将特化推迟到判断级别,由此得到的读取映射是满足健全性的最小并保持映射。该工作为分离式策略提供了首个完整的流敏感类型系统框架,并为信息流控制中的此类策略验证奠定了理论基础。
💡 推荐理由: 分离式策略在现实场景(如隐私保护、秘密共享)中具有重要应用,本文首次为其提供了完整的流敏感类型系统强制执行框架,填补了理论空白,为构建更精细的信息流控制工具奠定了基础。
🎯 建议动作: 研究跟进
排序因子: 来自 arXiv 其他板块 (+2) | Community 数据源 (+1) | LLM 评分加成 (+0.5)