The Shadow Knows: Refinement and security in sequential programs
The Shadow Knows: Refinement and security in sequential programs
复制标题
影子知道：顺序程序的细化和安全性
DOI：
10.1016/j.scico.2007.09.003
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Carroll Morgan
中科院分区：
文献类型：
--
作者：
Carroll Morgan
逐步细化是系统开发的一个重要概念工具，鼓励通过一些独立的正确性保持阶段，理想情况下可以孤立地理解的程序建设。安全的一个关键概念组成部分是对手对隐藏信息的无知。我们提出了一种新的方法结合这两个想法。我们的建议是基于一个数学定义的“保持一致性”的细化，通过限制对手的访问隐藏的信息扩展经典的细化：从规范到实现应该永远不会增加访问。新颖之处在于我们在顺序程序的上下文中实现这一点的方式。具体来说，我们给出了一个操作模型（和详细的理由），一个基本的顺序编程语言和它的操作语义在该模型中，一个“无知的逻辑”在同一模型上解释，然后一个程序逻辑语义将这些放在一起-最后，我们使用的逻辑建立，通过细化，一个真实的（虽然小）协议的正确性：Rivest的不经意传输。之前的一份报告也对Chaum's Dining Cryptographers进行了类似的处理。在传递中，我们解决了顺序程序的精化paradigm。
Stepwise refinement is a crucial conceptual tool for system development, encouraging program construction via a number of separate correctness-preserving stages which ideally can be understood in isolation. A crucial conceptual component of security is an adversary’s ignorance of concealed information. We suggest a novel method of combining these two ideas. Our suggestion is based on a mathematical definition of “ignorance-preserving” refinement that extends classical refinement by limiting an adversary’s access to concealed information: moving from specification to implementation should never increase that access. The novelty is the way we achieve this in the context of sequential programs. Specifically we give an operational model (and detailed justification for it), a basic sequential programming language and its operational semantics in that model, a “logic of ignorance” interpreted over the same model, then a program-logical semantics bringing those together — and finally we use the logic to establish, via refinement, the correctness of a real (though small) protocol: Rivest’s Oblivious Transfer. A previous report⋆treated Chaum’s Dining Cryptographers similarly. In passing we solve the Refinement Paradox for sequential programs.