Presentation

· Contributors · Organizations · Search Program · My Agenda

Towards A Formally Verified Fully Homomorphic Encryption Compute Engine

SessionThis is Formal...But You Can Come Casual!

DescriptionWe present a scalable approach for formally verifying the correctness of an 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 micro-architecture 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.

Authors

University of California, Berkeley

Jin Yang

Intel

Event Type