Cryptographic Enforcement of Language-Based Information Erasure
Cryptographic Enforcement of Language-Based Information Erasure
复制标题
基于语言的信息擦除的加密执行
DOI：
10.1109/csf.2015.30
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Stephen Chong
中科院分区：
文献类型：
--
作者：
Aslan Askarov;Scott Moore;Christos Dimoulas;Stephen Chong
信息擦除是一种正式的安全要求，规定何时必须从计算机系统中删除敏感数据。在正确执行擦除要求的系统中，在要求擦除敏感数据之后观察系统的攻击者不能推断出关于数据的任何信息。实施信息擦除的实际障碍包括：（1）正确确定哪些数据需要擦除，以及（2）可靠地删除潜在的大量数据，尽管存储服务不可信。在本文中，我们提出了一种新的形式化的基于语言的信息擦除，支持加密执法的擦除要求：敏感数据被加密存储前，擦除时，只有一个相对较小的一组解密密钥需要被删除。这种加密技术已经被许多实现数据删除的系统使用，以允许使用不可信的存储服务。然而，这些系统没有提供正确确定哪些数据需要擦除的支持，也没有解释或证明这些系统的正式语义属性。我们解决这些缺点。具体来说，我们研究了一种编程语言扩展与原语的公钥密码，并演示了如何信息流控制机制可以自动跟踪数据，需要擦除和可证明执行擦除要求，即使程序采用加密技术擦除。
Information erasure is a formal security requirement that stipulates when sensitive data must be removed from computer systems. In a system that correctly enforces erasure requirements, an attacker who observes the system after sensitive data is required to have been erased cannot deduce anything about the data. Practical obstacles to enforcing information erasure include: (1) correctly determining which data requires erasure, and (2) reliably deleting potentially large volumes of data, despite untrustworthy storage services. In this paper, we present a novel formalization of language-based information erasure that supports cryptographic enforcement of erasure requirements: sensitive data is encrypted before storage, and upon erasure, only a relatively small set of decryption keys needs to be deleted. This cryptographic technique has been used by a number of systems that implement data deletion to allow the use of untrustworthy storage services. However, these systems provide no support to correctly determine which data requires erasure, nor have the formal semantic properties of these systems been explained or proven to hold. We address these shortcomings. Specifically, we study a programming language extended with primitives for public-key cryptography, and demonstrate how information-flow control mechanisms can automatically track data that requires erasure and provably enforce erasure requirements even when programs employ cryptographic techniques for erasure.
DOI：
10.1145/1111037.1111045
发表时间：
2006-01
期刊：
--
影响因子：
--
作者：
Sebastian Hunt;David Sands
通讯作者：
Sebastian Hunt;David Sands