Towards a Formally Verified Fully Homomorphic Encryption Compute Engine

Towards a Formally Verified Fully Homomorphic Encryption Compute Engine

연구 분야: Verification

학회: DAC '23: Proceedings of the 60th Annual ACM/IEEE Design Automation Conference

We present a scalable approach for formally verifying the correctness of the Compute Engine (CE) against its ISA (Instruction Set Architecture) specification in an FHE (Fully Homomorphic Encryption) accelerator, critical to many applications where safety and security of information is of vital importance. It combines algorithmic verification of the microarchitecture modules in the CE against their functional specifications and implementation verification of the CE hardware against its micro-architecture algorithmic specifications. The correctness of the CE is guaranteed by treating micro-architecture modules as semantic-preserving program transformations and leveraging the composability of the semantic-preserving properties well established in compiler design and verification.