Towards Secure-by-Construction Compilers for Practical Systems

Towards Secure-by-Construction Compilers for Practical Systems
Host Faculty: Dr.Ashish Mishra
Speaker: Dr. Anitha Gollamudi
Date: 27 August
Time: 11:20 am
Venue: CSE Seminar Hall

Abstract
Dr. Anitha Gollamudi will present two different projects that demonstrate the construction of practical but formally correct secure compilers in two security-critical domains

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 for statically tracking 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, she presents a correctness-oriented IR, ILA, for type-checking circuits intended for homomorphic evaluation. Her IR is backed by a type system that tracks low-level quantitative bounds (e.g., ciphertext noise) without using the secret key. Using her type system, she identifies and proves a strong functional correctness criterion for ILA circuits. Towards the end, she also shows its applications for the CKKS scheme, specifically for encrypted inference.

Flexible, Fine-grained, and Secure-by-Construction Enclave Partitioning for LLVM Applications

While Trusted Execution Environments (TEEs) provide hardware isolation, they do not by themselves enforce information-flow security, and manually partitioning applications into enclave and non-enclave components is difficult and error-prone.

She addresses these challenges by developing an LLVM-based type system that combines information-flow control with security-aware memory safety, extending it to reason about enclave-aware attackers, and providing a type-preserving compilation that automatically partitions applications while preserving security.

Bio

Dr. Anitha Gollamudi is currently an assistant professor at Richard A. Miner School of Computer & 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. Her work is supported by NSF and ONR.

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.