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.

云服务（例如，云数据库，无服务器计算和机器学习作为服务）现在是当今数字世界的基本构建块。这些服务是复杂的黑匣子，在与服务所有者的不同管理领域中运行。目前尚不清楚云服务在面对操作员错误，配置错误，意外故障，硬件故障和软件错误时是否总是按预期运行。该提案旨在开发一套新的技术，以使用户能够在不信任云的情况下审核其云服务的完整性，而无需云的帮助。拟议的研究有三个主要推力，针对三个云服务家庭。第一个推力使用新的框架验证了交易数据库，该框架结合了新的测谎仪数据结构，图形编码，可满足性模型理论求解和硬件加速度。除了审核云数据库外，此推力还有助于阐明以不同的隔离级别提供的以客户为中心的保证。第二个推力研究审核无服务器计算的执行完整性，这使用户能够确保其无服务器功能按书面运行。第三个势头旨在通过证明汇编之前和之后的两个模型在语义上等同于云深学习编译。拟议的系统通过使审计云服务成为可能，使个人和组织能够对外包服务的正确性充满信心，并进一步刺激云提供商提供更好的服务。此外，该项目将进行新的讲座，谈判和外展活动，以突出云失败的风险以及审计技术的运作方式。拟议的项目将开发有关执行完整性的新研究生课程。所有材料将免费提供给公众。该网站将至少五年可用。该奖项反映了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