CAREER: Enabling Users to Audit the Integrity of Their Cloud Services

云服务（例如，云数据库、无服务器计算和机器学习即服务）现在是当今数字世界的基本组成部分。这些服务是复杂的黑盒，运行在与服务所有者不同的管理域中。目前还不清楚，当面对操作人员错误、错误配置、意外故障、硬件故障和软件错误时，云服务是否总是按预期运行。该提案旨在开发一套新的技术，使用户能够在不信任云、不借助云的情况下审计其云服务的完整性。拟议的研究有三个主要重点，针对三个云服务家族。第一个任务是用一个新框架验证事务数据库，该框架结合了新的测谎数据结构、图编码、可满足模理论求解和硬件加速。除了审计云数据库之外，此推力还有助于澄清由不同隔离级别提供的以客户为中心的保证。第二个重点研究审计无服务器计算的执行完整性，这使用户能够确保他们的无服务器功能按编写的方式运行。第三个推力旨在通过证明编译前后的两个模型在语义上等效来验证云深度学习编译。拟议的系统使审计云服务成为可能，使个人和组织能够对其外包服务的正确性获得信心，并进一步激励云提供商提供更好的服务。此外，该项目还将制作新的讲座、会谈和拓展活动，以突出云故障的风险以及审计技术的工作原理。本项目拟开设一门关于执行诚信的研究生新课程。所有材料都将免费提供给公众。该项目的代码、数据、文档、论文、技术报告和课程材料将在网站上公开：https://khoury-srg.github.io/AuditCloud。该网站将至少运行5年。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Cloud services (for example, cloud databases, serverless computing, and machine learning as a service) are now the basic building blocks of today's digital world. These services are complex black boxes, running in a different administrative domain from the service owners. It is unclear if cloud services always run as expected when facing operator errors, misconfigurations, unexpected failures, hardware faults, and software bugs. This proposal aims to develop a new set of techniques to enable users to audit the integrity of their cloud services without trusting the cloud and without help from the cloud.The proposed research has three main thrusts targeting three families of cloud services. The first thrust verifies transactional databases with a new framework that combines new polygraph data structures, graph encoding, Satisfiability Modulo Theories solving, and hardware accelerations. Besides auditing cloud databases, this thrust helps clarify client-centric guarantees provided by different isolation levels. The second thrust studies auditing the execution integrity of serverless computing, which enables users to ensure their serverless functions run as written. The third thrust aims to verify cloud deep learning compilation by proving the two models before and after compilation are semantically equivalent.The proposed systems, by making auditing cloud services possible, enable individuals and organizations to gain confidence about the correctness of their outsourced services and further spur cloud providers to provide better services. In addition, the project will produce new lectures, talks, and outreach activities to highlight the risks of cloud failures and how auditing techniques work. The proposed project will develop a new graduate course about execution integrity. All the materials will be freely available to the public.The project's code, data, documents, papers, technical reports, and course materials will be publicly available at the website: https://khoury-srg.github.io/AuditCloud. The website will be available for at least five years.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.