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

职业：使用户能够审核其云服务的完整性

• 批准号: 2237295
• 负责人: Cheng Tan
• 金额: $ 60.65万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-03-01 至 2028-02-29
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2237295&HistoricalAwards=false
• 关键词: CAREER; Enabling; Users; Audit; Integrity

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.

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

项目成果

Building Verified Neural Networks for Computer Systems with Ouroboros

• 发表时间: 2023
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Tianhao Wei;Zhihao Jia;Changliu Liu;Cheng Tan