Hypercollecting semantics and its application to static analysis of information flow
Hypercollecting semantics and its application to static analysis of information flow
复制标题
超集合语义及其在信息流静态分析中的应用
DOI：
10.1145/3093333.3009889
复制
发表时间：
2017
影响因子：
--
通讯作者：
Tronel, Frédéric
中科院分区：
文献类型：
--
作者：
Assaf, Mounir;Naumann, David A.;Signoles, Julien;Totel, Éric;Tronel, Frédéric
我们展示了如何在抽象解释的框架内表达和证明安全信息流的静态分析是完全正确的。关键思想是定义一个直接近似于感兴趣的超性质的伽罗瓦连接。为了使用这种伽罗瓦连接，我们引入了超收集语义的不动点表征，即“集合的集合”转换器。这使得完全在抽象解释的计算框架内系统地推导超特性的静态分析成为可能。我们通过给出示例静态分析来评估这种技术。对于定性信息流，我们导出了类似于Amtoft和Banerjee （SAS '04）的逻辑和Hunt和Sands （POPL '06）的类型系统的依赖分析。对于定量信息流，我们推导了一种新的基数分析，该分析限制了程序传递的泄漏，而不是简单地确定它是否存在。这包含了超安全但不安全的问题。我们使用该框架并引入各种变体，以达到与信息流的最新和精确静态分析相媲美的精度。
We show how static analysis for secure information flow can be expressed and proved correct entirely within the framework of abstract interpretation. The key idea is to define a Galois connection that directly approximates the hyperproperty of interest. To enable use of such Galois connections, we introduce a fixpoint characterisation of hypercollecting semantics, i.e. a "set of sets" transformer. This makes it possible to systematically derive static analyses for hyperproperties entirely within the calculational framework of abstract interpretation. We evaluate this technique by deriving example static analyses. For qualitative information flow, we derive a dependence analysis similar to the logic of Amtoft and Banerjee (SAS '04) and the type system of Hunt and Sands (POPL '06). For quantitative information flow, we derive a novel cardinality analysis that bounds the leakage conveyed by a program instead of simply deciding whether it exists. This encompasses problems that are hypersafety but notk-safety. We put the framework to use and introduce variations that achieve precision rivalling the most recent and precise static analyses for information flow.
登录
查看更多内容
结合时间分析：新的视角
DOI：
--
发表时间：
1991
期刊：
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
影响因子：
--
作者：
Sebastian Hunt;David Sands
通讯作者：
David Sands
DOI：
--
发表时间：
2015
期刊：
Logic Programming and Automated Reasoning
影响因子：
--
作者：
Luciano Bello;Daniel Hedin;A. Sabelfeld
通讯作者：
A. Sabelfeld
DOI：
10.1145/1111037.1111045
发表时间：
2006-01
期刊：
--
影响因子：
--
作者：
Sebastian Hunt;David Sands
通讯作者：
Sebastian Hunt;David Sands
攻击者知识的混合监控
DOI：
10.1109/csf.2016.23
发表时间：
2016
期刊：
2016 IEEE 29th Computer Security Foundations Symposium (CSF)
影响因子：
--
作者：
Frédéric Besson;Nataliia Bielova;T. Jensen
通讯作者：
T. Jensen
影响因子：
5.6
作者：
Agostino Cortesi;Giulia Costantini;Pietro Ferrara
通讯作者：
Pietro Ferrara