Systems for Computation on Encrypted Data

失去控制以及可能向服务提供商、恶意内部人员或有动机的黑客泄露私人信息被视为云计算广泛采用的障碍。加密领域的许多最新科学发展，如同态加密和函数加密或安全多方计算，通过在将数据发送到云端之前对其进行加密，提供了一种可行的解决方案。然而，现有软件的绝大多数代码太难用这些加密技术进行改造，并且不能从理论上的进步中受益。 我将通过研究新的方法来克服这一挑战，这些方法保留了现有的编程接口和语言，如Java或SQL，但编译成在高度加密的数据上运行的版本。来自系统社区的现有方法，例如CryptDB或JCrypt，能够执行现有程序，但使用弱加密机制，例如确定性加密，并且来自安全社区的现有方法，例如动态对称可搜索加密或AutoCrypt，使用可证明安全的方法，但明显缺乏功能，例如不允许范围查询。我的目标是在计算机科学中弥合这两种方法。一方面，我的目标是严格的正式模型的安全清楚地捕捉隐含的泄漏，另一方面，我的目标是工程可测试的系统，可以实际和实验验证的理论性能增益。这需要超越最新技术水平的以下进步：研究1）捕获预期功能和安全性的新的正式安全模型，开发2）针对这些模型的改进的加密机制和系统算法，最后3）证明这些模型的安全性和正确性。 我将针对重要的、已建立的编程接口，如SQL和Java，它们很难改变。对于SQL，我将开发改进的可搜索加密方案，这些方案没有泄漏，并开发相应的正式模型，以捕获泄漏滥用攻击的影响（博士生#1）。此外，我将开发使用数据不经意算法的安全计算中的查询处理（硕士生#3）。对于Java，我将为可验证的同态计算开发改进的方法（博士生#2），并为恶意模型开发知识推理（硕士生#4）。我将把开发的方法集成到应用服务器和数据库中，用于示例性应用程序（硕士生#5）。 如果在提案的最后，我们有科学基础在加密数据上运行现有的、真实世界的、大型的、交互式的云应用程序，我就成功了。拟议的工作是有价值的，加拿大通过培训HQP在计算机安全，展示了科学卓越的一个非常活跃的研究领域，并旨在突破高工业相关性的云计算。

The loss of control and the potential disclosure of private information to the service provider, malicious insiders or motivated hackers are seen as a barrier to the wide-spread adoption of cloud computing. Many recent scientific developments in encryption, such as homomorphic and functional encryption or secure multi-party computation, offer a viable solution by encrypting the data before sending it to the cloud. However, existing software the vast majority of code is too difficult to retrofit with these encryption techniques and does not benefit from the theoretical advances. I will overcome this challenge by researching new methods that preserve existing programming interfaces and languages, such as Java or SQL, but compile to versions running on strongly encrypted data. Existing methods from the systems community, such as CryptDB or JCrypt, are capable to execute existing programs, but use weak cryptographic mechanisms, e.g. deterministic encryption, and existing methods from the security community, such as dynamic symmetric searchable encryption or AutoCrypt, use provably secure methods, but significantly lack in functionality, e.g. not allowing range queries. I aim to bridge those two approaches in computer science. On the one hand I aim at rigorous formal models of security clearly capturing the implied leakage and on the other hand I aim at engineering testable systems that can practically and experimentally verify the theoretical performance gains. This requires the following advances beyond the state-of-the-art: researching 1) new formal security models that capture the intended functionality and security, developing 2) improved cryptographic mechanisms and systems algorithms for these models and finally 3) proving security and correctness in these models. I will target important, established programming interfaces, such as SQL and Java, which are very hard to change. For SQL I will develop improved searchable encryption schemes which have no leakage and corresponding formal models that capture the impact of leakage-abuse attacks (PhD student #1). Additionally I will develop query processing in secure computation using data-oblivious algorithms (Master student #3). For Java I will develop improved methods for verifiable homomorphic computation (PhD student #2) and develop knowledge inference for the malicious model (Master student #4). I will integrate the methods developed into application servers and databases for an exemplary application (Master student #5). I will have been successful, if at the end of the proposal we have the scientific foundation to run existing, real-world, large, interactive applications in the cloud on encrypted data. The proposed work is of value to Canada by training HQP in computer security, demonstrating scientific excellence in a very active research field and aiming at a break-through of high industrial relevance in cloud computing.