Computing Information Flow Using Symbolic Model-Checking
Computing Information Flow Using Symbolic Model-Checking
复制标题
使用符号模型检查计算信息流
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Stefan Schwoon
中科院分区：
文献类型：
--
作者：
Rohit Chadha;Umang Mathur;Stefan Schwoon
文献中已经提出了几种措施来量化由具有秘密输入的程序的公开输出所泄露的信息。考虑了当信息测度是基于（a）最小熵和（B）Shannon熵时，确定性或概率性程序泄漏信息的计算问题.在计算这些措施的关键挑战是，我们需要的可能的输出的总数，并为每个可能的输出，导致它的输入的数量。直接计算这些量是不可行的，因为状态爆炸问题。因此，我们提出了基于二叉决策图（BDDs）的符号算法。我们的方法的优点是，这些符号算法可以很容易地实现在任何基于BDD的模型检查工具，检查可达性确定性非递归程序计算程序摘要。我们证明了我们的方法的有效性，通过实现这些算法在一个工具轻便摩托车QLeak，这是建立在轻便摩托车，布尔程序的模型检查器。最后，我们将展示这种符号方法如何扩展到概率程序。
Several measures have been proposed in literature for quantifying the information leaked by the public outputs of a program with secret inputs. We consider the problem of computing information leaked by a deterministic or probabilistic program when the measure of information is based on (a) min-entropy and (b) Shannon entropy. The key challenge in computing these measures is that we need the total number of possible outputs and, for each possible output, the number of inputs that lead to it. A direct computation of these quantities is infeasible because of the state-explosion problem. We therefore propose symbolic algorithms based on binary decision diagrams (BDDs). The advantage of our approach is that these symbolic algorithms can be easily implemented in any BDD-based model-checking tool that checks for reachability in deterministic non-recursive programs by computing program summaries. We demonstrate the validity of our approach by implementing these algorithms in a tool Moped-QLeak, which is built upon Moped, a model checker for Boolean programs. Finally, we show how this symbolic approach extends to probabilistic programs.
DOI：
10.1109/csf.2013.20
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Chothia T
通讯作者：
Chothia T
影响因子：
1.2
作者：
Clark, David;Hunt, Sebastian;Malacaria, Pasquale
通讯作者：
Malacaria, Pasquale