Azkaban: A Zero-Knowledge Abstract Analysis for Neural Networks

Deep neural networks (DNNs) are increasingly used in sensitive applications, where certifying properties such as adversarial robustness and fairness is crucial. Several recent works propose DNN certification systems using zero-knowledge proofs (ZKPs)— cryptographic primitives that allow verifying certificates while maintaining confidentiality of the model. While certification algorithms typically treat the DNN as a function over reals, naively translating these algorithms into finite-precision implementations can result in unsound certification due to rounding errors. In ZKPs, this unsoundness is amplified due to a larger precision loss from fixed-point arithmetic emulated using finite fields. In this work, we highlight an overlooked gap in the soundness of prior protocols. We propose AZKABAN, a system for zero-knowledge abstract interpretation-based analysis with end-to-end soundness. We introduce operators for sound interval analysis over finite-fields, including efficient ZKP-amenable algorithms for inner-products and division, while preventing privacy leaks due to non-linear activations. We implement our system which is comprehensive in terms of supporting both feed-forward and convolutional neural networks. AZKABAN improves over the state-of-the-art ZK individual fairness certification protocol by up to two orders of magnitude in end-to-end proof time. Further, it scales to much larger models than those considered in the state-of-the-art. AZKABAN also provides, to our knowledge, the first solution for ZK robustness certification.