ANOSY: approximated knowledge synthesis with refinement types for declassification

ANOSY: approximated knowledge synthesis with refinement types for declassification
复制标题

ANOSY:具有用于解密的细化类型的近似知识合成

DOI:
10.1145/3519939.3523725
复制
发表时间:
2022
期刊:
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子:
--
通讯作者:
Parker, James
Parker, James
中科院分区:
--
文献类型:
--
作者:
Guria, Sankha Narayan;Vazou, Niki;Guarnieri, Marco;Parker, James

文献摘要

参考文献

被引文献

相似文献

不干涉是一种流行的方法来加强敏感数据的机密性。然而,在实际应用中往往需要对敏感信息进行解密,而这又打破了互不干扰的原则。我们提出ANOSY,一个近似的定量解密策略知识综合器。ANOSY使用细化类型来自动构造攻击者知识的机器检查过近似值和欠近似值,用于对多整数秘密的布尔查询。它还提供了一个AnosyT单子,用于通过多个解密查询跟踪攻击者的知识,并检查信息流控制应用程序中是否违反了用户指定的策略。我们实现了ANOSY的原型,并表明它是精确的和允许的:在使用间隔域的幂集发生策略违反之前,最多允许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.
DOI: 10.1145/2737924.2737957
发表时间: 2015-06
期刊: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子: --
作者:
Andrew Johnson;Lucas Waye;Scott Moore;Stephen Chong
通讯作者: Andrew Johnson;Lucas Waye;Scott Moore;Stephen Chong
DOI: 10.1007/978-3-319-89722-6_1
发表时间: 2018
期刊: ArXiv
影响因子: --
作者:
Ian Sweet;José Manuel Calderón Trilla;Chad Scherrer;M. Hicks;Stephen Magill
通讯作者: Stephen Magill
DOI: 10.1145/503272.503302
发表时间: 2002
期刊: 2016 IEEE 29th Computer Security Foundations Symposium (CSF)
影响因子: --
作者:
F. Pottier;Vincent Simonet
通讯作者: Vincent Simonet
Haskell 中的信息流编码
DOI: --
发表时间: 2006
期刊: 19th IEEE Computer Security Foundations Workshop (CSFW'06)
影响因子: --
作者:
Peng Li;Steve Zdancewic
通讯作者: Steve Zdancewic
DOI: 10.1109/csf.2010.8
发表时间: 2010-07
期刊: 2010 23rd IEEE Computer Security Foundations Symposium
影响因子: --
作者:
Boris Köpf;A. Rybalchenko
通讯作者: Boris Köpf;A. Rybalchenko