带迭代的隐马尔可夫规划代数
Hidden-Markov Program Algebra with iteration
摘要：
我们使用隐马尔可夫模型，以激励一个定量的成分语义的非干扰为基础的安全与迭代，包括一个细化或“实现”的关系，比较两个程序相对于他们的信息泄漏，我们提出了一个程序代数源级推理等程序，特别是作为一种手段，建立一个“实现”程序泄漏不超过其“规范”的程序。<p>这将两个主题结合在一起：我们扩展了我们早期的工作，有迭代，但只有定性的，通过使其定量;我们扩展了我们早期的定量工作，包括迭代。<p>我们提倡逐步细化和源代码级程序代数，作为概念推理工具和自动化援助的目标。一个选择的代数法给出了支持这一观点的情况下，定量不干扰，并证明了一个简单的迭代密码猜测攻击。
英文摘要：
We use Hidden Markov Models to motivate a quantitative compositional semantics for noninterference-based security with iteration, including a refinement- or "implements" relation that compares two programs with respect to their information leakage; and we propose a program algebra for source-level reasoning about such programs, in particular as a means of establishing that an "implementation" program leaks no more than its "specification" program. <p>This joins two themes: we extend our earlier work, having iteration but only qualitative, by making it quantitative; and we extend our earlier quantitative work by including iteration. <p>We advocate stepwise refinement and source-level program algebra, both as conceptual reasoning tools and as targets for automated assistance. A selection of algebraic laws is given to support this view in the case of quantitative noninterference; and it is demonstrated on a simple iterated password-guessing attack.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
