信息流推理的代数方法
An Algebraic Approach for Reasoning About Information Flow
摘要：
本文对安全系统中的信息泄漏问题进行了分析。我们解决了定量信息流（QIF）中使用的（标准）通道模型中指定和分析大型系统的问题。我们提出了几个运营商，匹配典型的系统组件之间的相互作用。我们探讨其代数性质的安全保护的细化关系定义的Alvim等人。和McIver等人。我们展示了如何代数可以用来简化大型系统规范，以方便计算的信息泄漏界限。我们证明了我们的结果的规范和分析的人群协议。最后，我们使用代数证明了一个新的算法来计算泄漏边界的协议。
英文摘要：
This paper concerns the analysis of information leaks in security systems. We address the problem of specifying and analyzing large systems in the (standard) channel model used in quantitative information flow (QIF). We propose several operators which match typical interactions between system components. We explore their algebraic properties with respect to the security-preserving refinement relation defined by Alvim et al. and McIver et al. We show how the algebra can be used to simplify large system specifications in order to facilitate the computation of information leakage bounds. We demonstrate our results on the specification and analysis of the Crowds Protocol. Finally, we use the algebra to justify a new algorithm to compute leakage bounds for this protocol.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
