Publications

Select Publications (Reverse Chronological Order)

(Click + button for abstract)

2025

• + T. Gollamudi, A. Gollamudi, and J. Gancher, “ILA: Correctness via Type Checking for Fully Homomorphic Encryption,” in CCS '25, forthcoming, 2025.
  Abstract: RLWE-based Fully Homomorphic Encryption (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 subtle, as one must closely track the noise to ensure correctness. Existing libraries and compilers offer limited support to statically track the noise. Additionally, FHE circuits are plagued by wraparound errors common in finite modulus arithmetic.
  
  We present a correctness-oriented IR, Intermediate Language for Arithmetic Circuits (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. The core type system does not assume a particular FHE scheme but axiomatizes a model of FHE. We instantiate this model with the exact FHE schemes (BGV, BFV, and TFHE), and obtain functional correctness for free.
  
  We implement a concrete type checker ILA, parameterized by the noise estimators for three popular FHE libraries (OpenFHE, SEAL, and TFHE-rs). We also use the type checker to infer optimal placement of modulus switching. Evaluation shows that ILA type checker is sound, practical, and efficient.
• + W. B. Nuzzo, M. Elwakil, and A. Gollamudi, “Automatic Inference of Enclave Placement in LLVM Compiler,” in Workshop on Principles of Secure Compilation (PriSC), 2025.
  Abstract: Trusted Execution Environments (TEEs) enable applications to obtain strong confidentiality and integrity guarantees even in the presence of privileged but malicious software. Key to their enforcement is an enclave—a secure hardware container that provides isolated execution. Building enclave-based applications requires careful partitioning, which is tedious and error-prone.
  
  We propose automatic inference of enclave placement in the LLVM compilation framework. Our algorithm takes a non-enclave application along with a security policy, infers the enclave placement, and compiles it to Intel SGX enclaves using the OpenEnclave framework. By implementing this at the LLVM IR level, any application compiled to LLVM IR can leverage our technique, significantly reducing the programmer’s burden.

2023

• + A. E. Michael*, A. Gollamudi*, J. Bosamiya, E. Johnson, A. Denlinger, C. Disselkoen, C. Watt, B. Parno, M. Patrignani, M. Vassena, et al., “Mswasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code,” Proc. ACM Programming Languages, vol. 7, no. POPL, pp. 425–454, 2023.
  *These authors contributed equally.
  Abstract: Most programs compiled to WebAssembly (Wasm) are written in unsafe languages like C and C++. Memory-unsafe C code remains unsafe in Wasm. Memory-Safe WebAssembly (MSWasm) extends Wasm with memory-safety abstractions to address this. We give precise semantics of MSWasm and prove that well-typed programs are robustly memory-safe. We develop a novel, language-independent memory-safety property, reason about a formal C-to-MSWasm compiler, and guide several implementations.
  
  Evaluation shows that enforcing memory safety has overheads ranging from 22% to 198%, depending on enforcement mechanism, and MSWasm allows easy swapping of enforcement mechanisms for performance-security trade-offs.
• + A. Gollamudi and S. Chong, “Expressive Authorization Policies using Computation Principals,” in SACMAT '23.
  Abstract: In authorization logics, it is natural to treat computations as principals, since systems need to decide how much authority to give computations when they execute. Existing authorization logics identify computation principals using brittle hash-based naming, treating them as black boxes. We introduce Coal, a programming-language calculus that embeds an authorization logic in its type system. Computation principals in Coal can be reasoned about, allowing fine-grained access control policies dependent on the structure and semantics of computations.

2019

• + A. Gollamudi, S. Chong, and O. Arden, “Information Flow Control for Distributed Trusted Execution Environments,” in Proc. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), 2019, pp. 304–318.
  Abstract: Distributed applications cannot assume that their security policies will be enforced on untrusted hosts. Trusted execution environments (TEEs) with cryptography enable execution of known code on untrusted hosts. TEEs do not establish trustworthiness of code executing inside them. This paper presents DFLATE, a core security calculus for distributed applications with TEEs. DFLATE enforces strong confidentiality but only weak integrity, reflecting TEE guarantees.

2018

• + A. Gollamudi and C. Fournet, “Building Secure SGX Enclaves using F*, C/C++ and X64,” in Proc. 2nd Workshop on Principles of Secure Compilation (PriSC), vol. 10, p. 46, 2018.
  Abstract: Intel SGX offers hardware mechanisms to isolate code and data running within enclaves. We use F∗ to develop specifications, code, and proofs, and safely compile F∗ code to standalone C. Legacy C++ code is also compiled defensively using runtime guards. The approach combines statically-verified F∗ code, dynamically-monitored C++, and SGX instructions, reasoning across different semantics layers (F∗ and X64).

2016

• + B. Karthikeyan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamy, et al., “Formal Verification of Smart Contracts,” in Proc. ACM Workshop on Programming Languages and Analysis for Security, Vienna, Austria, 2016, pp. 91–96.
  Abstract: Ethereum is a framework for cryptocurrencies using blockchain technology. EVM executes bytecode on a stack machine. Solidity compiles to EVM bytecode, but secure smart contracts are difficult to write due to openness and untrusted interactions. We outline a framework to analyze and verify runtime safety and functional correctness of Ethereum contracts via translation to F*, a functional programming language aimed at program verification.
• + A. Gollamudi and S. Chong, “Automatic enforcement of expressive security policies using enclaves,” in Proc. 2016 ACM SIGPLAN Int. Conf. on OOPSLA, 2016, pp. 494–513.
  Abstract: Hardware-based enclave protection mechanisms, such as Intel SGX, ARM TrustZone, and Apple's Secure Enclave, can protect code and data from low-level attackers. We present IMPE, a calculus that captures SGX-like mechanisms and enforces expressive confidentiality policies against attackers, including corrupt non-enclave code. A translation from a security-typed calculus automatically places code and data into enclaves.