Formal Verification of a Custom Compiler for a Fully Homomorphic Encryption Accelerator

We present a methodology to formally verify a custom compiler for a Fully Homomorphic Encryption (FHE) accelerator. Prior research has addressed formal verification of the hardware component of such accelerators. Equally important is the correctness of the software stack that decomposes and com-piles an FHE workload into the actual sequence of instructions that execute on the hardware. To ensure the correctness of the resulting instruction sequences, we apply a three-step verification process to 1) check for deadlocks, 2) build a baseline functional model of the instructions, and 3) verify that all possible executions of the instructions, subject to hardware design constraints such as latency variability, concurrency, etc. on the accelerator, will always match the baseline model. Coupling this verification step with the compiler not only guarantees correctness of the compiler results, but also enables quick feedback on the correctness of experimental optimizations as the compiler continues to evolve. We demonstrate how the proposed methodology is capable of identifying different types of bugs in a FHE accelerator compiler implementation.