arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2509.11559

ILA: Correctness via Type Checking for Fully Homomorphic Encryption

Tarakaram Gollamudi·Anitha Gollamudi·Joshua Gancher
View original source ↗Read source document ↗Export metadata ↓

Abstract

RLWE-based Fully Homomorphic Encryption (FHE) schemes add some small \emph{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. However, 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. These two limitations of existing compilers and libraries make FHE applications too difficult to develop with confidence. In this work, we present a \emph{correctness-oriented} IR, Intermediate Language for Arithmetic circuits, 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 \emph{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 \emph{model} of FHE. We instantiate this model with the exact FHE schemes (BGV, BFV and TFHE), and obtain functional correctness for free.

Explore related subjects

cs.CRcs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Tarakaram Gollamudi, Anitha Gollamudi, Joshua Gancher. 2025-09-15. ILA: Correctness via Type Checking for Fully Homomorphic Encryption. https://arxiv.org/abs/2509.11559

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

IntraGuard: Committee-Side Defenses Against Review Outsourcing to Commercial Chatbots

LLMs become increasingly capable, editorial boards and program committees are growing concerned about reviewers who fully outsource peer review to commercial chatbots. This concern stems from prior findings that current chatbots lack the independent critical thinking and depth of reasoning required to assess scientific novelty. One promising direction for mitigating this concern is to embed hidden instructions into manuscripts that disrupt or alter chatbot-generated reviews. However, existing methods remain intuitive and fragile, as they typically rely on homogeneous payloads injected in an inter-stream manner, rendering them susceptible to sanitization or neutralization. More broadly, the community still lacks a systematic formulation of this threat and a principled defense framework. In this paper, we identify End-to-End Review Outsourcing as an emerging threat and propose IntraGuard, a black-box, venue-agnostic defense framework grounded in the structural--visual decoupling inherent to the PDF. Designed for committee-side deployment, IntraGuard supports both explicit strategies that trigger refusal or warning signals, and implicit strategies that embed predefined textual markers into the generated review. These strategies can be deployed via any of three intra-stream injection mechanisms, each of which seamlessly embeds heterogeneous defensive text objects within the PDF's underlying structure without altering its visual presentation. Extensive evaluations (over 17,844 cases) across 7 real-world commercial chatbot settings and 12 venues spanning diverse disciplines show that IntraGuard achieves a defense success rate of up to 84%, while preserving peer-review invariance for human reviewers. We further evaluate 11 adaptive attacks spanning manuscript sanitization and instruction interference, and discuss the implications of constructing ensemble defenses.

cs.CR↗
arXiv2026

Efficient Fuzzy PSI under One-Sided Assumptions

Fuzzy private set intersection (PSI) enables two parties to identify approximately matching elements between their input sets, where two elements are considered a match if their distance is at most a threshold $δ$ under a given metric. Although substantial progress has been made, existing constructions for general Minkowski distances either rely on strong two-sided geometric separation assumptions or incur substantial overhead under one-sided assumptions. In this work, we present the first concretely efficient fuzzy PSI protocols for general $L_{p\in[1,\infty]}$ distances under one-sided assumptions, relying solely on lightweight symmetric-key primitives. Our constructions support both sender-sided and receiver-sided settings. We further study sparser input distributions and present more efficient protocols tailored to this case. To reduce the overhead scaling with $δ$, we non-trivially incorporate prefix trie techniques into our protocols, achieving $O(\logδ)$ complexity for general $L_{p\in[1,\infty]}$ distances for the first time, improving upon $O((\logδ)^d)$ or $O(δ)$ complexities of prior works. Extensive experiments, across a wide range of parameter settings, show that our protocols significantly outperform prior works under the same assumptions. Specifically, against van Baarsen and Pu (EUROCRYPT'24), our protocols achieve up to $248\times$ faster computation and up to $20\times$ lower communication. Against Dang et al. (CCS'25), we achieve up to $568\times$ speedup and up to $63\times$ communication reduction. Against Bui et al. (ASIACRYPT'25), we achieve up to $4978\times$ faster computation and up to $282\times$ lower communication.

cs.CR↗
arXiv2026

Enc53: DNSSEC-Anchored Stateless Tickets for Post-Quantum Authoritative DNS

DNSSEC authenticates RRsets, but does not provide endpoint authentication or channel security. DNS-over-TLS (DoT) and DNS-over-QUIC (DoQ) can facilitate such needs, but were designed for the stub-to-resolver hop, where stable long-lived connections amortize the expensive initial setup. The recursive-to-authoritative path's high fan-in and nonuniform per-resolver query frequency invert said dynamics. Post- quantum primitives further sharpen this mismatch: an ML-DSA WebPKI certificate chain crosses TCP's initial window, a cold PQ DoQ may incur up to about 140 times the total bytes of the same query over UDP. A survey of TLD and 2LD nameservers further bounds connection lifetimes, with almost half surveyed imposing limits on even non-idle connections. We present Enc53 -- a stateless session ticket protocol enabling efficient authenticated authoritative DNS encryption. Enc53 splits DNS encryption into 2 phases: a short-lived, DNSSEC-anchored, TLS- authenticated provisioning on the initial query in the 1st, and a steady state of 1-RTT AEAD-encrypted UDP DNS queries in the 2nd. Enc53 is server-side stateless: recursive resolvers hold the traffic secret and session ticket, authoritative nameservers hold only a symmetric STEK. We implemented Enc53 in Knot DNS. After provisioning, a steady state Enc53 exchange costs about 570 B -- roughly 3 times a plain UDP query -- and lands within 1 ms of the unencrypted UDP baseline. Resumed PQ-ADoT pays 7.7 times the bytes and 3 times the latency; resumed PQ-ADoQ pays 10 times the bytes for the same latency. When evaluated against a root server query trace, Enc53 achieves 2-fold compute efficiency over ADoT/ADoQ, 3-fold memory efficiency over ADoT, and 12-fold memory efficiency over ADoQ. Finally, when deployed in conjunction with FN-DSA-512 PQ-DNSSEC, the joint Enc53-DNSSEC UDP datagram remains below the 1232B buffer limit.

cs.CR↗