-
+
W. B. Nuzzo, B. Houle, S. Dodson and A. Gollamudi, “Short Paper: Permissive IFC Type System for Control-Flow Operations,” in 20th Workshop on Programming Languages and Analysis for Security (PLAS), 2025. Quick notes: Proposes a new type system to capture implicit flows in assembly-level languages.
Static information flow control type systems are carefully designed to prevent label creep problem: “pc”, the security label used to track the control flow sensitivity, increases monotonically and quickly reaches the top of the security lattice. This makes the type system overly restrictive. In languages with structured control flow, “pc” grows monotonically whenever control flow diverges (e.g., branches) but is reset to its original state at the convergence point. This enables the type system to be permissive. However, in languages with unstructured control flow, such as assembly level languages with explicit jumps, the “pc” reset point is not straight forward.
In this work, we investigate a permissive IFC type system for languages with unstructured control flow. Specifically, we use LLVM intermediate representation as our representative language with explicit jumps. Our key insight is that post-dominator nodes are the “pc” reset points, enabling a permissive control flow tracking. Our permissive type system enforces noninterference and is a work in progress.
-
+
T. Gollamudi, A. Gollamudi, and J. Gancher, “ILA: Correctness via Type Checking for Fully Homomorphic Encryption,” in ACM CCS, 2025.
Quick notes: Generalizes ILA to BGV/BFV and TFHE schemes
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.
-
+
T. Gollamudi, A. Gollamudi, and J. Gancher, “ILA: Correctness via Type Checking for Fully Homomorphic Encryption,” in Workshop on Principles of Secure Compilation (PriSC), 2025. Quick notes: Introduces ILA, a formal semantics analysis framework for BGV FHE scheme.
Abstract:
Popular 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 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. Additionally, we have designed ILA to be maximally general: our core type system does not directly assume a particular FHE scheme, but instead axiomatizes a model of FHE. We instantiate this model with the BGV scheme and get functional correctness for free.
We implemented the static ILA type checker parameterized by the noise estimators. We also use the type checker to infer the optimal placement of modulus switching, a noise reducing operation. Evaluation shows that the type checker is sound (always detects noise overflows) and practical (noise estimates are tight).
-
+
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. Quick notes: Compartmentalize LLVM IR applications to Intel SGX enclaves.
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.
