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

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

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.