On the computational soundness of cryptographically masked flows
On the computational soundness of cryptographically masked flows
复制标题
关于加密屏蔽流的计算可靠性
DOI：
10.1145/1328438.1328479
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Peeter Laud
中科院分区：
文献类型：
--
作者：
Peeter Laud
为了讨论采用密码操作的程序中信息流的安全性，必须使用基于程序状态分布的计算不可分辨能力的定义。这些定义，以及伴随的分析工具，是复杂的和容易出错的争论。由Askarov，Hedin和Sabelfeld提出的加密掩码流是一种抽象的执行模型和安全定义，试图抽象出计算安全的细节。这个抽象的模型是有用的，因为程序的分析可以使用通常的技术来执行非干扰。
在本文中，我们调查在哪些条件下，这个抽象的模型是计算上的声音，即当一个程序在他们的模型的安全意味着这个程序的计算安全。本文阐明了一组合理的条件，然后提出了一个更简单的抽象模型，但没有更多的限制比加密掩蔽流与这些条件的健全性。
To speak about the security of information flow in programs employing cryptographic operations, definitions based on computational indistinguish ability of distributions over program states have to be used. These definitions, as well as the accompanying analysis tools, are complex and error-prone to argue about. Cryptographically masked flows, proposed by Askarov, Hedin and Sabelfeld, are an abstract execution model and security definition that attempt to abstract away the details of computational security. This abstract model is useful because analysis of programs can be conducted using the usual techniques for enforcing non-interference.
In this paper we investigate under which conditions this abstract model is computationally sound, i.e. when does the security of a program in their model imply the computational security of this program. This paper spells out a reasonable set of conditions and then proposes a simpler abstract model that is nevertheless no more restrictive than the cryptographically masked flows together with these conditions for soundness.