A static analysis for quantifying information flow in a simple imperative language
A static analysis for quantifying information flow in a simple imperative language
复制标题
DOI：
10.3233/jcs-2007-15302
复制
发表时间：
2007-01-01
影响因子：
1.2
通讯作者：
Malacaria, Pasquale
中科院分区：
文献类型：
--
作者：
Clark, David;Hunt, Sebastian;Malacaria, Pasquale
我们提出了一种量化简单命令式语言干扰的方法，该语言包括循环结构。在本文中，我们着重于这种干扰定义的特定情况：通过特洛伊木马攻击从私人变量到公共变量的信息泄漏。我们根据香农的信息理论来量化泄漏，并通过证明泄漏的定义和编程语言干扰的经典概念来激发我们的定义。本文的主要贡献是基于此类语言定义的定量静态分析。该分析使用一些非平凡的信息理论结果，例如Fano的不平等和L-1不平等，为条件陈述提供了合理的界限。而通过将定性流敏关系分析整合到定量分析中来处理环。
We propose an approach to quantify interference in a simple imperative language that includes a looping construct. In this paper we focus on a particular case of this definition of interference: leakage of information from private variables to public ones via a Trojan Horse attack. We quantify leakage in terms of Shannon's information theory and we motivate our definition by proving a result relating this definition of leakage and the classical notion of programming language interference. The major contribution of the paper is a quantitative static analysis based on this definition for such a language. The analysis uses some non-trivial information theory results like Fano's inequality and the L-1 inequality to provide reasonable bounds for conditional statements. While-loops are handled by integrating a qualitative flow-sensitive dependency analysis into the quantitative analysis.