| Title | : | Building Real-World Secure Compilers with Formal Guarantees |
| Speaker | : | Anitha Gollamudi (UMass Lowell) |
| Details | : | Thu, 2 Jan, 2025 11:00 AM @ SSB 334 |
| Abstract: | : | I'll present two different projects that demonstrate the construction for practical but formally correct secure compilers in two security-critical domains. In the first part of the talk, I'll present "Automatic inference of Enclave Placement in LLVM Compiler". An enclave is a secure hardware container that provides isolated execution. However, in order to build enclave-based applications, developers have to carefully partition their application. The process can be tedious and error prone. In this work, we propose automatic inference of enclave placement in the LLVM compilation framework. Our enclave inference algorithm takes a non-enclave application along with a security policy; infers the enclave placement and compiles it to Intel SGX enclaves using OpenEnclave framework. By implementing at the level of LLVM IR, any application that gets compiled to LLVM IR can leverage our technique significantly reducing the programmer’s burden. In the second part of the talk, I'll present "ILA: Correctness via Type Checking for Fully Homomorphic Encryption (FHE)". FHE schemes add some small noise to the message during encryption. The noise accumulates with each homomorphic operation. When the noise exceeds a critical value, the FHE circuit produces an incorrect output. This makes developing FHE applications quite tedious and error-prone as existing libraries and compilers offer limited support to statically track the noise. Additionally, FHE circuits are also plagued by wraparound errors that are common in finite modulus arithmetic. Unfortunately, none of the existing compilers and libraries guarantee correct FHE evaluation. In this work, we present a correctness-oriented IR, ILA, for type-checking circuits intended for homomorphic evaluation. Our IR is backed by a type system that tracks low-level quantitative bounds (e.g., ciphertext noise) without using the secret key. Using our type system, we identify and prove a strong functional correctness criterion for ILA circuits. Bio: Dr. Anitha Gollamudi is currently an assistant professor at Richard A. Miner School of Computer and Information Sciences, UMass, Lowell. Her research enforces security in software applications against powerful cyber attackers. Specifically, she leverages trusted execution environments, a hardware-based technology, to provide formal guarantees in security-critical applications. Her work enables a step closer toward secure collaboration of mutually distrusting parties by still maintaining their compliance to privacy governing laws such as HIPAA and FERPA. She did her postdoc at Yale University and holds a Ph.D. in Computer Science from Harvard University. She was a NSF Computing Innovation Fellow and a 2021 Siebel Scholar. Prior to joining graduate school, Gollamudi was a compiler engineer at Atmel (now Microchip) and Advanced Micro Devices. She was one of the early engineers to develop an AVR-GCC compiler toolchain. Gollamudi holds a bachelor’s degree in computer science engineering from Andhra University, India. |
