Paper 2026/1387

ZK-Audit: Proving Power Side-Channel Resilience in Synthesized Hardware

Abstract

Modern hardware security heavily relies on the assumption that pre-synthesis algorithmic protections will survive the physical fabrication pipeline. However, untrusted third-party Electronic Design Automation (EDA) toolchains often apply aggressive structural optimizations that can silently compromise perfectly symmetric designs, introducing critical data-dependent power side-channel vulnerabilities. Existing pre-silicon verification methodologies require exposing highly sensitive, proprietary gate-level intellectual property (IP) to external auditors to verify structural security. In this paper, we introduce a novel Zero-Knowledge Hardware Auditor, an end-to-end framework that provides mathematical guarantees of physical data-obliviousness without revealing the underlying circuit netlist. By translating synthesized gate-level topologies into a custom Side-Channel Intermediate Language (SCIL), our architecture maps physical dynamic switching activity into arithmetic constraints executable within a Halo2 zero-knowledge virtual machine (zkVM). This enables the first implementation of a zero-knowledge Bounded Toggle Assessment (ZK-BTA), a deterministic structural counterpart to classical Test Vector Leakage Assessment. Experimental evaluations across standard cryptographic primitives and ISCAS-85 benchmarks demonstrate that the framework successfully identifies inherently leaky logic and captures EDA-induced asymmetries, such as a 13% leakage rate introduced into a theoretically secure Montgomery Ladder, while proving the structural integrity of Dual-Rail oblivious logical topologies. Furthermore, the asymmetric zk-SNARK architecture ensures scalable component-level auditing, yielding a succinct cryptographic proof of physical security that can be publicly verified in under 0.08 seconds.