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

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.