ILA: Correctness via Type Checking for Fully Homomorphic Encryption
summary
ILA is an intermediate language that attaches quantitative bounds (plaintext range and ciphertext noise) as types and proves that well-typed ILA circuits decrypt correctly. Implementation uses Microsoft SEAL and an instantiation for BGV, plus a static type checker that infers bounds and automatically places modulus-switching bootstraps. Evaluation shows the checker is sound (always flags noise overflow), gives tight noise estimates, and matches SEAL’s multiplicative depth in almost all benchmarks, making correctness checking practical.
AI-written summary · about
chapters (16)
- 0:00Homomorphic encryption intro
- 1:27FHE in Microsoft SEAL example
- 2:34Ring learning with errors
- 4:41Noise growth and decryption
- 6:07Tracking noise with types
- 7:09Functional correctness in FHE
- 8:13Overflow errors beyond noise
- 9:19Lattice-based type bounds
- 10:01Introducing ILA language
- 11:30ISA model for FHE schemes
- 12:57ISA operator specs
- 14:24Ciphertext bounds without key
- 15:48Typing rules for noise overflow
- 16:53Noise management and refresh
- 18:36Evaluation vs Microsoft SEAL
- 20:46Q&A
related talks
57mTutorial: Encrypted Computation from Lattices
51mObfuscation via GGH15 Encodings, 10 Years Later
46mRunning Circuits of Unbounded Depth over Encrypted Data, Securely, Using Lattices...
17mCalculational design of Incorrectness Separation Logic
01h 04mHow to Encrypt a Functionality
31mIdentity-Based Encryption
33mTeIL: a type-safe imperative Tensor Intermediate Language
22mCounterexample-Guided Inference of Modular Specifications