论文标题
Anosy：近似知识合成，具有改进类型的解密类型
ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
论文作者
论文摘要
非干预是执行敏感数据机密性的一种流行方式。但是，在现实的应用程序中通常需要对敏感信息解密，但会破坏不干预。我们提出了Anosy，这是定量解密策略的近似知识合成器。 Anosy使用改进类型自动构建机器检查了攻击者知识的过度和不足的攻击者知识，以查询多数直觉秘密的布尔查询。它还提供了一个Anosyt Monad，可以通过多个解密查询跟踪攻击者知识，并检查信息流控制应用程序中对用户指定策略的违法行为。我们实施了Anosy的原型，并表明它是精确且宽松的：在使用Intervals Intervals域进行违反策略之前，允许最多14个解密查询。
Non-interference is a popular way to enforce confidentiality of sensitive data. However, declassification of sensitive information is often needed in realistic applications but breaks non-interference. We present ANOSY, an approximate knowledge synthesizer for quantitative declassification policies. ANOSY uses refinement types to automatically construct machine checked over- and under-approximations of attacker knowledge for boolean queries on multi-integer secrets. It also provides an AnosyT monad to track the attacker knowledge over multiple declassification queries and checks for violations against user-specified policies in information flow control applications. We implement a prototype of ANOSY and show that it is precise and permissive: up to 14 declassification queries are permitted before a policy violation occurs using the powerset of intervals domain.
